- Dec 10, 2015
-
-
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
-
- Dec 04, 2015
-
-
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
-
- Nov 06, 2015
-
-
Julien Signoles authored
-
Julien Signoles authored
-
Julien Signoles authored
-
- Oct 29, 2015
-
-
Julien Signoles authored
-
- Oct 21, 2015
-
-
Julien Signoles authored
-
- Oct 01, 2015
-
-
Julien Signoles authored
Allow to use Merlin even in internal mode NB: compatibility with external compilation not tested
See merge request !16 -
Virgile Prevosto authored
NB: compatibility with external compilation not tested
-
- Aug 31, 2015
-
-
Julien Signoles authored
-
- Aug 26, 2015
-
-
Julien Signoles authored
-
Julien Signoles authored
-
- Aug 25, 2015
-
-
Julien Signoles authored
-
- Jul 26, 2015
-
-
Boris Yakobowski authored
-
- Jun 30, 2015
-
-
Julien Signoles authored
-
- Jun 24, 2015
-
-
Julien Signoles authored
-