- Jan 08, 2016
-
-
Julien Signoles authored
-
- Jan 05, 2016
-
-
Boris Yakobowski authored
-
- Dec 28, 2015
-
-
Julien Signoles authored
-
Julien Signoles authored
-
- Dec 26, 2015
-
-
Julien Signoles authored
-
Julien Signoles authored
Miscellaneous updates/Convenience script The merge request suggests the following changes: - Removal of trailing spaces in visit.ml. - Adjustment of the `stdio.c` test to prevent it from writing a test file into the project's root directory. - Added a convenience script for runs of E-ACSL/GCC. Functionality to `install` and `uninstall` executable files from the `scripts` directory has also been added. See merge request !19
-
Julien Signoles authored
-
- Dec 16, 2015
-
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
add an option to pass specific flags directly to frama-c
-
Kostyantyn Vorobyov authored
added option to redirect all output to a given file
-
Kostyantyn Vorobyov authored
errors or warnings
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
Used frama-c-config tool instead of frama-c executable to retrieve share path
-
Kostyantyn Vorobyov authored
- Renamed to e-acsl-gcc.sh - BUGFIX: Clean abort on frama-c/gcc failures - Use an explicit list of disabled warnings instead of plain '-w' for gcc runs
-
- Dec 15, 2015
-
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
using E-ACSL plugin and their subsequent compilation using GCC.
-
Kostyantyn Vorobyov authored
into the project's root
-
Kostyantyn Vorobyov authored
-
- Dec 10, 2015
-
-
Julien Signoles authored
-
Julien Signoles authored
-
Julien Signoles authored
Kostyantyn/bugfix/global initialisers This is the fix for the issue `0001817`: `Literal strings in global arrays with compound initializers are not correctly initialized`. The change is as we have discussed during our meeting on the 7th of December. The gist of the fix as follows: - Initialisers of all global variables are kept (instead of being removed), so as the code used for initialisations within the body of the `__e_acsl_memory_init`. - Literal strings used in initialisations are recorded via special global variables. The fix relies on the fact that a compiler will maintain only a single instance of a literal string, so recording a literal string once will cover all its uses. For example, strings pointed to by some global variables `A` and `B`: ``` ... const char *A = "X"; const char *B = "X"; ... ``` will be captured by: ``` ... __e_acsl_literal_string = "X"; __store_block((void *)__e_acsl_literal_string,sizeof("X")); __full_init((void *)__e_acsl_literal_string); __literal_string((void *)__e_acsl_literal_string); ... ``` There are some test failures, as some code generation has changed. I have intentionally left them in for the fist time so you can see the tests that fail. If this patch is accepted I am happy to fix the test suite and add a couple of new tests to cover the issue. I have also attached a file with some examples of global initialisers for different cases which you may find useful. [compound_initialiser.c](https://git.frama-c.com/frama-c/e-acsl/uploads/3599d1cbca9c790d6dd231d052ccf2f0/compound_initialiser.c) See merge request !18
-
Kostyantyn Vorobyov authored
doc/Changelog
-
Kostyantyn Vorobyov authored
-
- Dec 09, 2015
-
-
François Bobot authored
-
François Bobot authored
-
- Dec 08, 2015
-
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
- Updated CI configuration
-
Kostyantyn Vorobyov authored
initializers - Changes to the oracles in order to accommodate the changes to code generation
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
variables (which point to literal strings) generated by E-ACSL
-
Kostyantyn Vorobyov authored
times
-
Kostyantyn Vorobyov authored
global initialisers or not) with a boolean switch called is_initialiser used to detect and filter out compound initialisers and update [global_vars] mapping
-
Kostyantyn Vorobyov authored
during global initialisation
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
declarations
-
Kostyantyn Vorobyov authored
-
- Dec 07, 2015
-
-
Kostyantyn Vorobyov authored
variables (which point to literal strings) generated by E-ACSL
-
Kostyantyn Vorobyov authored
times
-