source: src/Clight/test/sum.c.ma @ 1139

Last change on this file since 1139 was 1139, checked in by campbell, 9 years ago

Shift init_data out of generic program record so that it only appears
in programs that contain initialisation data (Clight and Cminor). Other
stages just have the size of each variable and translate it to Init_space
when building the initial state.

File size: 3.0 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/toCminor.ma".
63include "Cminor/semantics.ma".
64
65example e1: finishes_with (repr I32 74) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
66normalize
67@refl
68qed.
69
70include "Cminor/toRTLabs.ma".
71include "RTLabs/semantics.ma".
72
73example e2: finishes_with (repr I32 74) ? (
74do p1 ← clight_to_cminor myprog;
75do p2 ← cminor_to_rtlabs p1;
76 exec_up_to RTLabs_fullexec p2 1000 [ ]).
77normalize
78@refl
79qed.
Note: See TracBrowser for help on using the repository browser.