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

Last change on this file since 2771 was 2180, checked in by campbell, 8 years ago

Fix off-by-one error in GenMem?.ma.

File size: 1.1 KB
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  ) [] [〈ident_of_nat 1, (Tarray (Tint I8 Unsigned ) 4)〉 ]
7         (Ssequence
8         (Sassign (Expr (Ederef
9                    (Expr (Ebinop Oadd
10                      (Expr (Evar (ident_of_nat 1))
11                        (Tarray (Tint I8 Unsigned ) 4))
12                      (Expr (Econst_int I32 (repr ? 4)) (Tint I32 Signed  )))
13                      (Tpointer (Tint I8 Unsigned )))) (Tint I8 Unsigned ))
14           (Expr (Ecast (Tint I8 Unsigned )
15             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
16             (Tint I8 Unsigned )))
17         (Sreturn (Some expr (Expr (Econst_int I32 (repr ? 0))
18                               (Tint I32 Signed  )))))
19       
20       
21       
22     )〉]
23  (ident_of_nat 0)
24 
25.
26
27(*
28example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
29normalize  (* you can examine the result here *)
30*)
Note: See TracBrowser for help on using the repository browser.