Changeset 978 for src/Clight/test

Timestamp:

Jun 16, 2011, 1:32:19 PM (10 years ago)

Author:

campbell

Message:

Update remaining Clight examples.

Location:

src/Clight/test

Files:

• duff.ma (deleted)
• factorial.c.ma (moved) (moved from src/Clight/test/factorial.ma) (4 diffs)
• io.ma (deleted)
• io2.ma (deleted)
• search.c.ma (added)
• switcher.c.ma (moved) (moved from src/Clight/test/switcher.ma) (7 diffs)

src/Clight/test/factorial.c.ma

@@ -8 +8 @@
       (Ssequence
       (Scall (Some expr (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
-        (Expr (Evar (ident_of_nat 0))
-          (Tfunction Tnil (Tint I32 Signed  )))
+        (Expr (Evar (ident_of_nat 0)) (Tfunction Tnil (Tint I32 Signed  )))
         [])
       (Ssequence
       (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
-        (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
-      (Ssequence
+        (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
       (Ssequence
       (Sfor (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
-              (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
-        (Expr (Ebinop Ole
-          (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
+              (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
+        (Expr (Ebinop Ole (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
           (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
           (Tint I32 Signed  ))
@@ -25 +22 @@
           (Expr (Ebinop Oadd
             (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
-            (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
+            (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
             (Tint I32 Signed  )))
         (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
@@ -33 +30 @@
             (Tint I32 Signed  )))
       )
-      Sskip)
-      (Sreturn (Some expr (Expr (Evar (ident_of_nat 3))
-                            (Tint I32 Signed  )))))))
+      (Sreturn (Some expr (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  )))))))
     
     
@@ -44 +39 @@
 .
 
-example exec: finishes_with (repr 120) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 5)]).
+example exec: finishes_with (repr I32 120) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 5)]).
 normalize  (* you can examine the result here *)
 @refl qed.

src/Clight/test/switcher.c.ma

@@ -9 +9 @@
       (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
         (Expr (Ecast (Tint I8 Unsigned )
-          (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
+          (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
           (Tint I8 Unsigned )))
       (Ssequence
@@ -17 +17 @@
         [])
       (Sswitch (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  )) (
-        (LScase (repr 1)
+        (LScase I32 (repr ? 1)
           Sbreak
-          (LScase (repr 3)
+          (LScase I32 (repr ? 3)
             (Ssequence
             (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
@@ -27 +27 @@
                     (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
                     (Tint I32 Signed  ))
-                  (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
+                  (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
                   (Tint I32 Signed  ))) (Tint I8 Unsigned )))
             Sbreak)
-            (LScase (repr 5)
+            (LScase I32 (repr ? 5)
               (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
                 (Expr (Ecast (Tint I8 Unsigned )
@@ -37 +37 @@
                       (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
                       (Tint I32 Signed  ))
-                    (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
+                    (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
                     (Tint I32 Signed  ))) (Tint I8 Unsigned )))
-              (LScase (repr 7)
+              (LScase I32 (repr ? 7)
                 (Ssequence
                 (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
@@ -47 +47 @@
                         (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
                         (Tint I32 Signed  ))
-                      (Expr (Econst_int (repr 3)) (Tint I32 Signed  )))
+                      (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
                       (Tint I32 Signed  ))) (Tint I8 Unsigned )))
                 Sbreak)
@@ -57 +57 @@
                           (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
                           (Tint I32 Signed  ))
-                        (Expr (Econst_int (repr 16)) (Tint I32 Signed  )))
-                        (Tint I32 Signed  ))) (Tint I8 Unsigned ))))))))
+                        (Expr (Econst_int I32 (repr ? 16))
+                          (Tint I32 Signed  ))) (Tint I32 Signed  )))
+                      (Tint I8 Unsigned ))))))))
       )))
       (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
@@ -71 +72 @@
 .
 
-example exec0: finishes_with (repr 16) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 0)]).
+example exec0: finishes_with (repr I32 16) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 0)]).
 normalize  (* you can examine the result here *)
 @refl qed.
 
-example exec1: finishes_with (repr 0) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 1)]).
+example exec1: finishes_with (repr I32 0) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 1)]).
 normalize  (* you can examine the result here *)
 @refl qed.
 
-example exec3: finishes_with (repr 1) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 3)]).
+example exec3: finishes_with (repr I32 1) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 3)]).
 normalize  (* you can examine the result here *)
 @refl qed.
 
-example exec5: finishes_with (repr 5) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 5)]).
+example exec5: finishes_with (repr I32 5) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 5)]).
 normalize  (* you can examine the result here *)
 @refl qed.
 
-example exec7: finishes_with (repr 3) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 7)]).
+example exec7: finishes_with (repr I32 3) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 7)]).
 normalize  (* you can examine the result here *)
 @refl qed.