Merge branch 'bugfix/basile/eacsl-142-non-blocking-check' into 'master'
[eacsl] Add support of `check` annotations Closes e-acsl#142 See merge request frama-c/frama-c!3076
Showing
- src/plugins/e-acsl/doc/Changelog 2 additions, 0 deletionssrc/plugins/e-acsl/doc/Changelog
- src/plugins/e-acsl/doc/refman/changes_modern.tex 1 addition, 0 deletionssrc/plugins/e-acsl/doc/refman/changes_modern.tex
- src/plugins/e-acsl/doc/refman/fn_behavior.tex 6 additions, 6 deletionssrc/plugins/e-acsl/doc/refman/fn_behavior.tex
- src/plugins/e-acsl/doc/refman/model.tex 1 addition, 1 deletionsrc/plugins/e-acsl/doc/refman/model.tex
- src/plugins/e-acsl/doc/refman/predicate.tex 20 additions, 20 deletionssrc/plugins/e-acsl/doc/refman/predicate.tex
- src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.c 6 additions, 4 deletions...e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.c
- src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h 13 additions, 5 deletions...e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h
- src/plugins/e-acsl/src/code_generator/contract.ml 77 additions, 71 deletionssrc/plugins/e-acsl/src/code_generator/contract.ml
- src/plugins/e-acsl/src/code_generator/env.ml 1 addition, 1 deletionsrc/plugins/e-acsl/src/code_generator/env.ml
- src/plugins/e-acsl/src/code_generator/env.mli 2 additions, 2 deletionssrc/plugins/e-acsl/src/code_generator/env.mli
- src/plugins/e-acsl/src/code_generator/logic_array.ml 1 addition, 1 deletionsrc/plugins/e-acsl/src/code_generator/logic_array.ml
- src/plugins/e-acsl/src/code_generator/loops.ml 2 additions, 2 deletionssrc/plugins/e-acsl/src/code_generator/loops.ml
- src/plugins/e-acsl/src/code_generator/loops.mli 1 addition, 1 deletionsrc/plugins/e-acsl/src/code_generator/loops.mli
- src/plugins/e-acsl/src/code_generator/memory_translate.ml 1 addition, 1 deletionsrc/plugins/e-acsl/src/code_generator/memory_translate.ml
- src/plugins/e-acsl/src/code_generator/smart_stmt.ml 11 additions, 3 deletionssrc/plugins/e-acsl/src/code_generator/smart_stmt.ml
- src/plugins/e-acsl/src/code_generator/smart_stmt.mli 15 additions, 11 deletionssrc/plugins/e-acsl/src/code_generator/smart_stmt.mli
- src/plugins/e-acsl/src/code_generator/translate.ml 27 additions, 20 deletionssrc/plugins/e-acsl/src/code_generator/translate.ml
- src/plugins/e-acsl/src/code_generator/translate.mli 5 additions, 1 deletionsrc/plugins/e-acsl/src/code_generator/translate.mli
- src/plugins/e-acsl/src/code_generator/translate_annots.ml 3 additions, 3 deletionssrc/plugins/e-acsl/src/code_generator/translate_annots.ml
- src/plugins/e-acsl/tests/arith/oracle_ci/arith.res.oracle 3 additions, 3 deletionssrc/plugins/e-acsl/tests/arith/oracle_ci/arith.res.oracle
Loading
Please register or sign in to comment