Changeset 717
- Timestamp:
- Mar 29, 2011, 5:54:36 PM (9 years ago)
- Location:
- src/Clight
- Files:
-
- 5 added
- 4 deleted
- 5 edited
-
Csem.ma (modified) (1 diff)
-
test/duff.ma (modified) (4 diffs)
-
test/factorial.ma (modified) (1 diff)
-
test/funptr.ma (deleted)
-
test/insertsort.ma (added)
-
test/io.c.ma (deleted)
-
test/io.ma (added)
-
test/io2.c.ma (deleted)
-
test/io2.ma (added)
-
test/memorymodel.ma (modified) (2 diffs)
-
test/search.c (added)
-
test/search.ma (added)
-
test/transform1.ma (modified) (2 diffs)
-
test/trivial.ma (deleted)
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/Csem.ma
r700 r717 183 183 match v1 with 184 184 [ Vint n1 ⇒ match v2 with 185 [ Vint n2 ⇒ Some ? (Vint (\snd (split ? wordsize wordsize (multiplication ? n1 n2)))) 185 [ Vint n2 ⇒ Some ? (Vint (mul n1 n2)) 186 (* [ Vint n2 ⇒ Some ? (Vint (\snd (split ? wordsize wordsize (multiplication ? n1 n2))))*) 186 187 | _ ⇒ None ? ] 187 188 | _ ⇒ None ? ] -
src/Clight/test/duff.ma
r415 r717 1 include " Animation.ma".1 include "Clight/Animation.ma". 2 2 3 (* This definition takes a long time to be accepted. *) 4 5 ndefinition myprog := mk_program fundef type 6 [mk_pair ?? (succ_pos_of_nat 132 (* copy *)) (Internal ( 7 mk_function Tvoid [mk_pair ?? (succ_pos_of_nat 151) (Tpointer Any (Tint I16 Signed )); mk_pair ?? (succ_pos_of_nat 152) (Tpointer Any (Tint I16 Signed )); mk_pair ?? (succ_pos_of_nat 153) (Tint I32 Signed )] [mk_pair ?? (succ_pos_of_nat 133) (Tint I32 Signed ); mk_pair ?? (succ_pos_of_nat 134) (Tint I32 Signed ); mk_pair ?? (succ_pos_of_nat 135) (Tpointer Any (Tint I16 Signed )); mk_pair ?? (succ_pos_of_nat 136) (Tpointer Any (Tint I16 Signed )); mk_pair ?? (succ_pos_of_nat 137) (Tpointer Any (Tint I16 Signed )); mk_pair ?? (succ_pos_of_nat 138) (Tpointer Any (Tint I16 Signed )); mk_pair ?? (succ_pos_of_nat 139) (Tpointer Any (Tint I16 Signed )); mk_pair ?? (succ_pos_of_nat 140) (Tpointer Any (Tint I16 Signed )); mk_pair ?? (succ_pos_of_nat 141) (Tpointer Any (Tint I16 Signed )); mk_pair ?? (succ_pos_of_nat 142) (Tpointer Any (Tint I16 Signed )); mk_pair ?? (succ_pos_of_nat 143) (Tpointer Any (Tint I16 Signed )); mk_pair ?? (succ_pos_of_nat 144) (Tpointer Any (Tint I16 Signed )); mk_pair ?? (succ_pos_of_nat 145) (Tpointer Any (Tint I16 Signed )); mk_pair ?? (succ_pos_of_nat 146) (Tpointer Any (Tint I16 Signed )); mk_pair ?? (succ_pos_of_nat 147) (Tpointer Any (Tint I16 Signed )); mk_pair ?? (succ_pos_of_nat 148) (Tpointer Any (Tint I16 Signed )); mk_pair ?? (succ_pos_of_nat 149) (Tpointer Any (Tint I16 Signed )); mk_pair ?? (succ_pos_of_nat 150) (Tpointer Any (Tint I16 Signed ))] 8 (Ssequence 9 (Sassign (Expr (Evar (succ_pos_of_nat 133)) (Tint I32 Signed )) 10 (Expr (Ebinop Odiv 11 (Expr (Ebinop Oadd 12 (Expr (Evar (succ_pos_of_nat 153)) (Tint I32 Signed )) 13 (Expr (Econst_int (repr 7)) (Tint I32 Signed ))) 14 (Tint I32 Signed )) 15 (Expr (Econst_int (repr 8)) (Tint I32 Signed ))) 16 (Tint I32 Signed ))) 17 (Sswitch (Expr (Ebinop Omod 18 (Expr (Evar (succ_pos_of_nat 153)) (Tint I32 Signed )) 19 (Expr (Econst_int (repr 8)) (Tint I32 Signed ))) 20 (Tint I32 Signed )) ( 21 (LScase (repr 0) 22 (Slabel (succ_pos_of_nat 154) 23 (Ssequence 24 (Ssequence 25 (Sassign (Expr (Evar (succ_pos_of_nat 149)) 3 definition myprog := mk_program fundef type 4 [〈succ_pos_of_nat 0 (* copy *), Internal ( 5 mk_function Tvoid [〈succ_pos_of_nat 19, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 20, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 21, (Tint I32 Signed )〉 ] [〈succ_pos_of_nat 1, (Tint I32 Signed )〉 ; 〈succ_pos_of_nat 2, (Tint I32 Signed )〉 ; 〈succ_pos_of_nat 3, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 4, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 5, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 6, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 7, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 8, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 9, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 10, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 11, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 12, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 13, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 14, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 15, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 16, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 17, (Tpointer Any (Tint I16 Signed ))〉 ; 〈succ_pos_of_nat 18, (Tpointer Any (Tint I16 Signed ))〉 ] 6 (Ssequence 7 (Sassign (Expr (Evar (succ_pos_of_nat 1)) (Tint I32 Signed )) 8 (Expr (Ebinop Odiv 9 (Expr (Ebinop Oadd 10 (Expr (Evar (succ_pos_of_nat 21)) (Tint I32 Signed )) 11 (Expr (Econst_int (repr 7)) (Tint I32 Signed ))) 12 (Tint I32 Signed )) 13 (Expr (Econst_int (repr 8)) (Tint I32 Signed ))) 14 (Tint I32 Signed ))) 15 (Sswitch (Expr (Ebinop Omod 16 (Expr (Evar (succ_pos_of_nat 21)) (Tint I32 Signed )) 17 (Expr (Econst_int (repr 8)) (Tint I32 Signed ))) 18 (Tint I32 Signed )) ( 19 (LScase (repr 0) 20 (Slabel (succ_pos_of_nat 22) 21 (Ssequence 22 (Ssequence 23 (Sassign (Expr (Evar (succ_pos_of_nat 17)) 24 (Tpointer Any (Tint I16 Signed ))) 25 (Expr (Evar (succ_pos_of_nat 19)) 26 (Tpointer Any (Tint I16 Signed )))) 27 (Sassign (Expr (Evar (succ_pos_of_nat 19)) 28 (Tpointer Any (Tint I16 Signed ))) 29 (Expr (Ebinop Oadd 30 (Expr (Evar (succ_pos_of_nat 17)) 31 (Tpointer Any (Tint I16 Signed ))) 32 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 33 (Tpointer Any (Tint I16 Signed ))))) 34 (Ssequence 35 (Ssequence 36 (Sassign (Expr (Evar (succ_pos_of_nat 18)) 37 (Tpointer Any (Tint I16 Signed ))) 38 (Expr (Evar (succ_pos_of_nat 20)) 39 (Tpointer Any (Tint I16 Signed )))) 40 (Sassign (Expr (Evar (succ_pos_of_nat 20)) 41 (Tpointer Any (Tint I16 Signed ))) 42 (Expr (Ebinop Oadd 43 (Expr (Evar (succ_pos_of_nat 18)) 44 (Tpointer Any (Tint I16 Signed ))) 45 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 46 (Tpointer Any (Tint I16 Signed ))))) 47 (Sassign (Expr (Ederef 48 (Expr (Evar (succ_pos_of_nat 17)) 49 (Tpointer Any (Tint I16 Signed )))) 50 (Tint I16 Signed )) 51 (Expr (Ederef 52 (Expr (Evar (succ_pos_of_nat 18)) 53 (Tpointer Any (Tint I16 Signed )))) (Tint I16 Signed )))))) 54 (LScase (repr 7) 55 (Ssequence 56 (Sassign (Expr (Evar (succ_pos_of_nat 15)) 57 (Tpointer Any (Tint I16 Signed ))) 58 (Expr (Evar (succ_pos_of_nat 19)) 59 (Tpointer Any (Tint I16 Signed )))) 60 (Ssequence 61 (Sassign (Expr (Evar (succ_pos_of_nat 19)) 62 (Tpointer Any (Tint I16 Signed ))) 63 (Expr (Ebinop Oadd 64 (Expr (Evar (succ_pos_of_nat 15)) 65 (Tpointer Any (Tint I16 Signed ))) 66 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 67 (Tpointer Any (Tint I16 Signed )))) 68 (Ssequence 69 (Sassign (Expr (Evar (succ_pos_of_nat 16)) 70 (Tpointer Any (Tint I16 Signed ))) 71 (Expr (Evar (succ_pos_of_nat 20)) 72 (Tpointer Any (Tint I16 Signed )))) 73 (Ssequence 74 (Sassign (Expr (Evar (succ_pos_of_nat 20)) 75 (Tpointer Any (Tint I16 Signed ))) 76 (Expr (Ebinop Oadd 77 (Expr (Evar (succ_pos_of_nat 16)) 78 (Tpointer Any (Tint I16 Signed ))) 79 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 80 (Tpointer Any (Tint I16 Signed )))) 81 (Sassign (Expr (Ederef 82 (Expr (Evar (succ_pos_of_nat 15)) 83 (Tpointer Any (Tint I16 Signed )))) 84 (Tint I16 Signed )) 85 (Expr (Ederef 86 (Expr (Evar (succ_pos_of_nat 16)) 87 (Tpointer Any (Tint I16 Signed )))) (Tint I16 Signed ))))))) 88 (LScase (repr 6) 89 (Ssequence 90 (Sassign (Expr (Evar (succ_pos_of_nat 13)) 91 (Tpointer Any (Tint I16 Signed ))) 92 (Expr (Evar (succ_pos_of_nat 19)) 93 (Tpointer Any (Tint I16 Signed )))) 94 (Ssequence 95 (Sassign (Expr (Evar (succ_pos_of_nat 19)) 96 (Tpointer Any (Tint I16 Signed ))) 97 (Expr (Ebinop Oadd 98 (Expr (Evar (succ_pos_of_nat 13)) 26 99 (Tpointer Any (Tint I16 Signed ))) 27 (Expr (Evar (succ_pos_of_nat 151)) 28 (Tpointer Any (Tint I16 Signed )))) 29 (Sassign (Expr (Evar (succ_pos_of_nat 151)) 100 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 101 (Tpointer Any (Tint I16 Signed )))) 102 (Ssequence 103 (Sassign (Expr (Evar (succ_pos_of_nat 14)) 104 (Tpointer Any (Tint I16 Signed ))) 105 (Expr (Evar (succ_pos_of_nat 20)) 106 (Tpointer Any (Tint I16 Signed )))) 107 (Ssequence 108 (Sassign (Expr (Evar (succ_pos_of_nat 20)) 109 (Tpointer Any (Tint I16 Signed ))) 110 (Expr (Ebinop Oadd 111 (Expr (Evar (succ_pos_of_nat 14)) 30 112 (Tpointer Any (Tint I16 Signed ))) 31 (Expr (Ebinop Oadd 32 (Expr (Evar (succ_pos_of_nat 149)) 33 (Tpointer Any (Tint I16 Signed ))) 34 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 35 (Tpointer Any (Tint I16 Signed ))))) 36 (Ssequence 37 (Ssequence 38 (Sassign (Expr (Evar (succ_pos_of_nat 150)) 39 (Tpointer Any (Tint I16 Signed ))) 40 (Expr (Evar (succ_pos_of_nat 152)) 41 (Tpointer Any (Tint I16 Signed )))) 42 (Sassign (Expr (Evar (succ_pos_of_nat 152)) 43 (Tpointer Any (Tint I16 Signed ))) 44 (Expr (Ebinop Oadd 45 (Expr (Evar (succ_pos_of_nat 150)) 46 (Tpointer Any (Tint I16 Signed ))) 47 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 48 (Tpointer Any (Tint I16 Signed ))))) 49 (Sassign (Expr (Ederef 50 (Expr (Evar (succ_pos_of_nat 149)) 113 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 114 (Tpointer Any (Tint I16 Signed )))) 115 (Sassign (Expr (Ederef 116 (Expr (Evar (succ_pos_of_nat 13)) 117 (Tpointer Any (Tint I16 Signed )))) 118 (Tint I16 Signed )) 119 (Expr (Ederef 120 (Expr (Evar (succ_pos_of_nat 14)) 121 (Tpointer Any (Tint I16 Signed )))) 122 (Tint I16 Signed ))))))) 123 (LScase (repr 5) 124 (Ssequence 125 (Sassign (Expr (Evar (succ_pos_of_nat 11)) 126 (Tpointer Any (Tint I16 Signed ))) 127 (Expr (Evar (succ_pos_of_nat 19)) 128 (Tpointer Any (Tint I16 Signed )))) 129 (Ssequence 130 (Sassign (Expr (Evar (succ_pos_of_nat 19)) 131 (Tpointer Any (Tint I16 Signed ))) 132 (Expr (Ebinop Oadd 133 (Expr (Evar (succ_pos_of_nat 11)) 134 (Tpointer Any (Tint I16 Signed ))) 135 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 136 (Tpointer Any (Tint I16 Signed )))) 137 (Ssequence 138 (Sassign (Expr (Evar (succ_pos_of_nat 12)) 139 (Tpointer Any (Tint I16 Signed ))) 140 (Expr (Evar (succ_pos_of_nat 20)) 141 (Tpointer Any (Tint I16 Signed )))) 142 (Ssequence 143 (Sassign (Expr (Evar (succ_pos_of_nat 20)) 144 (Tpointer Any (Tint I16 Signed ))) 145 (Expr (Ebinop Oadd 146 (Expr (Evar (succ_pos_of_nat 12)) 147 (Tpointer Any (Tint I16 Signed ))) 148 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 149 (Tpointer Any (Tint I16 Signed )))) 150 (Sassign (Expr (Ederef 151 (Expr (Evar (succ_pos_of_nat 11)) 152 (Tpointer Any (Tint I16 Signed )))) 153 (Tint I16 Signed )) 154 (Expr (Ederef 155 (Expr (Evar (succ_pos_of_nat 12)) 51 156 (Tpointer Any (Tint I16 Signed )))) 52 (Tint I16 Signed )) 53 (Expr (Ederef 54 (Expr (Evar (succ_pos_of_nat 150)) 55 (Tpointer Any (Tint I16 Signed )))) (Tint I16 Signed )))))) 56 (LScase (repr 7) 57 (Ssequence 58 (Sassign (Expr (Evar (succ_pos_of_nat 147)) 59 (Tpointer Any (Tint I16 Signed ))) 60 (Expr (Evar (succ_pos_of_nat 151)) 61 (Tpointer Any (Tint I16 Signed )))) 62 (Ssequence 63 (Sassign (Expr (Evar (succ_pos_of_nat 151)) 64 (Tpointer Any (Tint I16 Signed ))) 65 (Expr (Ebinop Oadd 66 (Expr (Evar (succ_pos_of_nat 147)) 67 (Tpointer Any (Tint I16 Signed ))) 68 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 69 (Tpointer Any (Tint I16 Signed )))) 70 (Ssequence 71 (Sassign (Expr (Evar (succ_pos_of_nat 148)) 72 (Tpointer Any (Tint I16 Signed ))) 73 (Expr (Evar (succ_pos_of_nat 152)) 74 (Tpointer Any (Tint I16 Signed )))) 75 (Ssequence 76 (Sassign (Expr (Evar (succ_pos_of_nat 152)) 77 (Tpointer Any (Tint I16 Signed ))) 78 (Expr (Ebinop Oadd 79 (Expr (Evar (succ_pos_of_nat 148)) 80 (Tpointer Any (Tint I16 Signed ))) 81 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 82 (Tpointer Any (Tint I16 Signed )))) 83 (Sassign (Expr (Ederef 84 (Expr (Evar (succ_pos_of_nat 147)) 157 (Tint I16 Signed ))))))) 158 (LScase (repr 4) 159 (Ssequence 160 (Sassign (Expr (Evar (succ_pos_of_nat 9)) 161 (Tpointer Any (Tint I16 Signed ))) 162 (Expr (Evar (succ_pos_of_nat 19)) 163 (Tpointer Any (Tint I16 Signed )))) 164 (Ssequence 165 (Sassign (Expr (Evar (succ_pos_of_nat 19)) 166 (Tpointer Any (Tint I16 Signed ))) 167 (Expr (Ebinop Oadd 168 (Expr (Evar (succ_pos_of_nat 9)) 169 (Tpointer Any (Tint I16 Signed ))) 170 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 171 (Tpointer Any (Tint I16 Signed )))) 172 (Ssequence 173 (Sassign (Expr (Evar (succ_pos_of_nat 10)) 174 (Tpointer Any (Tint I16 Signed ))) 175 (Expr (Evar (succ_pos_of_nat 20)) 176 (Tpointer Any (Tint I16 Signed )))) 177 (Ssequence 178 (Sassign (Expr (Evar (succ_pos_of_nat 20)) 179 (Tpointer Any (Tint I16 Signed ))) 180 (Expr (Ebinop Oadd 181 (Expr (Evar (succ_pos_of_nat 10)) 182 (Tpointer Any (Tint I16 Signed ))) 183 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 184 (Tpointer Any (Tint I16 Signed )))) 185 (Sassign (Expr (Ederef 186 (Expr (Evar (succ_pos_of_nat 9)) 187 (Tpointer Any (Tint I16 Signed )))) 188 (Tint I16 Signed )) 189 (Expr (Ederef 190 (Expr (Evar (succ_pos_of_nat 10)) 85 191 (Tpointer Any (Tint I16 Signed )))) 86 (Tint I16 Signed )) 87 (Expr (Ederef 88 (Expr (Evar (succ_pos_of_nat 148)) 89 (Tpointer Any (Tint I16 Signed )))) (Tint I16 Signed ))))))) 90 (LScase (repr 6) 91 (Ssequence 92 (Sassign (Expr (Evar (succ_pos_of_nat 145)) 93 (Tpointer Any (Tint I16 Signed ))) 94 (Expr (Evar (succ_pos_of_nat 151)) 95 (Tpointer Any (Tint I16 Signed )))) 96 (Ssequence 97 (Sassign (Expr (Evar (succ_pos_of_nat 151)) 98 (Tpointer Any (Tint I16 Signed ))) 99 (Expr (Ebinop Oadd 100 (Expr (Evar (succ_pos_of_nat 145)) 101 (Tpointer Any (Tint I16 Signed ))) 102 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 103 (Tpointer Any (Tint I16 Signed )))) 104 (Ssequence 105 (Sassign (Expr (Evar (succ_pos_of_nat 146)) 106 (Tpointer Any (Tint I16 Signed ))) 107 (Expr (Evar (succ_pos_of_nat 152)) 108 (Tpointer Any (Tint I16 Signed )))) 109 (Ssequence 110 (Sassign (Expr (Evar (succ_pos_of_nat 152)) 111 (Tpointer Any (Tint I16 Signed ))) 112 (Expr (Ebinop Oadd 113 (Expr (Evar (succ_pos_of_nat 146)) 114 (Tpointer Any (Tint I16 Signed ))) 115 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 116 (Tpointer Any (Tint I16 Signed )))) 117 (Sassign (Expr (Ederef 118 (Expr (Evar (succ_pos_of_nat 145)) 192 (Tint I16 Signed ))))))) 193 (LScase (repr 3) 194 (Ssequence 195 (Sassign (Expr (Evar (succ_pos_of_nat 7)) 196 (Tpointer Any (Tint I16 Signed ))) 197 (Expr (Evar (succ_pos_of_nat 19)) 198 (Tpointer Any (Tint I16 Signed )))) 199 (Ssequence 200 (Sassign (Expr (Evar (succ_pos_of_nat 19)) 201 (Tpointer Any (Tint I16 Signed ))) 202 (Expr (Ebinop Oadd 203 (Expr (Evar (succ_pos_of_nat 7)) 204 (Tpointer Any (Tint I16 Signed ))) 205 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 206 (Tpointer Any (Tint I16 Signed )))) 207 (Ssequence 208 (Sassign (Expr (Evar (succ_pos_of_nat 8)) 209 (Tpointer Any (Tint I16 Signed ))) 210 (Expr (Evar (succ_pos_of_nat 20)) 211 (Tpointer Any (Tint I16 Signed )))) 212 (Ssequence 213 (Sassign (Expr (Evar (succ_pos_of_nat 20)) 214 (Tpointer Any (Tint I16 Signed ))) 215 (Expr (Ebinop Oadd 216 (Expr (Evar (succ_pos_of_nat 8)) 217 (Tpointer Any (Tint I16 Signed ))) 218 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 219 (Tpointer Any (Tint I16 Signed )))) 220 (Sassign (Expr (Ederef 221 (Expr (Evar (succ_pos_of_nat 7)) 222 (Tpointer Any (Tint I16 Signed )))) 223 (Tint I16 Signed )) 224 (Expr (Ederef 225 (Expr (Evar (succ_pos_of_nat 8)) 119 226 (Tpointer Any (Tint I16 Signed )))) 120 (Tint I16 Signed )) 121 (Expr (Ederef 122 (Expr (Evar (succ_pos_of_nat 146)) 123 (Tpointer Any (Tint I16 Signed )))) (Tint I16 Signed ))))))) 124 (LScase (repr 5) 125 (Ssequence 126 (Sassign (Expr (Evar (succ_pos_of_nat 143)) 127 (Tpointer Any (Tint I16 Signed ))) 128 (Expr (Evar (succ_pos_of_nat 151)) 129 (Tpointer Any (Tint I16 Signed )))) 130 (Ssequence 131 (Sassign (Expr (Evar (succ_pos_of_nat 151)) 132 (Tpointer Any (Tint I16 Signed ))) 133 (Expr (Ebinop Oadd 134 (Expr (Evar (succ_pos_of_nat 143)) 135 (Tpointer Any (Tint I16 Signed ))) 136 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 137 (Tpointer Any (Tint I16 Signed )))) 138 (Ssequence 139 (Sassign (Expr (Evar (succ_pos_of_nat 144)) 140 (Tpointer Any (Tint I16 Signed ))) 141 (Expr (Evar (succ_pos_of_nat 152)) 142 (Tpointer Any (Tint I16 Signed )))) 143 (Ssequence 144 (Sassign (Expr (Evar (succ_pos_of_nat 152)) 145 (Tpointer Any (Tint I16 Signed ))) 146 (Expr (Ebinop Oadd 147 (Expr (Evar (succ_pos_of_nat 144)) 148 (Tpointer Any (Tint I16 Signed ))) 149 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 150 (Tpointer Any (Tint I16 Signed )))) 151 (Sassign (Expr (Ederef 152 (Expr (Evar (succ_pos_of_nat 143)) 227 (Tint I16 Signed ))))))) 228 (LScase (repr 2) 229 (Ssequence 230 (Sassign (Expr (Evar (succ_pos_of_nat 5)) 231 (Tpointer Any (Tint I16 Signed ))) 232 (Expr (Evar (succ_pos_of_nat 19)) 233 (Tpointer Any (Tint I16 Signed )))) 234 (Ssequence 235 (Sassign (Expr (Evar (succ_pos_of_nat 19)) 236 (Tpointer Any (Tint I16 Signed ))) 237 (Expr (Ebinop Oadd 238 (Expr (Evar (succ_pos_of_nat 5)) 239 (Tpointer Any (Tint I16 Signed ))) 240 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 241 (Tpointer Any (Tint I16 Signed )))) 242 (Ssequence 243 (Sassign (Expr (Evar (succ_pos_of_nat 6)) 244 (Tpointer Any (Tint I16 Signed ))) 245 (Expr (Evar (succ_pos_of_nat 20)) 246 (Tpointer Any (Tint I16 Signed )))) 247 (Ssequence 248 (Sassign (Expr (Evar (succ_pos_of_nat 20)) 249 (Tpointer Any (Tint I16 Signed ))) 250 (Expr (Ebinop Oadd 251 (Expr (Evar (succ_pos_of_nat 6)) 252 (Tpointer Any (Tint I16 Signed ))) 253 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 254 (Tpointer Any (Tint I16 Signed )))) 255 (Sassign (Expr (Ederef 256 (Expr (Evar (succ_pos_of_nat 5)) 257 (Tpointer Any (Tint I16 Signed )))) 258 (Tint I16 Signed )) 259 (Expr (Ederef 260 (Expr (Evar (succ_pos_of_nat 6)) 153 261 (Tpointer Any (Tint I16 Signed )))) 154 (Tint I16 Signed )) 155 (Expr (Ederef 156 (Expr (Evar (succ_pos_of_nat 144)) 157 (Tpointer Any (Tint I16 Signed )))) 158 (Tint I16 Signed ))))))) 159 (LScase (repr 4) 160 (Ssequence 161 (Sassign (Expr (Evar (succ_pos_of_nat 141)) 162 (Tpointer Any (Tint I16 Signed ))) 163 (Expr (Evar (succ_pos_of_nat 151)) 164 (Tpointer Any (Tint I16 Signed )))) 165 (Ssequence 166 (Sassign (Expr (Evar (succ_pos_of_nat 151)) 167 (Tpointer Any (Tint I16 Signed ))) 168 (Expr (Ebinop Oadd 169 (Expr (Evar (succ_pos_of_nat 141)) 170 (Tpointer Any (Tint I16 Signed ))) 171 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 172 (Tpointer Any (Tint I16 Signed )))) 173 (Ssequence 174 (Sassign (Expr (Evar (succ_pos_of_nat 142)) 175 (Tpointer Any (Tint I16 Signed ))) 176 (Expr (Evar (succ_pos_of_nat 152)) 177 (Tpointer Any (Tint I16 Signed )))) 178 (Ssequence 179 (Sassign (Expr (Evar (succ_pos_of_nat 152)) 180 (Tpointer Any (Tint I16 Signed ))) 181 (Expr (Ebinop Oadd 182 (Expr (Evar (succ_pos_of_nat 142)) 183 (Tpointer Any (Tint I16 Signed ))) 184 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 185 (Tpointer Any (Tint I16 Signed )))) 186 (Sassign (Expr (Ederef 187 (Expr (Evar (succ_pos_of_nat 141)) 262 (Tint I16 Signed ))))))) 263 (LScase (repr 1) 264 (Ssequence 265 (Sassign (Expr (Evar (succ_pos_of_nat 3)) 266 (Tpointer Any (Tint I16 Signed ))) 267 (Expr (Evar (succ_pos_of_nat 19)) 268 (Tpointer Any (Tint I16 Signed )))) 269 (Ssequence 270 (Sassign (Expr (Evar (succ_pos_of_nat 19)) 271 (Tpointer Any (Tint I16 Signed ))) 272 (Expr (Ebinop Oadd 273 (Expr (Evar (succ_pos_of_nat 3)) 274 (Tpointer Any (Tint I16 Signed ))) 275 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 276 (Tpointer Any (Tint I16 Signed )))) 277 (Ssequence 278 (Sassign (Expr (Evar (succ_pos_of_nat 4)) 279 (Tpointer Any (Tint I16 Signed ))) 280 (Expr (Evar (succ_pos_of_nat 20)) 281 (Tpointer Any (Tint I16 Signed )))) 282 (Ssequence 283 (Sassign (Expr (Evar (succ_pos_of_nat 20)) 284 (Tpointer Any (Tint I16 Signed ))) 285 (Expr (Ebinop Oadd 286 (Expr (Evar (succ_pos_of_nat 4)) 287 (Tpointer Any (Tint I16 Signed ))) 288 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 289 (Tpointer Any (Tint I16 Signed )))) 290 (Ssequence 291 (Sassign (Expr (Ederef 292 (Expr (Evar (succ_pos_of_nat 3)) 293 (Tpointer Any (Tint I16 Signed )))) 294 (Tint I16 Signed )) 295 (Expr (Ederef 296 (Expr (Evar (succ_pos_of_nat 4)) 188 297 (Tpointer Any (Tint I16 Signed )))) 189 (Tint I16 Signed )) 190 (Expr (Ederef 191 (Expr (Evar (succ_pos_of_nat 142)) 192 (Tpointer Any (Tint I16 Signed )))) 193 (Tint I16 Signed ))))))) 194 (LScase (repr 3) 195 (Ssequence 196 (Sassign (Expr (Evar (succ_pos_of_nat 139)) 197 (Tpointer Any (Tint I16 Signed ))) 198 (Expr (Evar (succ_pos_of_nat 151)) 199 (Tpointer Any (Tint I16 Signed )))) 200 (Ssequence 201 (Sassign (Expr (Evar (succ_pos_of_nat 151)) 202 (Tpointer Any (Tint I16 Signed ))) 203 (Expr (Ebinop Oadd 204 (Expr (Evar (succ_pos_of_nat 139)) 205 (Tpointer Any (Tint I16 Signed ))) 206 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 207 (Tpointer Any (Tint I16 Signed )))) 208 (Ssequence 209 (Sassign (Expr (Evar (succ_pos_of_nat 140)) 210 (Tpointer Any (Tint I16 Signed ))) 211 (Expr (Evar (succ_pos_of_nat 152)) 212 (Tpointer Any (Tint I16 Signed )))) 213 (Ssequence 214 (Sassign (Expr (Evar (succ_pos_of_nat 152)) 215 (Tpointer Any (Tint I16 Signed ))) 216 (Expr (Ebinop Oadd 217 (Expr (Evar (succ_pos_of_nat 140)) 218 (Tpointer Any (Tint I16 Signed ))) 219 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 220 (Tpointer Any (Tint I16 Signed )))) 221 (Sassign (Expr (Ederef 222 (Expr (Evar (succ_pos_of_nat 139)) 223 (Tpointer Any (Tint I16 Signed )))) 224 (Tint I16 Signed )) 225 (Expr (Ederef 226 (Expr (Evar (succ_pos_of_nat 140)) 227 (Tpointer Any (Tint I16 Signed )))) 228 (Tint I16 Signed ))))))) 229 (LScase (repr 2) 230 (Ssequence 231 (Sassign (Expr (Evar (succ_pos_of_nat 137)) 232 (Tpointer Any (Tint I16 Signed ))) 233 (Expr (Evar (succ_pos_of_nat 151)) 234 (Tpointer Any (Tint I16 Signed )))) 235 (Ssequence 236 (Sassign (Expr (Evar (succ_pos_of_nat 151)) 237 (Tpointer Any (Tint I16 Signed ))) 238 (Expr (Ebinop Oadd 239 (Expr (Evar (succ_pos_of_nat 137)) 240 (Tpointer Any (Tint I16 Signed ))) 241 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 242 (Tpointer Any (Tint I16 Signed )))) 243 (Ssequence 244 (Sassign (Expr (Evar (succ_pos_of_nat 138)) 245 (Tpointer Any (Tint I16 Signed ))) 246 (Expr (Evar (succ_pos_of_nat 152)) 247 (Tpointer Any (Tint I16 Signed )))) 248 (Ssequence 249 (Sassign (Expr (Evar (succ_pos_of_nat 152)) 250 (Tpointer Any (Tint I16 Signed ))) 251 (Expr (Ebinop Oadd 252 (Expr (Evar (succ_pos_of_nat 138)) 253 (Tpointer Any (Tint I16 Signed ))) 254 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 255 (Tpointer Any (Tint I16 Signed )))) 256 (Sassign (Expr (Ederef 257 (Expr (Evar (succ_pos_of_nat 137)) 258 (Tpointer Any (Tint I16 Signed )))) 259 (Tint I16 Signed )) 260 (Expr (Ederef 261 (Expr (Evar (succ_pos_of_nat 138)) 262 (Tpointer Any (Tint I16 Signed )))) 263 (Tint I16 Signed ))))))) 264 (LScase (repr 1) 265 (Ssequence 266 (Sassign (Expr (Evar (succ_pos_of_nat 135)) 267 (Tpointer Any (Tint I16 Signed ))) 268 (Expr (Evar (succ_pos_of_nat 151)) 269 (Tpointer Any (Tint I16 Signed )))) 270 (Ssequence 271 (Sassign (Expr (Evar (succ_pos_of_nat 151)) 272 (Tpointer Any (Tint I16 Signed ))) 273 (Expr (Ebinop Oadd 274 (Expr (Evar (succ_pos_of_nat 135)) 275 (Tpointer Any (Tint I16 Signed ))) 276 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 277 (Tpointer Any (Tint I16 Signed )))) 278 (Ssequence 279 (Sassign (Expr (Evar (succ_pos_of_nat 136)) 280 (Tpointer Any (Tint I16 Signed ))) 281 (Expr (Evar (succ_pos_of_nat 152)) 282 (Tpointer Any (Tint I16 Signed )))) 283 (Ssequence 284 (Sassign (Expr (Evar (succ_pos_of_nat 152)) 285 (Tpointer Any (Tint I16 Signed ))) 286 (Expr (Ebinop Oadd 287 (Expr (Evar (succ_pos_of_nat 136)) 288 (Tpointer Any (Tint I16 Signed ))) 289 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 290 (Tpointer Any (Tint I16 Signed )))) 291 (Ssequence 292 (Sassign (Expr (Ederef 293 (Expr (Evar (succ_pos_of_nat 135)) 294 (Tpointer Any (Tint I16 Signed )))) 295 (Tint I16 Signed )) 296 (Expr (Ederef 297 (Expr (Evar (succ_pos_of_nat 136)) 298 (Tpointer Any (Tint I16 Signed )))) 299 (Tint I16 Signed ))) 300 (Ssequence 301 (Sassign (Expr (Evar (succ_pos_of_nat 134)) 302 (Tint I32 Signed )) 303 (Expr (Ebinop Osub 304 (Expr (Evar (succ_pos_of_nat 133)) 305 (Tint I32 Signed )) 306 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 307 (Tint I32 Signed ))) 308 (Ssequence 309 (Sassign (Expr (Evar (succ_pos_of_nat 133)) 310 (Tint I32 Signed )) 311 (Expr (Evar (succ_pos_of_nat 134)) 312 (Tint I32 Signed ))) 313 (Sifthenelse (Expr (Ebinop Ogt 314 (Expr (Evar (succ_pos_of_nat 134)) 315 (Tint I32 Signed )) 316 (Expr (Econst_int (repr 0)) 317 (Tint I32 Signed ))) 318 (Tint I32 Signed )) 319 (Sgoto (succ_pos_of_nat 154)) 320 Sskip)))))))) 321 (LSdefault 322 Sskip))))))))) 323 ))) 324 325 326 327 )); 328 mk_pair ?? (succ_pos_of_nat 155 (* main *)) (Internal ( 329 mk_function (Tint I32 Signed ) [] [mk_pair ?? (succ_pos_of_nat 156) (Tarray Any (Tint I16 Signed ) 3); mk_pair ?? (succ_pos_of_nat 157) (Tarray Any (Tint I16 Signed ) 3)] 298 (Tint I16 Signed ))) 299 (Ssequence 300 (Sassign (Expr (Evar (succ_pos_of_nat 2)) 301 (Tint I32 Signed )) 302 (Expr (Ebinop Osub 303 (Expr (Evar (succ_pos_of_nat 1)) 304 (Tint I32 Signed )) 305 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 306 (Tint I32 Signed ))) 307 (Ssequence 308 (Sassign (Expr (Evar (succ_pos_of_nat 1)) 309 (Tint I32 Signed )) 310 (Expr (Evar (succ_pos_of_nat 2)) 311 (Tint I32 Signed ))) 312 (Sifthenelse (Expr (Ebinop Ogt 313 (Expr (Evar (succ_pos_of_nat 2)) 314 (Tint I32 Signed )) 315 (Expr (Econst_int (repr 0)) 316 (Tint I32 Signed ))) 317 (Tint I32 Signed )) 318 (Sgoto (succ_pos_of_nat 22)) 319 Sskip)))))))) 320 (LSdefault 321 Sskip))))))))) 322 ))) 323 324 325 326 )〉; 327 〈succ_pos_of_nat 23 (* main *), Internal ( 328 mk_function (Tint I32 Signed ) [] [〈succ_pos_of_nat 24, (Tarray Any (Tint I16 Signed ) 3)〉 ; 〈succ_pos_of_nat 25, (Tarray Any (Tint I16 Signed ) 3)〉 ] 330 329 (Ssequence 331 330 (Sassign (Expr (Ederef 332 331 (Expr (Ebinop Oadd 333 (Expr (Evar (succ_pos_of_nat 156))332 (Expr (Evar (succ_pos_of_nat 24)) 334 333 (Tarray Any (Tint I16 Signed ) 3)) 335 334 (Expr (Econst_int (repr 0)) (Tint I32 Signed ))) … … 341 340 (Sassign (Expr (Ederef 342 341 (Expr (Ebinop Oadd 343 (Expr (Evar (succ_pos_of_nat 156))342 (Expr (Evar (succ_pos_of_nat 24)) 344 343 (Tarray Any (Tint I16 Signed ) 3)) 345 344 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) … … 351 350 (Sassign (Expr (Ederef 352 351 (Expr (Ebinop Oadd 353 (Expr (Evar (succ_pos_of_nat 156))352 (Expr (Evar (succ_pos_of_nat 24)) 354 353 (Tarray Any (Tint I16 Signed ) 3)) 355 354 (Expr (Econst_int (repr 2)) (Tint I32 Signed ))) … … 359 358 (Tint I16 Signed ))) 360 359 (Ssequence 361 (Scall (None ?) (Expr (Evar (succ_pos_of_nat 132))362 (Tfunction (Tcons (Tpointer Any (Tint I16 Signed )) (Tcons (Tpointer Any (Tint I16 Signed )) (Tcons (Tint I32 Signed ) Tnil))) Tvoid))363 [(Expr (Evar (succ_pos_of_nat 157))360 (Scall (None expr) (Expr (Evar (succ_pos_of_nat 0)) 361 (Tfunction (Tcons (Tpointer Any (Tint I16 Signed )) (Tcons (Tpointer Any (Tint I16 Signed )) (Tcons (Tint I32 Signed ) Tnil))) Tvoid)) 362 [(Expr (Evar (succ_pos_of_nat 25)) 364 363 (Tarray Any (Tint I16 Signed ) 3)); 365 (Expr (Evar (succ_pos_of_nat 156)) 366 (Tarray Any (Tint I16 Signed ) 3)); 364 (Expr (Evar (succ_pos_of_nat 24)) (Tarray Any (Tint I16 Signed ) 3)); 367 365 (Expr (Econst_int (repr 3)) (Tint I32 Signed ))]) 368 (Sreturn (Some ?(Expr (Ebinop Oadd369 (Expr (Ebinop Oadd370 (Expr (Ecast (Tint I32 Signed )371 (Expr (Ederef372 (Expr (Ebinop Oadd373 (Expr (Evar (succ_pos_of_nat 157))374 (Tarray Any (Tint I16 Signed ) 3))375 (Expr (Econst_int (repr 0))376 (Tint I32 Signed )))377 (Tarray Any (Tint I16 Signed ) 3)))378 (Tint I16 Signed ))) (Tint I32 Signed ))379 (Expr (Ecast (Tint I32 Signed )380 (Expr (Ederef381 (Expr (Ebinop Oadd382 (Expr (Evar (succ_pos_of_nat 157))383 (Tarray Any (Tint I16 Signed ) 3))384 (Expr (Econst_int (repr 1))385 (Tint I32 Signed )))386 (Tarray Any (Tint I16 Signed ) 3)))387 (Tint I16 Signed ))) (Tint I32 Signed )))388 (Tint I32 Signed ))389 (Expr (Ecast (Tint I32 Signed )390 (Expr (Ederef391 (Expr (Ebinop Oadd392 (Expr (Evar (succ_pos_of_nat 157))393 (Tarray Any (Tint I16 Signed ) 3))394 (Expr (Econst_int (repr 2))395 (Tint I32 Signed )))396 (Tarray Any (Tint I16 Signed ) 3)))397 (Tint I16 Signed ))) (Tint I32 Signed )))398 (Tint I32 Signed ))))))))366 (Sreturn (Some expr (Expr (Ebinop Oadd 367 (Expr (Ebinop Oadd 368 (Expr (Ecast (Tint I32 Signed ) 369 (Expr (Ederef 370 (Expr (Ebinop Oadd 371 (Expr (Evar (succ_pos_of_nat 25)) 372 (Tarray Any (Tint I16 Signed ) 3)) 373 (Expr (Econst_int (repr 0)) 374 (Tint I32 Signed ))) 375 (Tarray Any (Tint I16 Signed ) 3))) 376 (Tint I16 Signed ))) (Tint I32 Signed )) 377 (Expr (Ecast (Tint I32 Signed ) 378 (Expr (Ederef 379 (Expr (Ebinop Oadd 380 (Expr (Evar (succ_pos_of_nat 25)) 381 (Tarray Any (Tint I16 Signed ) 3)) 382 (Expr (Econst_int (repr 1)) 383 (Tint I32 Signed ))) 384 (Tarray Any (Tint I16 Signed ) 3))) 385 (Tint I16 Signed ))) (Tint I32 Signed ))) 386 (Tint I32 Signed )) 387 (Expr (Ecast (Tint I32 Signed ) 388 (Expr (Ederef 389 (Expr (Ebinop Oadd 390 (Expr (Evar (succ_pos_of_nat 25)) 391 (Tarray Any (Tint I16 Signed ) 3)) 392 (Expr (Econst_int (repr 2)) 393 (Tint I32 Signed ))) 394 (Tarray Any (Tint I16 Signed ) 3))) 395 (Tint I16 Signed ))) (Tint I32 Signed ))) 396 (Tint I32 Signed )))))))) 399 397 400 398 401 399 402 ) )]403 (succ_pos_of_nat 155)400 )〉] 401 (succ_pos_of_nat 23) 404 402 [] 405 403 . 406 404 407 nremark exec: result ? (exec_up_to myprog 80 []). 408 nnormalize; (* you can examine the result here *) 409 @; nqed. 405 example exec: 406 (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 0)]; OK ? (is_final s)) = OK ? (Some ? (repr 6)). 407 normalize @refl 408 qed. -
src/Clight/test/factorial.ma
r415 r717 1 include " Animation.ma".1 include "Clight/Animation.ma". 2 2 3 ndefinition myprog := mk_program fundef type4 [mk_pair ?? (succ_pos_of_nat 132 (* get_input *)) (External (succ_pos_of_nat 132) Tnil (Tint I32 Signed ));5 mk_pair ?? (succ_pos_of_nat 133 (* main *)) (Internal (6 mk_function (Tint I32 Signed ) [] [ mk_pair ?? (succ_pos_of_nat 134) (Tint I32 Signed ); mk_pair ?? (succ_pos_of_nat 135) (Tint I32 Signed ); mk_pair ?? (succ_pos_of_nat 136) (Tint I32 Signed )]3 definition myprog := mk_program fundef type 4 [〈succ_pos_of_nat 0 (* get_input *), External (succ_pos_of_nat 0) Tnil (Tint I32 Signed )〉; 5 〈succ_pos_of_nat 1 (* main *), Internal ( 6 mk_function (Tint I32 Signed ) [] [〈succ_pos_of_nat 2, (Tint I32 Signed )〉 ; 〈succ_pos_of_nat 3, (Tint I32 Signed )〉 ; 〈succ_pos_of_nat 4, (Tint I32 Signed )〉 ] 7 7 (Ssequence 8 (Scall (Some ? (Expr (Evar (succ_pos_of_nat 134)) (Tint I32 Signed )))9 (Expr (Evar (succ_pos_of_nat 132))8 (Scall (Some expr (Expr (Evar (succ_pos_of_nat 2)) (Tint I32 Signed ))) 9 (Expr (Evar (succ_pos_of_nat 0)) 10 10 (Tfunction Tnil (Tint I32 Signed ))) 11 11 []) 12 12 (Ssequence 13 (Sassign (Expr (Evar (succ_pos_of_nat 135)) (Tint I32 Signed ))13 (Sassign (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed )) 14 14 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 15 15 (Ssequence 16 (Sfor (Sassign (Expr (Evar (succ_pos_of_nat 136)) (Tint I32 Signed )) 16 (Ssequence 17 (Sfor (Sassign (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed )) 17 18 (Expr (Econst_int (repr 2)) (Tint I32 Signed ))) 18 19 (Expr (Ebinop Ole 19 (Expr (Evar (succ_pos_of_nat 136)) (Tint I32 Signed ))20 (Expr (Evar (succ_pos_of_nat 134)) (Tint I32 Signed )))20 (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed )) 21 (Expr (Evar (succ_pos_of_nat 2)) (Tint I32 Signed ))) 21 22 (Tint I32 Signed )) 22 (Sassign (Expr (Evar (succ_pos_of_nat 136)) (Tint I32 Signed ))23 (Sassign (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed )) 23 24 (Expr (Ebinop Oadd 24 (Expr (Evar (succ_pos_of_nat 136)) (Tint I32 Signed ))25 (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed )) 25 26 (Expr (Econst_int (repr 1)) (Tint I32 Signed ))) 26 27 (Tint I32 Signed ))) 27 (Sassign (Expr (Evar (succ_pos_of_nat 135)) (Tint I32 Signed ))28 (Sassign (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed )) 28 29 (Expr (Ebinop Omul 29 (Expr (Evar (succ_pos_of_nat 135)) (Tint I32 Signed ))30 (Expr (Evar (succ_pos_of_nat 136)) (Tint I32 Signed )))30 (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed )) 31 (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed ))) 31 32 (Tint I32 Signed ))) 32 33 ) 33 (Sreturn (Some ? (Expr (Evar (succ_pos_of_nat 135)) 34 (Tint I32 Signed ))))))) 34 Sskip) 35 (Sreturn (Some expr (Expr (Evar (succ_pos_of_nat 3)) 36 (Tint I32 Signed ))))))) 35 37 36 38 37 39 38 ) )]39 (succ_pos_of_nat 1 33)40 )〉] 41 (succ_pos_of_nat 1) 40 42 [] 41 43 . 42 44 43 nremark exec: result ? (exec_up_to myprog 40 [EVint (repr 5)]). 44 nnormalize; (* you can examine the result here *) 45 @; nqed. 45 example exec: 46 (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 5)]; OK ? (is_final s)) = OK ? (Some ? (repr 120)). 47 normalize (* you can examine the result here *) 48 @refl qed. -
src/Clight/test/memorymodel.ma
r409 r717 13 13 (**************************************************************************) 14 14 15 include " Mem.ma".15 include "common/Mem.ma". 16 16 17 17 … … 20 20 access, preventing you reading back more information than the memory can 21 21 store. *) 22 ndefinition store0 := empty.23 ndefinition store1block : mem × block ≝ alloc store0 0 4 Any.24 ndefinition store1 : mem ≝ fst ?? store1block.25 ndefinition block := snd ?? store1block.22 definition store0 := empty. 23 definition store1block : mem × block ≝ alloc store0 0 4 Any. 24 definition store1 : mem ≝ fst ?? store1block. 25 definition block := snd ?? store1block. 26 26 27 27 (* write a value *) 28 ndefinition store2 : mem.29 nletin r ≝ (store Mint16unsigned store1 Any block 0 (Vint one));28 definition store2 : mem. 29 letin r ≝ (store Mint16unsigned store1 Any block 0 (Vint one)); 30 30 31 nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;32 ##| #rr; #_; napply rr ##] nqed.31 lapply (refl ? r); elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct 32 | #rr #_ @rr ] qed. 33 33 34 34 (* overwrite the first byte of the value *) 35 ndefinition store3 : mem.36 nletin r ≝ (store Mint8unsigned store1 Any block 0 (Vint one));35 definition store3 : mem. 36 letin r ≝ (store Mint8unsigned store1 Any block 0 (Vint one)); 37 37 38 nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;39 ##| #rr; #_; napply rr ##] nqed.38 lapply (refl ? r) elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct 39 | #rr #_ @ rr ] qed. 40 40 41 41 (* The size checking rejects the read and gives us Some Vundef. *) 42 nremark vl_undef: load Mint16signed store3 Any block 0 = Some ? Vundef. //; nqed.42 example vl_undef: load Mint16signed store3 Any block 0 = Some ? Vundef. @refl qed. 43 43 44 44 (* The read is successful and returns a signed version of the value. *) 45 nremark vl_ok': load Mint8unsigned store3 Any block 0 = Some ? (Vint (zero_ext 8 one)). //; nqed.45 example vl_ok': load Mint8unsigned store3 Any block 0 = Some ? (Vint (zero_ext 8 one)). // qed. 46 46 47 47 (* NB: Double frees are allowed by the memory model (although not necessarily 48 48 by the language). *) 49 ndefinition store4 := free store3 block.50 ndefinition store5 : mem. nletin r ≝ (free store3 block); nwhd in r; napply r; nqed.49 definition store4 := free store3 block. 50 definition store5 : mem. letin r ≝ (free store3 block); whd in r @r qed. 51 51 52 52 (* No ordering is imposed on deallocation (even though alloc and free are only used for 53 53 stack memory in the semantics. *) 54 ndefinition storeA := empty.55 ndefinition storeBblkB := alloc storeA 0 4 Any.56 ndefinition storeCblkC := alloc (fst ?? storeBblkB) 0 8 Any.57 ndefinition storeD := free (fst ?? storeCblkC) (snd ?? storeBblkB).58 ndefinition storeE : mem. nletin r ≝ (free storeD (snd ?? storeCblkC)).59 nwhd in r; napply r; nqed.54 definition storeA := empty. 55 definition storeBblkB := alloc storeA 0 4 Any. 56 definition storeCblkC := alloc (fst ?? storeBblkB) 0 8 Any. 57 definition storeD := free (fst ?? storeCblkC) (snd ?? storeBblkB). 58 definition storeE : mem. letin r ≝ (free storeD (snd ?? storeCblkC)). 59 whd in r @r qed. 60 60 61 61 (* Access to the "object representation" (as the C standard puts it) is not specified. *) 62 ndefinition storeI := empty.63 ndefinition storeIIblk := alloc storeA 0 4 Any.64 ndefinition storeIII : mem.65 nletin r ≝ (store Mint32 (fst ?? storeIIblk) Any (snd ?? storeIIblk) 0 (Vint one));66 nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;67 ##| #rr; #_; napply rr ##] nqed.68 ndefinition byte := load Mint8unsigned storeIII Any (snd ?? storeIIblk) 0.69 nremark byteundef: byte = Some ? Vundef. //; nqed. (* :( *)62 definition storeI := empty. 63 definition storeIIblk := alloc storeA 0 4 Any. 64 definition storeIII : mem. 65 letin r ≝ (store Mint32 (fst ?? storeIIblk) Any (snd ?? storeIIblk) 0 (Vint one)); 66 lapply (refl ? r) elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct 67 | #rr #_ @rr ] qed. 68 definition byte := load Mint8unsigned storeIII Any (snd ?? storeIIblk) 0. 69 example byteundef: byte = Some ? Vundef. // qed. (* :( *) -
src/Clight/test/transform1.ma
r25 r717 1 1 (* 2 2 include "Csyntax.ma". 3 3 include "AST.ma". … … 131 131 ##] 132 132 ##| 133 134 *)
Note: See TracChangeset
for help on using the changeset viewer.
