Merge branch '794-wp-incorrect-quantification-over-logic-types' into 'master'
Resolve "[wp] incorrect quantification over logic types" Closes #794 See merge request frama-c/frama-c!2538
No related branches found
No related tags found
Showing
- src/plugins/wp/Cvalues.ml 0 additions, 5 deletionssrc/plugins/wp/Cvalues.ml
- src/plugins/wp/Cvalues.mli 0 additions, 1 deletionsrc/plugins/wp/Cvalues.mli
- src/plugins/wp/LogicCompiler.ml 84 additions, 29 deletionssrc/plugins/wp/LogicCompiler.ml
- src/plugins/wp/LogicCompiler.mli 2 additions, 0 deletionssrc/plugins/wp/LogicCompiler.mli
- src/plugins/wp/LogicSemantics.ml 1 addition, 1 deletionsrc/plugins/wp/LogicSemantics.ml
- src/plugins/wp/ProverWhy3.ml 51 additions, 27 deletionssrc/plugins/wp/ProverWhy3.ml
- src/plugins/wp/tests/wp/oracle/sharing.res.oracle 22 additions, 0 deletionssrc/plugins/wp/tests/wp/oracle/sharing.res.oracle
- src/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle 73 additions, 60 deletionssrc/plugins/wp/tests/wp_acsl/oracle/inductive.res.oracle
- src/plugins/wp/tests/wp_acsl/oracle/sum_types.res.oracle 235 additions, 0 deletionssrc/plugins/wp/tests/wp_acsl/oracle/sum_types.res.oracle
- src/plugins/wp/tests/wp_acsl/sum_types.i 35 additions, 0 deletionssrc/plugins/wp/tests/wp_acsl/sum_types.i
- src/plugins/wp/tests/wp_plugin/model.i 1 addition, 1 deletionsrc/plugins/wp/tests/wp_plugin/model.i
- src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle 87 additions, 0 deletions...plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle
- src/plugins/wp/tests/wp_typed/oracle/struct_array_type.res.oracle 21 additions, 0 deletions...ins/wp/tests/wp_typed/oracle/struct_array_type.res.oracle
Loading
Please register or sign in to comment