[ACSL] Make `Logic_interp` aware of local variables scopes
Note: at some point, it might be useful to make `term` and `pred` take a `kinstr` as argument to have a better scope for typechecking.
Showing
- src/kernel_services/analysis/logic_interp.ml 42 additions, 10 deletionssrc/kernel_services/analysis/logic_interp.ml
- src/kernel_services/ast_data/kernel_function.ml 6 additions, 0 deletionssrc/kernel_services/ast_data/kernel_function.ml
- src/kernel_services/ast_data/kernel_function.mli 8 additions, 0 deletionssrc/kernel_services/ast_data/kernel_function.mli
Loading
Please register or sign in to comment