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

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

Fix up Clight examples.

File size: 3.5 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 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 )
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 )))
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
49                               (Expr (Ecast (Tint I32 Signed  )
50                                 (Expr (Evar (ident_of_nat 5))
51                                   (Tint I8 Unsigned ))) (Tint I32 Signed  ))
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     )〉]
66  (ident_of_nat 0)
67 
68.
69
70(*
71example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
72normalize  (* you can examine the result here *)
73*)
Note: See TracBrowser for help on using the repository browser.