Ignore:
Timestamp:
Mar 4, 2011, 6:20:28 PM (9 years ago)
Author:
campbell
Message:

Switch to more conservative definitions in preparation for review.
(Efficient mul/div via Z, sort out some disambiguation problems that have
appeared.)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Csem.ma

    r583 r638  
    201201      match v1 with
    202202      [ Vint n1 ⇒ match v2 with
    203         [ Vint n2 ⇒ option_map … Vint (division_u ? n1 n2)
     203        [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (divu n1 n2))
     204(*        [ Vint n2 ⇒ option_map … Vint (division_u ? n1 n2)*)
    204205        | _ ⇒ None ? ]
    205206      | _ ⇒ None ? ]
     
    207208      match v1 with
    208209       [ Vint n1 ⇒ match v2 with
    209          [ Vint n2 ⇒ option_map … Vint (division_s ? n1 n2)
     210         [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint(divs n1 n2))
     211(*         [ Vint n2 ⇒ option_map … Vint (division_s ? n1 n2)*)
    210212         | _ ⇒ None ? ]
    211213      | _ ⇒ None ? ]
     
    225227      match v1 with
    226228      [ Vint n1 ⇒ match v2 with
    227         [ Vint n2 ⇒ option_map … Vint (modulus_u ? n1 n2)
     229        [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (modu n1 n2))
     230(*        [ Vint n2 ⇒ option_map … Vint (modulus_u ? n1 n2)*)
    228231        | _ ⇒ None ? ]
    229232      | _ ⇒ None ? ]
     
    231234      match v1 with
    232235      [ Vint n1 ⇒ match v2 with
    233         [ Vint n2 ⇒ option_map … Vint (modulus_s ? n1 n2)
     236        [ Vint n2 ⇒ if eq n2 zero then None ? else Some ? (Vint (mods n1 n2))
     237(*        [ Vint n2 ⇒ option_map … Vint (modulus_s ? n1 n2)*)
    234238        | _ ⇒ None ? ]
    235239      | _ ⇒ None ? ]
Note: See TracChangeset for help on using the changeset viewer.