diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Pure.ml | 3 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 5 |
2 files changed, 7 insertions, 1 deletions
diff --git a/src/Pure.ml b/src/Pure.ml index 90f6dc26..fc6cbad1 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -496,5 +496,8 @@ type fun_def = { *) signature : fun_sig; inputs : var list; + inputs_lvs : typed_lvalue list; + (** The inputs seen as lvalues. Allows to make transformations, for example + to replace unused variables by `_` *) body : expression; } diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index d7bcadb4..ada64720 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -1292,12 +1292,15 @@ let translate_fun_def (ctx : bs_ctx) (body : S.expression) : fun_def = backward_ids) in let inputs = List.append ctx.forward_inputs backward_inputs in + let inputs_lvs = List.map (fun v -> mk_typed_lvalue_from_var v None) inputs in (* Sanity check *) assert ( List.for_all (fun (var, ty) -> (var : var).ty = ty) (List.combine inputs signature.inputs)); - let def = { def_id; back_id = bid; basename; signature; inputs; body } in + let def = + { def_id; back_id = bid; basename; signature; inputs; inputs_lvs; body } + in (* Debugging *) log#ldebug (lazy |