Ignore:
Timestamp:
May 10, 2013, 6:21:46 PM (7 years ago)
Author:
tranquil
Message:

added validate_pointer filter
in Interference added that intereference only fires on non eliminable
statements

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/joint_semantics.ma

    r3261 r3265  
    2121; pc_from_label : (Σbl.block_region bl = Code) → F globals → label →
    2222    option program_counter
     23; get_joint_if_local_stacksize : F globals → ℕ
     24; get_joint_if_params_stacksize : F globals → ℕ
    2325}.
    2426
     
    237239    ident (* current *) → call_dest uns_pars (* current ret *) →
    238240      state st_pars → res (state st_pars × program_counter)
     241  (* filter parts of the stack that are accessible *)
     242  ; validate_pointer : ∀globals.∀ge : genv_gen F globals.
     243    ident (* current *) → state st_pars → pointer → res unit
    239244  }.
    240245
     
    458463    ! vaddrl ← dpl_arg_retrieve … st addrl;
    459464    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
     465    !_ validate_pointer … ge curr_id st vaddr ;
    460466    ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
    461467    acca_store p … dst v st
     
    464470    ! vaddrl ← dpl_arg_retrieve … st addrl;
    465471    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
     472    !_ validate_pointer … ge curr_id st vaddr ;
    466473    ! v ← acca_arg_retrieve … st src;
    467474    ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
Note: See TracChangeset for help on using the changeset viewer.