source: src/Clight/test/runtime.test.ma @ 2106

Last change on this file since 2106 was 1276, checked in by campbell, 9 years ago

Support for replacing operations with runtime support functions in Clight.
Note the caveats in the comments.

File size: 453 bytes
Line 
1include "Clight/test/runtime.c.ma".
2
3
4include "Clight/fresh.ma".
5include "Clight/SimplifyCasts.ma".
6include "Clight/addRuntime.ma".
7
8definition u ≝ universe_for_program myprog.
9definition p0 ≝ simplify_program myprog.
10definition p ≝ \fst (add_runtime_replacements p0 u).
11
12(*
13example x : result ? p.
14normalize
15*)
16
17example exec: result ? (exec_up_to clight_fullexec p 1000 [EVint I32 (repr I32 0)]).
18normalize  (* you can examine the result here *)
Note: See TracBrowser for help on using the repository browser.