[E-ACSL] analysis: fixed soundness bug when calling several times the same function
Showing
- src/plugins/e-acsl/TODO 0 additions, 1 deletionsrc/plugins/e-acsl/TODO
- src/plugins/e-acsl/known_bugs/bts1392_ghost_extern.i 0 additions, 6 deletionssrc/plugins/e-acsl/known_bugs/bts1392_ghost_extern.i
- src/plugins/e-acsl/known_bugs/bts1412.c 0 additions, 154 deletionssrc/plugins/e-acsl/known_bugs/bts1412.c
- src/plugins/e-acsl/pre_analysis.ml 106 additions, 45 deletionssrc/plugins/e-acsl/pre_analysis.ml
- src/plugins/e-acsl/tests/e-acsl-runtime/call.c 23 additions, 0 deletionssrc/plugins/e-acsl/tests/e-acsl-runtime/call.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.err.oracle 0 additions, 0 deletions...gins/e-acsl/tests/e-acsl-runtime/oracle/call.1.err.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle 58 additions, 0 deletions...gins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.err.oracle 0 additions, 0 deletions...lugins/e-acsl/tests/e-acsl-runtime/oracle/call.err.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.res.oracle 58 additions, 0 deletions...lugins/e-acsl/tests/e-acsl-runtime/oracle/call.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c 171 additions, 0 deletionssrc/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c 171 additions, 0 deletionssrc/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_call2.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c 7 additions, 0 deletions...plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c 7 additions, 0 deletions...lugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
Loading
Please register or sign in to comment