-
- Downloads
Merge branch 'bugfix/kostyantyn/mmodel-initializers' into 'master'
Bugfix in memory model initialization The E-ACSL instrumentation engine does instrument `__e_acsl_memory_init` function (which initializes a memory model) if there are no variables to track. This is a shortcoming because a program might still need to track its memory state, for instance the following program: ``` int main(void) { /* Allocation increases */ char *a = malloc(7); /* @assert (__heap_size == 7); */ } ``` This merge request suggests a fix for this issue. See merge request !42
No related branches found
No related tags found
Showing
- src/plugins/e-acsl/misc.ml 3 additions, 0 deletionssrc/plugins/e-acsl/misc.ml
- src/plugins/e-acsl/misc.mli 1 addition, 0 deletionssrc/plugins/e-acsl/misc.mli
- src/plugins/e-acsl/mmodel_analysis.ml 12 additions, 2 deletionssrc/plugins/e-acsl/mmodel_analysis.ml
- src/plugins/e-acsl/tests/e-acsl-runtime/init_function.c 13 additions, 0 deletionssrc/plugins/e-acsl/tests/e-acsl-runtime/init_function.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init_function.c 13 additions, 0 deletions...ns/e-acsl/tests/e-acsl-runtime/oracle/gen_init_function.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init_function.err.oracle 0 additions, 0 deletions...acsl/tests/e-acsl-runtime/oracle/init_function.err.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init_function.res.oracle 17 additions, 0 deletions...acsl/tests/e-acsl-runtime/oracle/init_function.res.oracle
- src/plugins/e-acsl/visit.ml 1 addition, 4 deletionssrc/plugins/e-acsl/visit.ml
Loading
Please register or sign in to comment