Literal strings in global arrays with compound initializers are not correctly initialized
ID0001817: This issue was created automatically from Mantis Issue 1817. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001817 | Frama-C | Plug-in > E-ACSL | public | 2014-06-25 | 2017-01-18 |
| Reporter | arvidj | Assigned To | kvorobyov | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | Frama-C 14-Silicon |
Description :
Frama-C GIT Commit: b71d80ef
The generated function for initializing global variables "__e_acsl_memory_init" does not handle arrays containing literal strings with compound intializers.
Example:
char A[2] = {"foo", "bar"}; int main(void) { /@ assert \valid(A[0]) ; / /@ assert \valid(A[1]) ; */ }
Generated __e_acsl_memory_init: void __e_acsl_memory_init(void) { char *__e_acsl_literal_string; __store_block((void *)(A),sizeof(char *[2])); __e_acsl_literal_string = "bar"; __store_block((void *)__e_acsl_literal_string,sizeof("bar")); __full_init((void *)__e_acsl_literal_string,sizeof("bar")); __literal_string((void *)__e_acsl_literal_string); A = (char *)__e_acsl_literal_string; return; }
The last assignment is incorrect.