@ngsrinivas This is a pr of window_based program equivalence check. Could you please review the following key functions when you are free? Thanks!
There are three key functions of static analysis:
static_analysis() -> static analysis of a program
set_up_smt_inout_orig() -> setting the static variables in validator input and output according to the original program's static analysis
set_up_smt_inout_win() -> setting validator input and output for a window program according to the original program's static analysis
input_constraint() is a function of variable path condition constraints in the precondition.
smt_pgm_eq_chk(), smt_pgm_set_pre() and smt_pgm_set_same_input() are also modified for the window program.
For the precondition setting: only V_win_r in the V_pre_w are being set;
For the postcondition equivalence check, only check the intersection of V_win_w and V_post_r
@ngsrinivas This is a pr of window_based program equivalence check. Could you please review the following key functions when you are free? Thanks! There are three key functions of static analysis: static_analysis() -> static analysis of a program set_up_smt_inout_orig() -> setting the static variables in validator input and output according to the original program's static analysis set_up_smt_inout_win() -> setting validator input and output for a window program according to the original program's static analysis
input_constraint() is a function of variable path condition constraints in the precondition. smt_pgm_eq_chk(), smt_pgm_set_pre() and smt_pgm_set_same_input() are also modified for the window program.
For the precondition setting: only V_win_r in the V_pre_w are being set; For the postcondition equivalence check, only check the intersection of V_win_w and V_post_r