Basile Desloges authored 5 years ago and Julien Signoles committed 5 years ago

A `file` parameter is added before `line`, and the `char *` parameters
have been converted to `const char *`.

[e-acsl] ensure that terms of the E-ACSL ast are never shared before code injection. This invariant is required for E-ACSL typing soundness

- Modifiable with GCC flag without redefinition warning
- No overlapping with other segments when it's too big
- TODO: Overlapping can still occur if stack is too big

Fixes Issue 69: unsound translation when bounds for quantified variables are bigger than their types

 - Safe locations are ok but need to increase TLS to 32 Mo for the libxml usecase
 - Fix order of operations during memory initialization
 - TODO: memory allocated before main are not seen as being valid

- BTS #!1354 is actually not yet fixed
- Logic functions and logic global variables are not yet supported
- Better description of features that are not yet implemented
- Add missing \cinput files

 - Date format in Changelog
 - No code generation in the original project
 - \valid_read(&(t.j) + (1..3)) is valid
 - addresses -> pointers