source: src/Clight/test/castremoval.c.ma @ 2106

Last change on this file since 2106 was 1513, checked in by campbell, 9 years ago

Fix up Clight examples.

File size: 3.5 KB
RevLine 
[1198]1include "Clight/Cexec.ma".
2include "common/Animation.ma".
3
[1513]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 I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 4, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 5, (Tint I8 Unsigned )〉 ]
7         (Ssequence
8         (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
9           (Expr (Ecast (Tint I8 Unsigned )
10             (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
11             (Tint I8 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 ? 2)) (Tint I32 Signed  )))
16             (Tint I8 Unsigned )))
17         (Ssequence
18         (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
19           (Expr (Ecast (Tint I8 Unsigned )
20             (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed  )))
21             (Tint I8 Unsigned )))
22         (Ssequence
23         (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I8 Unsigned ))
24           (Expr (Ecast (Tint I8 Unsigned )
[1198]25             (Expr (Ebinop Oadd
26               (Expr (Ecast (Tint I32 Signed  )
27                 (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
28                 (Tint I32 Signed  ))
29               (Expr (Ecast (Tint I32 Signed  )
30                 (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
[1513]31                 (Tint I32 Signed  ))) (Tint I32 Signed  )))
32             (Tint I8 Unsigned )))
33         (Ssequence
34         (Sassign (Expr (Evar (ident_of_nat 5)) (Tint I8 Unsigned ))
35           (Expr (Ecast (Tint I8 Unsigned )
36             (Expr (Ebinop Oadd
37               (Expr (Ebinop Oadd
38                 (Expr (Ecast (Tint I32 Signed  )
39                   (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
40                   (Tint I32 Signed  ))
41                 (Expr (Ecast (Tint I32 Signed  )
42                   (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
43                   (Tint I32 Signed  ))) (Tint I32 Signed  ))
44               (Expr (Ecast (Tint I32 Signed  )
45                 (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
46                 (Tint I32 Signed  ))) (Tint I32 Signed  )))
47             (Tint I8 Unsigned )))
48         (Sreturn (Some expr (Expr (Ebinop Oeq
[1198]49                               (Expr (Ecast (Tint I32 Signed  )
[1513]50                                 (Expr (Evar (ident_of_nat 5))
[1198]51                                   (Tint I8 Unsigned ))) (Tint I32 Signed  ))
[1513]52                               (Expr (Ebinop Oadd
53                                 (Expr (Ecast (Tint I32 Signed  )
54                                   (Expr (Evar (ident_of_nat 4))
55                                     (Tint I8 Unsigned )))
56                                   (Tint I32 Signed  ))
57                                 (Expr (Ecast (Tint I32 Signed  )
58                                   (Expr (Evar (ident_of_nat 3))
59                                     (Tint I8 Unsigned )))
60                                   (Tint I32 Signed  ))) (Tint I32 Signed  )))
61                               (Tint I32 Signed  )))))))))
62       
63       
64       
65     )〉]
[1198]66  (ident_of_nat 0)
[1513]67 
[1198]68.
69
[1513]70(*
71example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
[1198]72normalize  (* you can examine the result here *)
[1513]73*)
Note: See TracBrowser for help on using the repository browser.