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

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

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

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