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

Last change on this file since 1631 was 1276, checked in by campbell, 10 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.