source: src/Clight/test/castremoval.test.ma @ 2177

Last change on this file since 2177 was 1876, checked in by campbell, 8 years ago

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

File size: 537 bytes
Line 
1include "common/Animation.ma".
2include "Clight/test/castremoval.c.ma".
3
4example exec: finishes_with (repr I32 1) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
5normalize  (* you can examine the result here *)
6%
7qed.
8
9include "Clight/SimplifyCasts.ma".
10
11example simplified: result ? (simplify_program myprog).
12normalize
13%
14qed.
15
16example exec_s: finishes_with (repr I32 1) ? (exec_up_to clight_fullexec (simplify_program myprog) 1000 [EVint I32 (repr I32 0)]).
17normalize  (* you can examine the result here *)
18%
19qed.
20
Note: See TracBrowser for help on using the repository browser.