Changeset 1876 for src/Clight/test

Timestamp:

Apr 4, 2012, 6:48:26 PM (9 years ago)

Author:

campbell

Message:

Update Cexec soundness proof.
Change finishes_with predicate to inductive form so that qed no longer
spends huge amounts of time typechecking.

Location:

src/Clight/test

Files:

• castremoval.test.ma (modified) (2 diffs)
• duff.test.ma (modified) (1 diff)
• factorial.test.ma (modified) (1 diff)
• null-op.test.ma (modified) (1 diff)
• search.c.ma (modified) (3 diffs)
• sum.test.ma (modified) (4 diffs)
• switcher.test.ma (modified) (1 diff)

src/Clight/test/castremoval.test.ma

@@ -4 +4 @@
 example exec: finishes_with (repr I32 1) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
 normalize  (* you can examine the result here *)
-@refl
+%
 qed.
 
@@ -16 +16 @@
 example exec_s: finishes_with (repr I32 1) ? (exec_up_to clight_fullexec (simplify_program myprog) 1000 [EVint I32 (repr I32 0)]).
 normalize  (* you can examine the result here *)
-@refl
+%
 qed.
 

src/Clight/test/duff.test.ma

@@ -3 +3 @@
 example exec: finishes_with (repr I32 6) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
 normalize  (* you can examine the result here *)
-@refl
+%
 qed.

src/Clight/test/factorial.test.ma

@@ -3 +3 @@
 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/null-op.test.ma

@@ -3 +3 @@
 example exec: finishes_with (repr 1) ? (exec_up_to clight_fullexec myprog 50 [ ]).
 normalize  (* you can examine the result here *)
-@refl
+%
 qed.

src/Clight/test/search.c.ma

@@ -186 +186 @@
 example exec: finishes_with (repr I32 3) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
 normalize  (* you can examine the result here *)
-@refl
+%
 qed.
 
@@ -197 +197 @@
 *)
 normalize
-@refl
+%
 qed.
 
@@ -213 +213 @@
  exec_up_to RTLabs_fullexec p2 1000 [ ]).*)
 normalize
-@refl
+%
 qed.
 (*

src/Clight/test/sum.test.ma

@@ -3 +3 @@
 example exec: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
 normalize  (* you can examine the result here *)
-@refl
+%
 qed.
 
@@ -10 +10 @@
 example es: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec (simplify_program myprog) 1000 [ ]).
 normalize  (* you can examine the result here *)
-@refl
+%
 qed.
 
@@ -20 +20 @@
    (λp. exec_up_to Cminor_fullexec p 1000 [ ])).
 normalize
-@refl
+%
 qed.
 
@@ -31 +31 @@
  (λp2. exec_up_to RTLabs_fullexec p2 1000 [ ]))).
 normalize
-@refl
+%
 qed.
 (*

src/Clight/test/switcher.test.ma

@@ -4 +4 @@
 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.
+% qed.
 
 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.
+% qed.
 
 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.
+% qed.
 
 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.
+% qed.
 
 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.
+% qed.