diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Pure.ml | 15 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 4 |
2 files changed, 11 insertions, 8 deletions
diff --git a/src/Pure.ml b/src/Pure.ml index 45609273..02f6b1ba 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -82,17 +82,20 @@ type scalar_value = V.scalar_value type constant_value = V.constant_value -type var = { id : VarId.id; ty : ty } +type var = { + id : VarId.id; + basename : string option; + (** The "basename" is used to generate a meaningful name for the variable + (by potentially adding an index to uniquely identify it). + *) + ty : ty; +} (** Because we introduce a lot of temporary variables, the list of variables is not fixed: we thus must carry all its information with the variable itself. - - TODO: add a field for the basename. *) -type var_or_dummy = - | Var of var (** TODO: use var_id, not var *) - | Dummy (** Ignored value: `_`. *) +type var_or_dummy = Var of var | Dummy (** Ignored value: `_`. *) (** A left value (which appears on the left of assignments *) type lvalue = diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 53073563..716b4e94 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -571,7 +571,7 @@ let fresh_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : (* Generate the fresh variable *) let id, var_counter = VarId.fresh ctx.var_counter in let ty = ctx_translate_fwd_ty ctx sv.sv_ty in - let var = { id; ty } in + let var = { id; basename = None; ty } in (* Insert in the map *) let sv_to_var = V.SymbolicValueId.Map.add sv.sv_id var ctx.sv_to_var in (* Update the context *) @@ -587,7 +587,7 @@ let fresh_vars_for_symbolic_values (svl : V.symbolic_value list) (ctx : bs_ctx) let fresh_var (ty : ty) (ctx : bs_ctx) : bs_ctx * var = (* Generate the fresh variable *) let id, var_counter = VarId.fresh ctx.var_counter in - let var = { id; ty } in + let var = { id; basename = None; ty } in (* Update the context *) let ctx = { ctx with var_counter } in (* Return *) |