Changeset 965 for src/Clight/test

Timestamp:

Jun 15, 2011, 4:15:56 PM (10 years ago)

Author:

campbell

Message:

Update some Clight examples.

Location:

src/Clight/test

Files:

• duff.c.ma (added)
• insertsort.c (modified) (1 diff)
• insertsort.c.ma (added)
• insertsort.ma (deleted)
• null-op.c.ma (moved) (moved from src/Clight/test/null-op.ma) (6 diffs)
• search.ma (deleted)
• sum.c.ma (moved) (moved from src/Clight/test/sum.ma) (6 diffs)

src/Clight/test/insertsort.c

@@ +1 @@
+/* Remove memory region for now. */
+#define __pdata
+
 struct list {
   unsigned char i;

src/Clight/test/null-op.c.ma

@@ -9 +9 @@
                   (Tpointer Any (Tint I8 Unsigned )))
          (Expr (Ecast (Tpointer Any (Tint I8 Unsigned ))
-           (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
+           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
            (Tpointer Any (Tint I8 Unsigned ))))
        (Ssequence
@@ -23 +23 @@
                         (Tpointer Any (Tint I8 Unsigned ))))
                       (Tint I32 Signed  ))
-         (Sreturn (Some expr (Expr (Econst_int (repr 0)) (Tint I32 Signed  ))))
+         (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
+                               (Tint I32 Signed  ))))
          Sskip)
        (Ssequence
@@ -33 +34 @@
                           (Tpointer Any (Tint I8 Unsigned ))))
                         (Tint I32 Signed  ))
-                      (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
+                      (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
                       (Tint I32 Signed  ))
-         (Sreturn (Some expr (Expr (Econst_int (repr 0)) (Tint I32 Signed  ))))
+         (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
+                               (Tint I32 Signed  ))))
          Sskip)
        (Ssequence
@@ -42 +44 @@
          (Expr (Ebinop Oadd
            (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned )))
-           (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
+           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
            (Tpointer Any (Tint I8 Unsigned ))))
        (Ssequence
        (Sassign (Expr (Evar (ident_of_nat 2))
                   (Tpointer Any (Tint I8 Unsigned )))
-         (Expr (Ebinop Oadd (Expr (Econst_int (repr 0)) (Tint I32 Signed  ))
+         (Expr (Ebinop Oadd
+           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  ))
            (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned ))))
            (Tpointer Any (Tint I8 Unsigned ))))
@@ -55 +58 @@
          (Expr (Ebinop Osub
            (Expr (Evar (ident_of_nat 2)) (Tpointer Any (Tint I8 Unsigned )))
-           (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
+           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
            (Tpointer Any (Tint I8 Unsigned ))))
        (Sreturn (Some expr (Expr (Ebinop Oeq
@@ -62 +65 @@
                              (Expr (Ecast (Tpointer Any (Tint I8 Unsigned ))
                                (Expr (Ecast (Tpointer Any Tvoid)
-                                 (Expr (Econst_int (repr 0))
-                                   (Tint I32 Unsigned)))
+                                 (Expr (Econst_int I8 (repr ? 0))
+                                   (Tint I8 Unsigned )))
                                  (Tpointer Any Tvoid)))
                                (Tpointer Any (Tint I8 Unsigned ))))

src/Clight/test/sum.c.ma

@@ +1 @@
+include "Clight/Cexec.ma".
 include "common/Animation.ma".
-include "Clight/Cexec.ma".
 
 definition myprog := mk_program clight_fundef type
@@ -10 +10 @@
            (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
            (Tint I8 Unsigned )))
-       (Ssequence
        (Ssequence
        (Sfor (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
@@ -37 +36 @@
                        (Tarray Any (Tint I8 Unsigned ) 5))
                      (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  )))
-                     (Tarray Any (Tint I8 Unsigned ) 5)))
+                     (Tpointer Any (Tint I8 Unsigned ))))
                    (Tint I8 Unsigned ))) (Tint I32 Signed  )))
                (Tint I32 Signed  ))) (Tint I8 Unsigned )))
        )
-       Sskip)
        (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
                              (Expr (Evar (ident_of_nat 2))
@@ -51 +49 @@
   (ident_of_nat 0)
   [〈〈〈ident_of_nat 3 (* src *),
-     [(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 17)) ;
-     (Init_int8 (repr I8 8)) ; (Init_int8 (repr I8 4)) ]〉, Any〉,
+     [(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ;
+     (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 8)) ;
+     (Init_int8 (repr I8 4)) ]〉, Any〉,
      (Tarray Any (Tint I8 Unsigned ) 5)〉]
 .
@@ -64 +63 @@
 include "Cminor/semantics.ma".
 
-example e1: finishes_with (repr 74) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
+example e1: finishes_with (repr I32 74) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
 normalize
 @refl
@@ -72 +71 @@
 include "RTLabs/semantics.ma".
 
-example e2: finishes_with (repr 74) ? (
+example e2: finishes_with (repr I32 74) ? (
 do p1 ← clight_to_cminor myprog;
 do p2 ← cminor_to_rtlabs p1;