[kernel] use same mechanisms for loop allocates as for loop assigns
Showing
- src/kernel_internals/typing/allocates.ml 2 additions, 1 deletionsrc/kernel_internals/typing/allocates.ml
- src/kernel_services/ast_data/annotations.ml 48 additions, 13 deletionssrc/kernel_services/ast_data/annotations.ml
- src/kernel_services/ast_data/annotations.mli 6 additions, 2 deletionssrc/kernel_services/ast_data/annotations.mli
- src/kernel_services/ast_queries/logic_utils.mli 1 addition, 0 deletionssrc/kernel_services/ast_queries/logic_utils.mli
- src/kernel_services/visitors/visitor.ml 4 additions, 2 deletionssrc/kernel_services/visitors/visitor.ml
- tests/spec/loop_assigns_generated.ml 21 additions, 1 deletiontests/spec/loop_assigns_generated.ml
- tests/spec/oracle/loop_assigns_generated.res.oracle 5 additions, 1 deletiontests/spec/oracle/loop_assigns_generated.res.oracle
Loading
Please register or sign in to comment