Merge branch 'feature/wp/nullable-ref' into 'master'
Supports nullable pointers in context See merge request frama-c/frama-c!3078
No related branches found
No related tags found
Showing
- src/kernel_services/ast_queries/acsl_extension.mli 1 addition, 1 deletionsrc/kernel_services/ast_queries/acsl_extension.mli
- src/kernel_services/ast_queries/cil.mli 1 addition, 1 deletionsrc/kernel_services/ast_queries/cil.mli
- src/plugins/wp/Factory.ml 10 additions, 4 deletionssrc/plugins/wp/Factory.ml
- src/plugins/wp/Generator.ml 13 additions, 1 deletionsrc/plugins/wp/Generator.ml
- src/plugins/wp/MemVar.ml 82 additions, 27 deletionssrc/plugins/wp/MemVar.ml
- src/plugins/wp/MemoryContext.ml 95 additions, 33 deletionssrc/plugins/wp/MemoryContext.ml
- src/plugins/wp/MemoryContext.mli 3 additions, 1 deletionsrc/plugins/wp/MemoryContext.mli
- src/plugins/wp/RefUsage.ml 58 additions, 0 deletionssrc/plugins/wp/RefUsage.ml
- src/plugins/wp/RefUsage.mli 8 additions, 0 deletionssrc/plugins/wp/RefUsage.mli
- src/plugins/wp/doc/manual/nullable.c 9 additions, 0 deletionssrc/plugins/wp/doc/manual/nullable.c
- src/plugins/wp/doc/manual/wp_caveat.tex 9 additions, 2 deletionssrc/plugins/wp/doc/manual/wp_caveat.tex
- src/plugins/wp/tests/wp_bts/oracle/bts_1828.1.res.oracle 1 addition, 1 deletionsrc/plugins/wp/tests/wp_bts/oracle/bts_1828.1.res.oracle
- src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle 1 addition, 1 deletion...ugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle
- src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle 1 addition, 1 deletion...ests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle
- src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle 1 addition, 1 deletion...s/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle
- src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle 1 addition, 1 deletion..._gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
- src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle 1 addition, 1 deletion...llery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
- src/plugins/wp/tests/wp_hoare/oracle/dispatch_var.res.oracle 1 addition, 1 deletionsrc/plugins/wp/tests/wp_hoare/oracle/dispatch_var.res.oracle
- src/plugins/wp/tests/wp_hoare/oracle/memory_hypotheses_checking.res.oracle 16 additions, 16 deletions...sts/wp_hoare/oracle/memory_hypotheses_checking.res.oracle
- src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle 1 addition, 1 deletionsrc/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle
Loading
Please register or sign in to comment