[E-ACSL] handle specified function without code. BTW that fixes bugs #1300 and #1340.
[E-ACSL] convert postcondition even in presence of untranslated assigns clause [E-ACSL] fix bug when the translation of a predicate containing \at is abruptely stopped because of a not-yet-implemented construct (the generated code contained undeclared __e_acsl_at variables)
Showing
- src/plugins/e-acsl/Makefile.in 1 addition, 0 deletionssrc/plugins/e-acsl/Makefile.in
- src/plugins/e-acsl/TODO 0 additions, 6 deletionssrc/plugins/e-acsl/TODO
- src/plugins/e-acsl/doc/Changelog 4 additions, 0 deletionssrc/plugins/e-acsl/doc/Changelog
- src/plugins/e-acsl/env.ml 27 additions, 7 deletionssrc/plugins/e-acsl/env.ml
- src/plugins/e-acsl/env.mli 9 additions, 0 deletionssrc/plugins/e-acsl/env.mli
- src/plugins/e-acsl/gcc_test.sh 1 addition, 1 deletionsrc/plugins/e-acsl/gcc_test.sh
- src/plugins/e-acsl/main.ml 15 additions, 6 deletionssrc/plugins/e-acsl/main.ml
- src/plugins/e-acsl/pre_visit.ml 245 additions, 0 deletionssrc/plugins/e-acsl/pre_visit.ml
- src/plugins/e-acsl/pre_visit.mli 32 additions, 0 deletionssrc/plugins/e-acsl/pre_visit.mli
- src/plugins/e-acsl/share/e-acsl/e_acsl.h 2 additions, 0 deletionssrc/plugins/e-acsl/share/e-acsl/e_acsl.h
- src/plugins/e-acsl/tests/e-acsl-runtime/at.i 4 additions, 1 deletionsrc/plugins/e-acsl/tests/e-acsl-runtime/at.i
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle 3 additions, 1 deletion...ns/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle 3 additions, 1 deletion...gins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle 3 additions, 1 deletion...ins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle 3 additions, 1 deletion...ugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle 3 additions, 1 deletion...ins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle 3 additions, 1 deletion...ugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle 23 additions, 13 deletions...lugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle 18 additions, 8 deletionssrc/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
- src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle 3 additions, 1 deletion...s/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle
Loading
Please register or sign in to comment