source: src/Clight/test/ @ 1878

Last change on this file since 1878 was 1876, checked in by campbell, 9 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: 199 bytes
[1513]1include "Clight/test/".
3example exec: finishes_with (repr I32 6) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
4normalize  (* you can examine the result here *)
Note: See TracBrowser for help on using the repository browser.