[eacsl] Update assertions with blocking behavior
Use the `predicate_kind` of `toplevel_predicate` to decide if an assertion should be blocking or not.
Showing
- src/plugins/e-acsl/src/code_generator/contract.ml 63 additions, 43 deletionssrc/plugins/e-acsl/src/code_generator/contract.ml
- 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 1 addition, 1 deletionsrc/plugins/e-acsl/src/code_generator/loops.ml
- 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/translate.ml 27 additions, 19 deletionssrc/plugins/e-acsl/src/code_generator/translate.ml
Loading
Please register or sign in to comment