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

Last change on this file since 881 was 881, checked in by campbell, 10 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.