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

Last change on this file since 2176 was 2176, checked in by campbell, 7 years ago

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File size: 2.6 KB
Line 
1include "Clight/Cexec.ma".
2include "common/Animation.ma".
3
4definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
5  [〈〈ident_of_nat 0 (* src *), XData〉,
6     〈[(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ;
7        (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 8)) ;
8        (Init_int8 (repr I8 4)) ], (Tarray (Tint I8 Unsigned ) 5)〉〉]
9  [〈ident_of_nat 1 (* main *), CL_Internal (
10     mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 2, (Tint I32 Signed  )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ]
11       (Ssequence
12       (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
13         (Expr (Ecast (Tint I8 Unsigned )
14           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
15           (Tint I8 Unsigned )))
16       (Ssequence
17       (Sfor (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
18               (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
19         (Expr (Ebinop Olt
20           (Expr (Ecast (Tint I32 Unsigned)
21             (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
22             (Tint I32 Unsigned))
23           (Expr (Esizeof (Tarray (Tint I8 Unsigned ) 5))
24             (Tint I32 Unsigned))) (Tint I32 Signed  ))
25         (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
26           (Expr (Ebinop Oadd
27             (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
28             (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
29             (Tint I32 Signed  )))
30         (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
31           (Expr (Ecast (Tint I8 Unsigned )
32             (Expr (Ebinop Oadd
33               (Expr (Ecast (Tint I32 Signed  )
34                 (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
35                 (Tint I32 Signed  ))
36               (Expr (Ecast (Tint I32 Signed  )
37                 (Expr (Ederef
38                   (Expr (Ebinop Oadd
39                     (Expr (Evar (ident_of_nat 0))
40                       (Tarray (Tint I8 Unsigned ) 5))
41                     (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
42                     (Tpointer (Tint I8 Unsigned )))) (Tint I8 Unsigned )))
43                 (Tint I32 Signed  ))) (Tint I32 Signed  )))
44             (Tint I8 Unsigned )))
45       )
46       (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
47                             (Expr (Evar (ident_of_nat 3))
48                               (Tint I8 Unsigned ))) (Tint I32 Signed  ))))))
49     
50     
51     
52   )〉]
53  (ident_of_nat 1)
54 
55.
56
57(*
58example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
59normalize  (* you can examine the result here *)
60*)
Note: See TracBrowser for help on using the repository browser.