Merge branch 'feature/blanchard/wp/clean-why3-theories' into 'master' (4cf18bdc) · Commits · pub / frama-c · GitLab

Skip to content

GitLab

Explore

Sign in

Primary navigation

Project

F

frama-c
- Activity
- Members
- Labels
- Issues
- Issue boards
- Milestones
- Wiki
- Incidents

Snippets Groups Projects

4cf18bdc

Commit 4cf18bdc authored 6 months ago by Loïc Correnson

Downloads
- Plain Diff

Merge branch 'feature/blanchard/wp/clean-why3-theories' into 'master'

Clean Why3 theories

See merge request frama-c/frama-c!4498

parents 5aad15c1 f0c4778f

No related branches found

No related tags found

No related merge requests found

Changes 11

Hide whitespace changes

Inline Side-by-side

Showing

src/plugins/wp/ProverWhy3.ml 0 additions, 15 deletions

src/plugins/wp/ProverWhy3.ml
src/plugins/wp/filter_axioms.ml 0 additions, 176 deletions

src/plugins/wp/filter_axioms.ml
src/plugins/wp/filter_axioms.mli 0 additions, 26 deletions

src/plugins/wp/filter_axioms.mli
src/plugins/wp/share/why3/frama_c_wp/cbits.mlw 0 additions, 240 deletions

src/plugins/wp/share/why3/frama_c_wp/cbits.mlw
src/plugins/wp/share/why3/frama_c_wp/cint.mlw 198 additions, 124 deletions

src/plugins/wp/share/why3/frama_c_wp/cint.mlw
src/plugins/wp/share/why3/frama_c_wp/qed.mlw 8 additions, 19 deletions

src/plugins/wp/share/why3/frama_c_wp/qed.mlw
src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle 1 addition, 1 deletion

...s/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle
src/plugins/wp/tests/wp_acsl/simpl_is_type.i 1 addition, 1 deletion

src/plugins/wp/tests/wp_acsl/simpl_is_type.i
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle 1 addition, 1 deletion

...ns/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
src/plugins/wp/tests/wp_typed/user_init.i 1 addition, 1 deletion

src/plugins/wp/tests/wp_typed/user_init.i
src/plugins/wp/wp.ml 0 additions, 1 deletion

src/plugins/wp/wp.ml

with 210 additions and 605 deletions

Loading

0% Loading or .

You are about to add 0 people to the discussion. Proceed with caution.

Finish editing this message first!

Please register or sign in to comment