source: src/Clight/test/sum.ma @ 881

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

Sort out regions in Cminor to fix Clight to Cminor translation of Ederef.

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