source: src/Clight/test/sum.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.3 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 I32 Signed  )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ]
7       (Ssequence
8       (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
9         (Expr (Ecast (Tint I8 Unsigned )
10           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
11           (Tint I8 Unsigned )))
12       (Ssequence
13       (Sfor (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
14               (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
15         (Expr (Ebinop Olt
16           (Expr (Ecast (Tint I32 Unsigned)
17             (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  )))
18             (Tint I32 Unsigned))
19           (Expr (Esizeof (Tarray Any (Tint I8 Unsigned ) 5))
20             (Tint I32 Unsigned))) (Tint I32 Signed  ))
21         (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
22           (Expr (Ebinop Oadd
23             (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
24             (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
25             (Tint I32 Signed  )))
26         (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
27           (Expr (Ecast (Tint I8 Unsigned )
28             (Expr (Ebinop Oadd
29               (Expr (Ecast (Tint I32 Signed  )
30                 (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
31                 (Tint I32 Signed  ))
32               (Expr (Ecast (Tint I32 Signed  )
33                 (Expr (Ederef
34                   (Expr (Ebinop Oadd
35                     (Expr (Evar (ident_of_nat 3))
36                       (Tarray Any (Tint I8 Unsigned ) 5))
37                     (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  )))
38                     (Tpointer Any (Tint I8 Unsigned ))))
39                   (Tint I8 Unsigned ))) (Tint I32 Signed  )))
40               (Tint I32 Signed  ))) (Tint I8 Unsigned )))
41       )
42       (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
43                             (Expr (Evar (ident_of_nat 2))
44                               (Tint I8 Unsigned ))) (Tint I32 Signed  ))))))
45     
46     
47     
48   )〉]
49  (ident_of_nat 0)
50  [〈〈ident_of_nat 3 (* src *), Any〉,
51     〈[(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ;
52     (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 8)) ;
53     (Init_int8 (repr I8 4)) ],
54     (Tarray Any (Tint I8 Unsigned ) 5)〉〉]
55.
56
57example exec: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
58normalize  (* you can examine the result here *)
59@refl
60qed.
61
62include "Clight/SimplifyCasts.ma".
63
64example es: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec (simplify_program myprog) 1000 [ ]).
65normalize  (* you can examine the result here *)
66@refl
67qed.
68
69include "Clight/toCminor.ma".
70include "Cminor/semantics.ma".
71
72example e1: finishes_with (repr I32 74) ? (do p ← clight_to_cminor (simplify_program myprog); exec_up_to Cminor_fullexec p 1000 [ ]).
73normalize
74@refl
75qed.
76
77include "Cminor/toRTLabs.ma".
78include "RTLabs/semantics.ma".
79
80example e2: finishes_with (repr I32 74) ? (
81do p1 ← clight_to_cminor (simplify_program myprog);
82do p2 ← cminor_to_rtlabs p1;
83 exec_up_to RTLabs_fullexec p2 1000 [ ]).
84normalize
85@refl
86qed.
Note: See TracBrowser for help on using the repository browser.