[eacsl] Update ocaml calls to the RTL
- Add prefix parameter to `Smart_stmt.rtl_call` - Remove `Smart_stmt.lib_call` and replace it with calls to `Smart_stmt.rtl_call` - Add `Smart_stmt.call` to call an arbitrary function from the AST - Use `Smart_stmt.call` when generating calls to `malloc` and `free
Showing
- src/plugins/e-acsl/src/code_generator/at_with_lscope.ml 2 additions, 2 deletionssrc/plugins/e-acsl/src/code_generator/at_with_lscope.ml
- src/plugins/e-acsl/src/code_generator/gmp.ml 4 additions, 3 deletionssrc/plugins/e-acsl/src/code_generator/gmp.ml
- src/plugins/e-acsl/src/code_generator/memory_translate.ml 2 additions, 1 deletionsrc/plugins/e-acsl/src/code_generator/memory_translate.ml
- src/plugins/e-acsl/src/code_generator/rational.ml 11 additions, 3 deletionssrc/plugins/e-acsl/src/code_generator/rational.ml
- src/plugins/e-acsl/src/code_generator/smart_stmt.ml 23 additions, 12 deletionssrc/plugins/e-acsl/src/code_generator/smart_stmt.ml
- src/plugins/e-acsl/src/code_generator/smart_stmt.mli 11 additions, 4 deletionssrc/plugins/e-acsl/src/code_generator/smart_stmt.mli
- src/plugins/e-acsl/src/code_generator/temporal.ml 21 additions, 13 deletionssrc/plugins/e-acsl/src/code_generator/temporal.ml
- src/plugins/e-acsl/src/code_generator/translate.ml 25 additions, 10 deletionssrc/plugins/e-acsl/src/code_generator/translate.ml
- src/plugins/e-acsl/src/libraries/functions.ml 5 additions, 5 deletionssrc/plugins/e-acsl/src/libraries/functions.ml
- src/plugins/e-acsl/src/libraries/functions.mli 6 additions, 0 deletionssrc/plugins/e-acsl/src/libraries/functions.mli
Loading
Please register or sign in to comment