Ignore:
Timestamp:
Dec 13, 2012, 5:22:51 PM (7 years ago)
Author:
garnier
Message:

Proof of expression translation correctness "mostly" done for CL to CM. Some inconsistencies found in bit width for constants
regarding boolean operators need to be fixed (either by modifying CL semantics of by making CM code generation inefficient).
An inconsistency between clight and cminor expression evaluation was found for cost labels (placed before and after trace) - not
fixed yet, for fear of breaking proofs. One or two small lemmas missing, and most importantly, binary operators not done yet.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/memoryInjections.ma

    r2500 r2554  
    371371
    372372
    373 (* A particular inversion. *)
     373(* particulars inversion. *)
    374374lemma value_eq_ptr_inversion :
    375375  ∀E,p1,v. value_eq E (Vptr p1) v → ∃p2. v = Vptr p2 ∧ pointer_translation p1 E = Some ? p2.
     
    381381     %{p2} @conj try @refl try assumption
    382382] qed.
     383
     384lemma value_eq_int_inversion :
     385  ∀E,sz,i,v. value_eq E (Vint sz i) v → v = (Vint sz i).
     386#E #sz #i #v #Heq inversion Heq
     387[ 1: #Habsurd destruct (Habsurd)
     388| 2: #sz #i #Heq #Heq' #_ @refl
     389| 3: #Habsurd destruct (Habsurd)
     390| 4: #p1 #p2 #Heq #Heqv #Heqv2 #_ destruct ]
     391qed.
    383392
    384393(* A cleaner version of inversion for [value_eq] *)
Note: See TracChangeset for help on using the changeset viewer.