Changeset 768 for src/Cminor/test/factorial.ma

Timestamp:

Apr 22, 2011, 1:49:12 PM (10 years ago)

Author:

campbell

Message:

Make Cminor tests test translation to RTLabs.

File:

• src/Cminor/test/factorial.ma (modified) (1 diff)

src/Cminor/test/factorial.ma

@@ -77 +77 @@
 normalize  (* you can examine the result here *)
 @refl qed.
+
+include "Cminor/toRTLabs.ma".
+include "RTLabs/semantics.ma".
+
+example execRTL: finishes_with (repr 120) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [EVint (repr 5)]).
+normalize  (* you can examine the result here *)
+@refl
+qed.
+