source: src/Clight/test/trivial.c.ma @ 2771

Last change on this file since 2771 was 2535, checked in by campbell, 7 years ago

Add the trivial C program with check that there's a measurable subtrace.

File size: 561 bytes
Line 
1include "Clight/Cexec.ma".
2include "common/Animation.ma".
3
4definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
5  [][〈ident_of_nat 0 (* main *), CL_Internal (
6       mk_function (Tint I32 Signed  ) [] []
7         (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
8                               (Tint I32 Signed  ))))
9       
10       
11       
12     )〉]
13  (ident_of_nat 0)
14 
15.
16
17(*
18example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
19normalize  (* you can examine the result here *)
20*)
Note: See TracBrowser for help on using the repository browser.