Changeset 2569 for src/common


Ignore:
Timestamp:
Jan 4, 2013, 2:59:37 PM (7 years ago)
Author:
campbell
Message:

Fix Clight semantics for ptr + char. (Compiler works anyway.)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Pointers.ma

    r2296 r2569  
    104104  λn,o,i. mk_offset (addition_n ? (offv o) (sign_ext … i)).
    105105(* A version of shift_offset_n for multiplied addresses which avoids overflow. *)
    106 definition shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
    107   λn,o,i,j. mk_offset (addition_n ? (offv o) (short_multiplication ? (bitvector_of_nat … i) (sign_ext … j))).
     106definition shift_offset_n : ∀n. offset → nat → signedness → BitVector n → offset ≝
     107  λn,o,i,sg,j. mk_offset (addition_n ? (offv o) (short_multiplication ? (bitvector_of_nat … i) (match sg with [ Signed ⇒ sign_ext … j | _ ⇒ zero_ext … j]))).
    108108definition neg_shift_offset : ∀n. offset → BitVector n → offset ≝
    109109  λn,o,i. mk_offset (subtraction ? (offv o) (sign_ext … i)).
    110 definition neg_shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
    111   λn,o,i,j. mk_offset (subtraction ? (offv o) (short_multiplication ? (bitvector_of_nat … i) (sign_ext … j))).
     110definition neg_shift_offset_n : ∀n. offset → nat → signedness → BitVector n → offset ≝
     111  λn,o,i,sg,j. mk_offset (subtraction ? (offv o) (short_multiplication ? (bitvector_of_nat … i) (match sg with [ Signed ⇒ sign_ext … j | _ ⇒ zero_ext … j]))).
    112112definition sub_offset : ∀n. offset → offset → BitVector n ≝
    113113  λn,x,y. sign_ext … (subtraction ? (offv x) (offv y)).
     
    132132
    133133(* multiply shift by a nat (i.e., sizeof) without danger of overflow *)
    134 definition shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝
    135  λn,p,i,j. mk_pointer (*ptype p*) (pblock p) (*pok p*) (shift_offset_n n (poff p) i j).
     134definition shift_pointer_n: ∀n. pointer → nat → signedness → BitVector n → pointer ≝
     135 λn,p,i,sg,j. mk_pointer (*ptype p*) (pblock p) (*pok p*) (shift_offset_n n (poff p) i sg j).
    136136
    137137definition neg_shift_pointer: ∀n. pointer → BitVector n → pointer ≝
    138138 λn,p,i. mk_pointer (*ptype p*) (pblock p) (*pok p*) (neg_shift_offset n (poff p) i).
    139139
    140 definition neg_shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝
    141  λn,p,i,j. mk_pointer (*ptype p*) (pblock p) (*pok p*) (neg_shift_offset_n n (poff p) i j).
     140definition neg_shift_pointer_n: ∀n. pointer → nat → signedness → BitVector n → pointer ≝
     141 λn,p,i,sg,j. mk_pointer (*ptype p*) (pblock p) (*pok p*) (neg_shift_offset_n n (poff p) i sg j).
    142142
    143143definition eq_pointer: pointer → pointer → bool ≝
Note: See TracChangeset for help on using the changeset viewer.