Changeset 744 for src/Clight/Csem.ma
 Timestamp:
 Apr 7, 2011, 6:53:59 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/Csem.ma
r725 r744 170 170 if eq_block b1 b2 then 171 171 if eq (repr (sizeof ty)) zero then None ? 172 else Some ? (Vint (divu (sub_offset ofs1 ofs2) (repr (sizeof ty)))) 172 else match division_u ? (sub_offset ofs1 ofs2) (repr (sizeof ty)) with 173 [ None ⇒ None ? 174  Some v ⇒ Some ? (Vint v) 175 ] 173 176 else None ? 174 177  _ ⇒ None ? ] … … 202 205 match v1 with 203 206 [ Vint n1 ⇒ match v2 with 204 [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (divu n1 n2)) 205 (* [ Vint n2 ⇒ option_map … Vint (division_u ? n1 n2)*) 207 [ Vint n2 ⇒ option_map … Vint (division_u ? n1 n2) 206 208  _ ⇒ None ? ] 207 209  _ ⇒ None ? ] … … 209 211 match v1 with 210 212 [ Vint n1 ⇒ match v2 with 211 [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint(divs n1 n2)) 212 (* [ Vint n2 ⇒ option_map … Vint (division_s ? n1 n2)*) 213 [ Vint n2 ⇒ option_map … Vint (division_s ? n1 n2) 213 214  _ ⇒ None ? ] 214 215  _ ⇒ None ? ] … … 228 229 match v1 with 229 230 [ Vint n1 ⇒ match v2 with 230 [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (modu n1 n2)) 231 (* [ Vint n2 ⇒ option_map … Vint (modulus_u ? n1 n2)*) 231 [ Vint n2 ⇒ option_map … Vint (modulus_u ? n1 n2) 232 232  _ ⇒ None ? ] 233 233  _ ⇒ None ? ] … … 235 235 match v1 with 236 236 [ Vint n1 ⇒ match v2 with 237 [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (mods n1 n2)) 238 (* [ Vint n2 ⇒ option_map … Vint (modulus_s ? n1 n2)*) 237 [ Vint n2 ⇒ option_map … Vint (modulus_s ? n1 n2) 239 238  _ ⇒ None ? ] 240 239  _ ⇒ None ? ]
Note: See TracChangeset
for help on using the changeset viewer.