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/semanticsUtils.ma

    r3037 r3265  
    408408  ! pt ← point_of_label … (joint_if_code … fn) lbl ;
    409409  return mk_program_counter bl (offset_of_point … p pt) in
    410 mk_genv_gen ?? genv ? stacksizes (pre_main_generator … p prog) pc_from_lbl.
     410mk_genv_gen ?? genv ? stacksizes (pre_main_generator … p prog) pc_from_lbl
     411(joint_if_local_stacksize …) (joint_if_params_stacksize …).
    411412#s #H
    412413cases (find_symbol_exists ?? (λx.x) … prog s ?)
Note: See TracChangeset for help on using the changeset viewer.