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

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

Clight cast removal (NB: quite different from the prototype).

File size: 3.6 KB
Line 
1include "Clight/Cexec.ma".
2include "common/Animation.ma".
3
4definition myprog := mk_program 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 ))) (Tint I32 Signed  ))
56                               (Expr (Ecast (Tint I32 Signed  )
57                                 (Expr (Evar (ident_of_nat 3))
58                                   (Tint I8 Unsigned ))) (Tint I32 Signed  )))
59                               (Tint I32 Signed  ))) (Tint I32 Signed  )))))))))
60     
61     
62     
63   )〉]
64  (ident_of_nat 0)
65  []
66.
67
68example exec: finishes_with (repr I32 1) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
69normalize  (* you can examine the result here *)
70@refl
71qed.
72
73include "Clight/SimplifyCasts.ma".
74
75example simplified: result ? (simplify_program myprog).
76normalize
77%
78qed.
79
80example exec_s: finishes_with (repr I32 1) ? (exec_up_to clight_fullexec (simplify_program myprog) 1000 [EVint I32 (repr I32 0)]).
81normalize  (* you can examine the result here *)
82@refl
83qed.
84
Note: See TracBrowser for help on using the repository browser.