Changeset 648


Ignore:
Timestamp:
Mar 7, 2011, 7:00:08 PM (9 years ago)
Author:
campbell
Message:

Oops, wrong bitvector negation.

Location:
Deliverables/D3.1/C-semantics
Files:
2 edited

Legend:

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

    r638 r648  
    7474  [ Tint _ _ ⇒
    7575      match v with
    76       [ Vint n ⇒ Some ? (Vint (negation_bv wordsize n))
    77       | _ => None ?
     76      [ Vint n ⇒ Some ? (Vint (two_complement_negation wordsize n))
     77      | _ None ?
    7878      ]
    7979  | Tfloat _ ⇒
  • Deliverables/D3.1/C-semantics/Integers.ma

    r638 r648  
    134134definition ltu : int → int → bool ≝ lt_u wordsize.
    135135
    136 definition neg : int → int ≝ negation_bv wordsize.
     136definition neg : int → int ≝ two_complement_negation wordsize.
    137137
    138138let rec zero_ext (n:Z) (x:int) on x : int ≝
Note: See TracChangeset for help on using the changeset viewer.