Merge branch 'feature/blanchard/wp/type-constraint' into 'stable/scandium'
[wp] Adds type constraints on MemTyped chunks See merge request frama-c/frama-c!2671
Showing
- src/plugins/wp/LogicCompiler.ml 8 additions, 1 deletionsrc/plugins/wp/LogicCompiler.ml
- src/plugins/wp/MemEmpty.ml 1 addition, 0 deletionssrc/plugins/wp/MemEmpty.ml
- src/plugins/wp/MemRegion.ml 2 additions, 0 deletionssrc/plugins/wp/MemRegion.ml
- src/plugins/wp/MemTyped.ml 67 additions, 11 deletionssrc/plugins/wp/MemTyped.ml
- src/plugins/wp/MemVar.ml 3 additions, 0 deletionssrc/plugins/wp/MemVar.ml
- src/plugins/wp/MemZeroAlias.ml 2 additions, 0 deletionssrc/plugins/wp/MemZeroAlias.ml
- src/plugins/wp/Sigs.ml 4 additions, 0 deletionssrc/plugins/wp/Sigs.ml
- src/plugins/wp/cfgWP.ml 7 additions, 3 deletionssrc/plugins/wp/cfgWP.ml
- src/plugins/wp/tests/wp_acsl/chunk_typing.i 54 additions, 0 deletionssrc/plugins/wp/tests/wp_acsl/chunk_typing.i
- src/plugins/wp/tests/wp_acsl/chunk_typing_usable.i 47 additions, 0 deletionssrc/plugins/wp/tests/wp_acsl/chunk_typing_usable.i
- src/plugins/wp/tests/wp_acsl/chunk_typing_usable.script 37 additions, 0 deletionssrc/plugins/wp/tests/wp_acsl/chunk_typing_usable.script
- src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle 1889 additions, 0 deletionssrc/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
- src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle 501 additions, 0 deletions...ns/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle
- src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle 9 additions, 52 deletionssrc/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
- src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle 63 additions, 0 deletions...ns/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle
- src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.res.oracle 24 additions, 0 deletions...ests/wp_acsl/oracle_qualif/chunk_typing_usable.res.oracle
Loading
Please register or sign in to comment