Merge branch 'feature/wp/extend-split-and' into 'master'
Extend split tactic : split conjunctions See merge request frama-c/frama-c!3470
No related branches found
No related tags found
Showing
- src/plugins/wp/Conditions.ml 20 additions, 11 deletionssrc/plugins/wp/Conditions.ml
- src/plugins/wp/Conditions.mli 4 additions, 0 deletionssrc/plugins/wp/Conditions.mli
- src/plugins/wp/ProverScript.ml 10 additions, 0 deletionssrc/plugins/wp/ProverScript.ml
- src/plugins/wp/TacSplit.ml 44 additions, 31 deletionssrc/plugins/wp/TacSplit.ml
- src/plugins/wp/Tactical.ml 9 additions, 0 deletionssrc/plugins/wp/Tactical.ml
- src/plugins/wp/Tactical.mli 1 addition, 0 deletionssrc/plugins/wp/Tactical.mli
- src/plugins/wp/tests/wp_tip/oracle/split.res.oracle 707 additions, 0 deletionssrc/plugins/wp/tests/wp_tip/oracle/split.res.oracle
- src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_and_ensures.json 4 additions, 0 deletions...ip/oracle/split.session/script/test_goal_and_ensures.json
- src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_eq_ensures.json 4 additions, 0 deletions...tip/oracle/split.session/script/test_goal_eq_ensures.json
- src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_ex_and_ensures.json 5 additions, 0 deletions...oracle/split.session/script/test_goal_ex_and_ensures.json
- src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_ex_if_ensures.json 5 additions, 0 deletions.../oracle/split.session/script/test_goal_ex_if_ensures.json
- src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_ex_imply_ensures.json 4 additions, 0 deletions...acle/split.session/script/test_goal_ex_imply_ensures.json
- src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_ex_or_ensures.json 4 additions, 0 deletions.../oracle/split.session/script/test_goal_ex_or_ensures.json
- src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_if_ensures.json 5 additions, 0 deletions...tip/oracle/split.session/script/test_goal_if_ensures.json
- src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_goal_neq_ensures.json 4 additions, 0 deletions...ip/oracle/split.session/script/test_goal_neq_ensures.json
- src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_inside_leq_ensures.json 6 additions, 0 deletions.../oracle/split.session/script/test_inside_leq_ensures.json
- src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_inside_lt_ensures.json 5 additions, 0 deletions...p/oracle/split.session/script/test_inside_lt_ensures.json
- src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_inside_neq_ensures.json 6 additions, 0 deletions.../oracle/split.session/script/test_inside_neq_ensures.json
- src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_and_ensures.json 4 additions, 0 deletions...ip/oracle/split.session/script/test_step_and_ensures.json
- src/plugins/wp/tests/wp_tip/oracle/split.session/script/test_step_branch_ensures.json 4 additions, 0 deletions...oracle/split.session/script/test_step_branch_ensures.json
Loading
Please register or sign in to comment