source: src/Clight/test/null-op.test.ma

Last change on this file 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: 176 bytes
RevLine 
[1513]1include "Clight/test/null-op.c.ma".
2
3example exec: finishes_with (repr 1) ? (exec_up_to clight_fullexec myprog 50 [ ]).
4normalize  (* you can examine the result here *)
[1876]5%
[1513]6qed.
Note: See TracBrowser for help on using the repository browser.