[e-acsl] fix logic variable escaping its scope
When translating a function we must ensure that it cannot re-use any expressions resulting from translating logic variables from its call site. One might think that this may not occur, since logic variables are unique. However sometimes the same logic function needs to be translated twice (with different signatures). In that case there are indeed indentical logic variables for different C code to be generated, and re-using that code would be erroneous. See the pathological example from the previous commit. This commit fixes this by clearing the map of logic bindings before translating a function body.
Showing
- src/plugins/e-acsl/doc/Changelog 1 addition, 0 deletionssrc/plugins/e-acsl/doc/Changelog
- src/plugins/e-acsl/src/code_generator/env.ml 1 addition, 0 deletionssrc/plugins/e-acsl/src/code_generator/env.ml
- src/plugins/e-acsl/src/code_generator/env.mli 2 additions, 0 deletionssrc/plugins/e-acsl/src/code_generator/env.mli
- src/plugins/e-acsl/src/code_generator/logic_functions.ml 3 additions, 0 deletionssrc/plugins/e-acsl/src/code_generator/logic_functions.ml
- src/plugins/e-acsl/src/code_generator/translate_terms.ml 2 additions, 1 deletionsrc/plugins/e-acsl/src/code_generator/translate_terms.ml
- src/plugins/e-acsl/tests/constructs/oracle/gen_let.c 1 addition, 2 deletionssrc/plugins/e-acsl/tests/constructs/oracle/gen_let.c
- src/plugins/e-acsl/tests/constructs/oracle/let.res.oracle 1 addition, 2 deletionssrc/plugins/e-acsl/tests/constructs/oracle/let.res.oracle
Loading
Please register or sign in to comment