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

Last change on this file since 2771 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: 2.3 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, (Tint I32 Unsigned)〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ]
7         (Ssequence
8         (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Unsigned))
9           (Expr (Ecast (Tint I32 Unsigned)
10             (Expr (Econst_int I32 (repr ? 16)) (Tint I32 Signed  )))
11             (Tint I32 Unsigned)))
12         (Ssequence
13         (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
14           (Expr (Ecast (Tint I8 Unsigned )
15             (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
16             (Tint I8 Unsigned )))
17         (Ssequence
18         (Swhile (Expr (Ebinop Odiv
19                   (Expr (Evar (ident_of_nat 1)) (Tint I32 Unsigned))
20                   (Expr (Ecast (Tint I32 Unsigned)
21                     (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
22                     (Tint I32 Unsigned))) (Tint I32 Unsigned))
23           (Ssequence
24           (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Unsigned))
25             (Expr (Ebinop Osub
26               (Expr (Evar (ident_of_nat 1)) (Tint I32 Unsigned))
27               (Expr (Ecast (Tint I32 Unsigned)
28                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
29                 (Tint I32 Unsigned))) (Tint I32 Unsigned)))
30           (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
31             (Expr (Ecast (Tint I8 Unsigned )
32               (Expr (Ebinop Oadd
33                 (Expr (Ecast (Tint I32 Signed  )
34                   (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
35                   (Tint I32 Signed  ))
36                 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
37                 (Tint I32 Signed  ))) (Tint I8 Unsigned )))))
38         (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
39                               (Expr (Evar (ident_of_nat 2))
40                                 (Tint I8 Unsigned ))) (Tint I32 Signed  )))))))
41       
42       
43       
44     )〉]
45  (ident_of_nat 0)
46 
47.
48
49(*
50example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
51normalize  (* you can examine the result here *)
52*)
Note: See TracBrowser for help on using the repository browser.