Changeset 1991 for src/Clight/test

Timestamp:

May 24, 2012, 4:24:55 PM (9 years ago)

Author:

campbell

Message:

Put the front end transformations together and make an example use it.

Location:

src/Clight/test

Files:

• search.c.ma (modified) (1 diff)
• search.test.ma (added)

src/Clight/test/search.c.ma

@@ -184 +184 @@
 .
 
-example exec: finishes_with (repr I32 3) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
-normalize  (* you can examine the result here *)
-%
-qed.
-
-include "Clight/toCminor.ma".
-include "Cminor/semantics.ma".
-
-example e1: finishes_with (repr I32 3) ? (bind ? (snapshot state) (clight_to_cminor myprog) (λp. exec_up_to Cminor_fullexec p 1000 [ ])).
-(*
-example e1: finishes_with (repr I32 3) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
-*)
-normalize
-%
-qed.
-
-include "Cminor/toRTLabs.ma".
-include "RTLabs/semantics.ma".
-
-example e2: finishes_with (repr 3) ? (
-do p1 ← clight_to_cminor myprog;
-bind ? (snapshot state) (cminor_to_rtlabs p1) (λp2.
- exec_up_to RTLabs_fullexec p2 1000 [ ])).
-(*
-example e2: finishes_with (repr 3) ? (
-do p1 ← clight_to_cminor myprog;
-do p2 ← cminor_to_rtlabs p1;
- exec_up_to RTLabs_fullexec p2 1000 [ ]).*)
-normalize
-%
-qed.
-(*
-example csc: True.
-letin yyy ≝ (
-let xxx ≝ (clight_to_cminor myprog) in
-do p ← xxx ; cminor_to_rtlabs p)
-normalize in yyy;
-include "RTLabs/RTLabsToRTL.ma".
-
-example csc: True.
-letin xxx ≝ (clight_to_cminor myprog)
-letin yyy ≝ (do p ← xxx ; cminor_to_rtlabs p)
-letin zzz ≝ (do p ← yyy ; rtlabs_to_rtl p)
-@⊥ normalize in xxx;
-*)