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

Last change on this file since 961 was 961, checked in by campbell, 10 years ago

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

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 I32 (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 I32 (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 I32 (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 I8 28)) ; (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 17)) ;
54     (Init_int8 (repr I8 8)) ; (Init_int8 (repr I8 4)) ]〉, Any〉,
55     (Tarray Any (Tint I8 Unsigned ) 5)〉]
56.
57
58example exec: finishes_with (repr I32 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.