Merge branch 'feature/eva/is-infinite' into 'master' (a5a819cc) · 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

a5a819cc

Commit a5a819cc authored 3 years ago by Andre Maroneze

Downloads
- Plain Diff

Merge branch 'feature/eva/is-infinite' into 'master'

[Eva] Adds support for ACSL predicate is_infinite.

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

parents 18ff3268 4a0b63d1

No related branches found

No related tags found

Loading

Changes 5

Hide whitespace changes

Inline Side-by-side

Showing

src/kernel_services/abstract_interp/float_interval.ml 20 additions, 0 deletions

src/kernel_services/abstract_interp/float_interval.ml
src/kernel_services/abstract_interp/float_interval_sig.mli 2 additions, 0 deletions

src/kernel_services/abstract_interp/float_interval_sig.mli
src/plugins/value/legacy/eval_terms.ml 4 additions, 0 deletions

src/plugins/value/legacy/eval_terms.ml
tests/float/oracle/special_floats.res.oracle 54 additions, 27 deletions

tests/float/oracle/special_floats.res.oracle
tests/float/special_floats.c 24 additions, 1 deletion

tests/float/special_floats.c

with 104 additions and 28 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