| ... | @@ -3,15 +3,54 @@ |
... | @@ -3,15 +3,54 @@ |
|
|
- [frama-c-21.0-Scandium.tar.gz](downloads/frama-c-21.0-Scandium.tar.gz)
|
|
- [frama-c-21.0-Scandium.tar.gz](downloads/frama-c-21.0-Scandium.tar.gz)
|
|
|
|
|
|
|
|
## Manuals
|
|
## Manuals
|
|
|
- [acsl-1.15-beta.pdf](manuals/acsl-1.15-beta.pdf)
|
|
- [acsl-1.15](manuals/acsl-1.15.pdf)
|
|
|
- [acsl-implementation-21.0-Scandium.pdf](manuals/acsl-implementation-21.0-Scandium.pdf)
|
|
- [acsl-implementation](manuals/acsl-implementation-21.0-Scandium.pdf)
|
|
|
- [aorai-manual-21.0-Scandium.pdf](manuals/aorai-manual-21.0-Scandium.pdf)
|
|
- [aorai-example-21.0-Scandium.tgz](manuals/aorai-example-21.0-Scandium.tgz)
|
|
|
- [e-acsl-1.15-beta.pdf](manuals/e-acsl-1.15-beta.pdf)
|
|
- [aorai-manual](manuals/aorai-manual-21.0-Scandium.pdf)
|
|
|
- [e-acsl-implementation-21.0-Scandium.pdf](manuals/e-acsl-implementation-21.0-Scandium.pdf)
|
|
- [e-acsl-1.14](manuals/e-acsl-1.14.pdf)
|
|
|
- [e-acsl-manual-21.0-Scandium.pdf](manuals/e-acsl-manual-21.0-Scandium.pdf)
|
|
- [e-acsl-implementation](manuals/e-acsl-implementation-21.0-Scandium.pdf)
|
|
|
- [eva-manual-21.0-Scandium.pdf](manuals/eva-manual-21.0-Scandium.pdf)
|
|
- [e-acsl-manual](manuals/e-acsl-manual-21.0-Scandium.pdf)
|
|
|
- [metrics-manual-21.0-Scandium.pdf](manuals/metrics-manual-21.0-Scandium.pdf)
|
|
- [eva-manual](manuals/eva-manual-21.0-Scandium.pdf)
|
|
|
- [plugin-development-guide-21.0-Scandium.pdf](manuals/plugin-development-guide-21.0-Scandium.pdf)
|
|
- [metrics-manual](manuals/metrics-manual-21.0-Scandium.pdf)
|
|
|
- [rte-manual-21.0-Scandium.pdf](manuals/rte-manual-21.0-Scandium.pdf)
|
|
- [plugin-development-guide](manuals/plugin-development-guide-21.0-Scandium.pdf)
|
|
|
- [user-manual-21.0-Scandium.pdf](manuals/user-manual-21.0-Scandium.pdf)
|
|
- [rte-manual](manuals/rte-manual-21.0-Scandium.pdf)
|
|
|
- [wp-manual-21.0-Scandium.pdf](manuals/wp-manual-21.0-Scandium.pdf) |
|
- [user-manual](manuals/user-manual-21.0-Scandium.pdf)
|
|
|
|
- [wp-manual](manuals/wp-manual-21.0-Scandium.pdf)
|
|
|
|
|
|
|
|
## Main Changes
|
|
|
|
### Kernel
|
|
|
|
|
|
|
|
- new option `-warn-invalid-pointer` (disabled by default; warns on pointer arithmetic resulting in invalid values)
|
|
|
|
- new option `-warn-pointer-downcast` (enabled by default; warns when a pointer/integer conversion may lead to loss of precision)
|
|
|
|
- improved ghost support: `ghost else`, and check that ghost code does not alter normal control flow
|
|
|
|
- constfold can now use value of const globals
|
|
|
|
|
|
|
|
### Eva
|
|
|
|
|
|
|
|
- New option `-eva-domains` to enable a list of analysis domains (replacing the former options `-eva-name-domain`). `-eva-domains help` prints the list of available domains with a short description
|
|
|
|
- New option `-eva-domains-function` to enable domains only on given functions
|
|
|
|
- When `-warn-invalid-pointers` is enabled, emits alarms on invalid pointer arithmetics resulting in a pointer that does not point inside an object or one past an object (even if the pointer is not used afterward)
|
|
|
|
- The subdivision of evaluations can now be enabled locally:
|
|
|
|
- on given functions through option `-eva-subdivide-non-linear-function`
|
|
|
|
- on specific statements via `/*@ subdivide N; */` annotations.
|
|
|
|
|
|
|
|
### WP
|
|
|
|
|
|
|
|
- Upgraded Why3 backend (requires why3 1.3.1. Please note that if you're upgrading Why3 in the process, you might need to `rm ~/.why3.conf` for `why3 config --full-config` to succeed)
|
|
|
|
- Support for IEEE float model (why3 provers only)
|
|
|
|
- Smoke Tests : attempt to find inconsistencies or dead code from requirements (see `-wp-smoke-tests` option in WP manual)
|
|
|
|
- Many improvements in lemmas, tactics and cache management.
|
|
|
|
|
|
|
|
### E-ACSL
|
|
|
|
|
|
|
|
- Better support of complex jumps for `goto` and switch statements
|
|
|
|
|
|
|
|
### Instantiate
|
|
|
|
|
|
|
|
- A new plug-in, Instantiate, generates function specializations e.g. for functions with `void*` (`memcpy`/`memset`/etc), to help other plugins such as WP.
|
|
|
|
|
|
|
|
### Full list of changes
|
|
|
|
|
|
|
|
- [Main Changelog](https://git.frama-c.com/pub/frama-c/-/blob/21.0/Changelog)
|
|
|
|
- [WP Changelog](https://git.frama-c.com/pub/frama-c/-/blob/21.0/src/plugins/wp/Changelog)
|
|
|
|
- [E-ACSL Changelog](https://git.frama-c.com/pub/frama-c/-/blob/21.0/src/plugins/e-acsl/doc/Changelog) |
