[wp] Fixes opaque structures handling
Showing
- src/plugins/wp/CodeSemantics.ml 11 additions, 6 deletionssrc/plugins/wp/CodeSemantics.ml
- src/plugins/wp/Cvalues.ml 74 additions, 20 deletionssrc/plugins/wp/Cvalues.ml
- src/plugins/wp/Definitions.ml 8 additions, 8 deletionssrc/plugins/wp/Definitions.ml
- src/plugins/wp/Definitions.mli 23 additions, 8 deletionssrc/plugins/wp/Definitions.mli
- src/plugins/wp/LogicSemantics.ml 2 additions, 2 deletionssrc/plugins/wp/LogicSemantics.ml
- src/plugins/wp/MemLoader.ml 22 additions, 11 deletionssrc/plugins/wp/MemLoader.ml
- src/plugins/wp/MemLoader.mli 1 addition, 1 deletionsrc/plugins/wp/MemLoader.mli
- src/plugins/wp/MemMemory.ml 4 additions, 4 deletionssrc/plugins/wp/MemMemory.ml
- src/plugins/wp/MemMemory.mli 2 additions, 2 deletionssrc/plugins/wp/MemMemory.mli
- src/plugins/wp/MemRegion.ml 2 additions, 2 deletionssrc/plugins/wp/MemRegion.ml
- src/plugins/wp/MemTyped.ml 86 additions, 38 deletionssrc/plugins/wp/MemTyped.ml
- src/plugins/wp/MemVar.ml 21 additions, 9 deletionssrc/plugins/wp/MemVar.ml
- src/plugins/wp/ProverCoq.ml 12 additions, 7 deletionssrc/plugins/wp/ProverCoq.ml
- src/plugins/wp/ProverErgo.ml 12 additions, 7 deletionssrc/plugins/wp/ProverErgo.ml
- src/plugins/wp/ProverWhy3.ml 11 additions, 5 deletionssrc/plugins/wp/ProverWhy3.ml
- src/plugins/wp/tests/wp_acsl/opaque_struct.i 41 additions, 0 deletionssrc/plugins/wp/tests/wp_acsl/opaque_struct.i
- src/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle 83 additions, 0 deletionssrc/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle
- src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle 29 additions, 0 deletions...s/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle
Loading
Please register or sign in to comment