Changeset 978 for src/Clight/test
- Timestamp:
- Jun 16, 2011, 1:32:19 PM (10 years ago)
- Location:
- src/Clight/test
- Files:
-
- 1 added
- 3 deleted
- 2 moved
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/test/factorial.c.ma
r975 r978 8 8 (Ssequence 9 9 (Scall (Some expr (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed ))) 10 (Expr (Evar (ident_of_nat 0)) 11 (Tfunction Tnil (Tint I32 Signed ))) 10 (Expr (Evar (ident_of_nat 0)) (Tfunction Tnil (Tint I32 Signed ))) 12 11 []) 13 12 (Ssequence 14 13 (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed )) 15 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 16 (Ssequence 14 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 17 15 (Ssequence 18 16 (Sfor (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed )) 19 (Expr (Econst_int (repr 2)) (Tint I32 Signed ))) 20 (Expr (Ebinop Ole 21 (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed )) 17 (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed ))) 18 (Expr (Ebinop Ole (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed )) 22 19 (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed ))) 23 20 (Tint I32 Signed )) … … 25 22 (Expr (Ebinop Oadd 26 23 (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed )) 27 (Expr (Econst_int (repr1)) (Tint I32 Signed )))24 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 28 25 (Tint I32 Signed ))) 29 26 (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed )) … … 33 30 (Tint I32 Signed ))) 34 31 ) 35 Sskip) 36 (Sreturn (Some expr (Expr (Evar (ident_of_nat 3)) 37 (Tint I32 Signed ))))))) 32 (Sreturn (Some expr (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed ))))))) 38 33 39 34 … … 44 39 . 45 40 46 example exec: finishes_with (repr 120) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr5)]).41 example exec: finishes_with (repr I32 120) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 5)]). 47 42 normalize (* you can examine the result here *) 48 43 @refl qed. -
src/Clight/test/switcher.c.ma
r975 r978 9 9 (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )) 10 10 (Expr (Ecast (Tint I8 Unsigned ) 11 (Expr (Econst_int (repr0)) (Tint I32 Signed )))11 (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed ))) 12 12 (Tint I8 Unsigned ))) 13 13 (Ssequence … … 17 17 []) 18 18 (Sswitch (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed )) ( 19 (LScase (repr1)19 (LScase I32 (repr ? 1) 20 20 Sbreak 21 (LScase (repr3)21 (LScase I32 (repr ? 3) 22 22 (Ssequence 23 23 (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )) … … 27 27 (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))) 28 28 (Tint I32 Signed )) 29 (Expr (Econst_int (repr1)) (Tint I32 Signed )))29 (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed ))) 30 30 (Tint I32 Signed ))) (Tint I8 Unsigned ))) 31 31 Sbreak) 32 (LScase (repr5)32 (LScase I32 (repr ? 5) 33 33 (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )) 34 34 (Expr (Ecast (Tint I8 Unsigned ) … … 37 37 (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))) 38 38 (Tint I32 Signed )) 39 (Expr (Econst_int (repr2)) (Tint I32 Signed )))39 (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed ))) 40 40 (Tint I32 Signed ))) (Tint I8 Unsigned ))) 41 (LScase (repr7)41 (LScase I32 (repr ? 7) 42 42 (Ssequence 43 43 (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )) … … 47 47 (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))) 48 48 (Tint I32 Signed )) 49 (Expr (Econst_int (repr3)) (Tint I32 Signed )))49 (Expr (Econst_int I32 (repr ? 3)) (Tint I32 Signed ))) 50 50 (Tint I32 Signed ))) (Tint I8 Unsigned ))) 51 51 Sbreak) … … 57 57 (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))) 58 58 (Tint I32 Signed )) 59 (Expr (Econst_int (repr 16)) (Tint I32 Signed ))) 60 (Tint I32 Signed ))) (Tint I8 Unsigned )))))))) 59 (Expr (Econst_int I32 (repr ? 16)) 60 (Tint I32 Signed ))) (Tint I32 Signed ))) 61 (Tint I8 Unsigned )))))))) 61 62 ))) 62 63 (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed ) … … 71 72 . 72 73 73 example exec0: finishes_with (repr 16) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr0)]).74 example exec0: finishes_with (repr I32 16) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 0)]). 74 75 normalize (* you can examine the result here *) 75 76 @refl qed. 76 77 77 example exec1: finishes_with (repr 0) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr1)]).78 example exec1: finishes_with (repr I32 0) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 1)]). 78 79 normalize (* you can examine the result here *) 79 80 @refl qed. 80 81 81 example exec3: finishes_with (repr 1) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr3)]).82 example exec3: finishes_with (repr I32 1) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 3)]). 82 83 normalize (* you can examine the result here *) 83 84 @refl qed. 84 85 85 example exec5: finishes_with (repr 5) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr5)]).86 example exec5: finishes_with (repr I32 5) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 5)]). 86 87 normalize (* you can examine the result here *) 87 88 @refl qed. 88 89 89 example exec7: finishes_with (repr 3) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr7)]).90 example exec7: finishes_with (repr I32 3) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 7)]). 90 91 normalize (* you can examine the result here *) 91 92 @refl qed.
Note: See TracChangeset
for help on using the changeset viewer.