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

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

Adjust pretty printers for change in program records, try a test of each.

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)
5  [〈〈ident_of_nat 0 (* src *), Any〉,
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 Any (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 )〉 ]
[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))
23           (Expr (Esizeof (Tarray Any (Tint I8 Unsigned ) 5))
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))
[758]40                       (Tarray Any (Tint I8 Unsigned ) 5))
[1226]41                     (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
[965]42                     (Tpointer Any (Tint I8 Unsigned ))))
[758]43                   (Tint I8 Unsigned ))) (Tint I32 Signed  )))
44               (Tint I32 Signed  ))) (Tint I8 Unsigned )))
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.