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

83aaa3a7

Commit 83aaa3a7 authored 4 years ago by Basile Desloges

Downloads
- Plain Diff

Merge branch 'feature/basile/eacsl-127-quantif-binders' into 'master'

[eacsl] Add support for multiple binders in quantification

Closes e-acsl#73 and e-acsl#127

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

parents 332156a9 2bc55d31

No related branches found

No related tags found

Loading

Changes 9

Expand all Hide whitespace changes

Inline Side-by-side

Showing

src/plugins/e-acsl/doc/Changelog 2 additions, 0 deletions

src/plugins/e-acsl/doc/Changelog
src/plugins/e-acsl/src/analyses/typing.ml 17 additions, 6 deletions

src/plugins/e-acsl/src/analyses/typing.ml
src/plugins/e-acsl/src/analyses/typing.mli 2 additions, 2 deletions

src/plugins/e-acsl/src/analyses/typing.mli
src/plugins/e-acsl/src/code_generator/env.ml 9 additions, 2 deletions

src/plugins/e-acsl/src/code_generator/env.ml
src/plugins/e-acsl/src/code_generator/quantif.ml 529 additions, 90 deletions

src/plugins/e-acsl/src/code_generator/quantif.ml
src/plugins/e-acsl/tests/arith/oracle_ci/gen_quantif.c 546 additions, 13 deletions

src/plugins/e-acsl/tests/arith/oracle_ci/gen_quantif.c
src/plugins/e-acsl/tests/arith/oracle_ci/quantif.res.oracle 112 additions, 9 deletions

src/plugins/e-acsl/tests/arith/oracle_ci/quantif.res.oracle
src/plugins/e-acsl/tests/arith/quantif.i 59 additions, 0 deletions

src/plugins/e-acsl/tests/arith/quantif.i
src/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle 3 additions, 2 deletions

src/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle

with 1279 additions and 124 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