Merge branch 'kostyantyn/bugfix/global-initialisers' into 'master'
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
No related branches found
No related tags found
Showing
- src/plugins/e-acsl/.gitlab-ci.yml 6 additions, 0 deletionssrc/plugins/e-acsl/.gitlab-ci.yml
- src/plugins/e-acsl/doc/Changelog 2 additions, 0 deletionssrc/plugins/e-acsl/doc/Changelog
- src/plugins/e-acsl/tests/bts/bts1718.i 19 additions, 0 deletionssrc/plugins/e-acsl/tests/bts/bts1718.i
- src/plugins/e-acsl/tests/bts/oracle/bts1718.0.err.oracle 0 additions, 0 deletionssrc/plugins/e-acsl/tests/bts/oracle/bts1718.0.err.oracle
- src/plugins/e-acsl/tests/bts/oracle/bts1718.0.res.oracle 22 additions, 0 deletionssrc/plugins/e-acsl/tests/bts/oracle/bts1718.0.res.oracle
- src/plugins/e-acsl/tests/bts/oracle/bts1718.1.err.oracle 0 additions, 0 deletionssrc/plugins/e-acsl/tests/bts/oracle/bts1718.1.err.oracle
- src/plugins/e-acsl/tests/bts/oracle/bts1718.1.res.oracle 22 additions, 0 deletionssrc/plugins/e-acsl/tests/bts/oracle/bts1718.1.res.oracle
- src/plugins/e-acsl/tests/bts/oracle/bts1837.0.res.oracle 1 addition, 1 deletionsrc/plugins/e-acsl/tests/bts/oracle/bts1837.0.res.oracle
- src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle 1 addition, 1 deletionsrc/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle
- src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c 111 additions, 0 deletionssrc/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
- src/plugins/e-acsl/tests/bts/oracle/gen_bts17182.c 111 additions, 0 deletionssrc/plugins/e-acsl/tests/bts/oracle/gen_bts17182.c
- src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c 1 addition, 2 deletionssrc/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
- src/plugins/e-acsl/tests/e-acsl-runtime/compound_initializers.c 47 additions, 0 deletions...ugins/e-acsl/tests/e-acsl-runtime/compound_initializers.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.0.err.oracle 0 additions, 0 deletions.../e-acsl-runtime/oracle/compound_initializers.0.err.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.0.res.oracle 52 additions, 0 deletions.../e-acsl-runtime/oracle/compound_initializers.0.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.1.err.oracle 0 additions, 0 deletions.../e-acsl-runtime/oracle/compound_initializers.1.err.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.1.res.oracle 58 additions, 0 deletions.../e-acsl-runtime/oracle/compound_initializers.1.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_compound_initializers.c 243 additions, 0 deletions...l/tests/e-acsl-runtime/oracle/gen_compound_initializers.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_compound_initializers2.c 288 additions, 0 deletions.../tests/e-acsl-runtime/oracle/gen_compound_initializers2.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c 3 additions, 6 deletions...s/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
Loading
Please register or sign in to comment