Changeset 2822 for src/Clight/Csem.ma


Ignore:
Timestamp:
Mar 8, 2013, 12:48:20 PM (8 years ago)
Author:
garnier
Message:

A consitent proof state for Clight to Cminor, with some progress (and some temporary regressions)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r2722 r2822  
    129129].
    130130
    131 (* Ilias, 16 jan 2013: semantics of pointer/pointer subtraction slightly changed. Matched in toCminor.ma.
    132  * operation done on 32 bits and cast down to the target size using sign_ext or zero_ext, according to the
    133  * sign of the target type. We have to do the same in toCminor.ma
    134  * At least two things are ugly here : the fact that offsets are 32 bits (our arch is 8 bit right ?), and the downcast.
    135  * TODO: check the C standard to see if the following alternative is meaningful ?
    136  *   . the division can directly take as an argument a target size. There is also two [repr], one
    137  *     with type nat → bvint I32 (used here), one with type ∀sz. nat → bvint sz. Matching changes
    138  *     would have to be done in Cminor.
    139  *)
     131(* Ilias, 16 jan 2013: semantics of pointer/pointer subtraction slightly changed. Matched in toCminor.ma. *)
    140132let rec sem_sub (v1:val) (t1:type) (v2: val) (t2:type) (target:type) : option val ≝
    141133  match classify_sub t1 t2 with
Note: See TracChangeset for help on using the changeset viewer.