[wp] Better management of trivial FALSE in the context in Condition.ml
- do not drop type step without variables - better management of Branch/Either in Condition.ml
Showing
- src/plugins/wp/Conditions.ml 20 additions, 14 deletionssrc/plugins/wp/Conditions.ml
- src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle 9 additions, 5 deletions...s/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle
- src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memtyped.res.oracle 17 additions, 6 deletions..._acsl/oracle/assigned_not_initialized_memtyped.res.oracle
- src/plugins/wp/tests/wp_acsl/oracle/block_length.res.oracle 48 additions, 8 deletionssrc/plugins/wp/tests/wp_acsl/oracle/block_length.res.oracle
- src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.0.res.oracle 4 additions, 0 deletions...ugins/wp/tests/wp_acsl/oracle/init_value_mem.0.res.oracle
- src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle 8 additions, 4 deletions...s/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle
- src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle 21 additions, 0 deletionssrc/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
- src/plugins/wp/tests/wp_acsl/oracle/null.res.oracle 2 additions, 2 deletionssrc/plugins/wp/tests/wp_acsl/oracle/null.res.oracle
- src/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle 46 additions, 7 deletionssrc/plugins/wp/tests/wp_acsl/oracle/pointer.res.oracle
- src/plugins/wp/tests/wp_bts/oracle/bts_2079.res.oracle 3 additions, 3 deletionssrc/plugins/wp/tests/wp_bts/oracle/bts_2079.res.oracle
- src/plugins/wp/tests/wp_plugin/oracle/flash.0.res.oracle 65 additions, 49 deletionssrc/plugins/wp/tests/wp_plugin/oracle/flash.0.res.oracle
- src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle 65 additions, 43 deletionssrc/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle
- src/plugins/wp/tests/wp_plugin/oracle/init_const_guard.res.oracle 1 addition, 1 deletion...ins/wp/tests/wp_plugin/oracle/init_const_guard.res.oracle
- src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle 8 additions, 8 deletionssrc/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle
- src/plugins/wp/tests/wp_store/oracle/struct.res.oracle 4 additions, 0 deletionssrc/plugins/wp/tests/wp_store/oracle/struct.res.oracle
- src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle 1 addition, 1 deletionsrc/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle
- src/plugins/wp/tests/wp_typed/oracle/unit_hard.0.res.oracle 6 additions, 1 deletionsrc/plugins/wp/tests/wp_typed/oracle/unit_hard.0.res.oracle
- src/plugins/wp/tests/wp_typed/oracle/unit_hard.1.res.oracle 6 additions, 1 deletionsrc/plugins/wp/tests/wp_typed/oracle/unit_hard.1.res.oracle
Loading
Please register or sign in to comment