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

Last change on this file since 1276 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: 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.