Changeset 2638


Ignore:
Timestamp:
Feb 7, 2013, 2:15:51 PM (6 years ago)
Author:
piccolo
Message:

Back-end fixes for last Garnier's commit that removes the regions from
the blocks. Only part of the back-end has been fixed.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLtoERTLptrOK.ma

    r2604 r2638  
    12791279  fetch_function … (globalenv (λvars.fundef (F vars)) V i p)
    12801280    bl = Error … [MSG BadFunction].
    1281  #F#V#i#p ** #r #id #EQ1 #EQ2 destruct
     1281 #F#V#i#p ** #r #id #EQ1 destruct
    12821282  whd in match fetch_function; normalize nodelta
    12831283  >globalenv_no_minus_one
     
    12901290  fetch_function … (globalenv (λvars.fundef (F vars)) V i p)
    12911291    bl = Error … [MSG BadFunction].
    1292  #F#V#i#p ** #r #id #EQ1 #EQ2 destruct
     1292 #F#V#i#p ** #r #id #EQ1 destruct
    12931293  whd in match fetch_function; normalize nodelta
    12941294  >globalenv_no_zero
  • src/joint/Traces.ma

    r2601 r2638  
    7474  let sem_globals : evaluation_params ≝ pars in
    7575  let ge ≝ ev_genv sem_globals in
    76   let m ≝ alloc_mem … p in
    77   let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
     76  let m0 ≝ alloc_mem … p in
     77  let 〈m,spb〉 as H ≝ alloc … m0 0 external_ram_size in
    7878  let spp : xpointer ≝
    7979    «mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)),
     
    9595  | External _ ⇒ Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *)
    9696  ].
     97cases m0 in H; #m1 #m2 #m3 #H
     98whd in H:(???%); destruct whd in ⊢(??%?); @Zltb_elim_Type0 // #abs @⊥
     99@(absurd … (irreflexive_Zlt …)) % #I cases (I OZ) /3 by transitive_Zlt/
     100qed.
    97101
    98102definition joint_classify_step :
  • src/joint/joint_semantics.ma

    r2601 r2638  
    7575(* special program counter that is guaranteed to not correspond to anything *)
    7676definition exit_pc : program_counter ≝
    77   mk_program_counter «mk_block Code (-1), refl …» one.
     77  mk_program_counter «mk_block (-1), refl …» one.
    7878
    7979definition null_pc : Pos →  program_counter ≝ λpos.
    80     mk_program_counter «mk_block Code OZ, refl …» pos.
     80    mk_program_counter «mk_block ?, ?» pos.
     81cases daemon qed.
    8182
    8283definition set_m: ∀p. bemem → state p → state p ≝
     
    161162  fetch_internal_function … (globalenv (λvars.fundef (F vars)) V i p)
    162163    bl = Error … [MSG BadFunction].
    163  #F#V#i#p ** #r #id #EQ1 #EQ2 destruct
     164 #F#V#i#p ** #r #id #EQ1 destruct
    164165 whd in match fetch_internal_function;
    165166  whd in match fetch_function; normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.