diff options
Diffstat (limited to 'compiler/InterpreterExpressions.ml')
-rw-r--r-- | compiler/InterpreterExpressions.ml | 14 |
1 files changed, 5 insertions, 9 deletions
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index af545fb9..9f117933 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -283,7 +283,7 @@ let eval_operand_no_reorganize (config : config) (op : operand) List.find (fun (name, _) -> name = const_name) trait_decl.consts in (* Introduce a fresh symbolic value *) - let v = mk_fresh_symbolic_typed_value TraitConst ty in + let v = mk_fresh_symbolic_typed_value ty in (* Continue the evaluation *) let e = cf v ctx in (* We have to wrap the generated expression *) @@ -315,7 +315,7 @@ let eval_operand_no_reorganize (config : config) (op : operand) copy_value allow_adt_copy config ctx cv | SymbolicMode -> (* We use the looked up value only for its type *) - let v = mk_fresh_symbolic_typed_value KindConstGeneric cv.ty in + let v = mk_fresh_symbolic_typed_value cv.ty in (ctx, v) in (* Continue *) @@ -464,9 +464,7 @@ let eval_unary_op_symbolic (config : config) (unop : unop) (op : operand) | Cast (CastInteger (_, tgt_ty)), _ -> TLiteral (TInteger tgt_ty) | _ -> raise (Failure "Invalid input for unop") in - let res_sv = - { sv_kind = FunCallRet; sv_id = res_sv_id; sv_ty = res_sv_ty } - in + let res_sv = { sv_id = res_sv_id; sv_ty = res_sv_ty } in (* Call the continuation *) let expr = cf (Ok (mk_typed_value_from_symbolic_value res_sv)) ctx in (* Synthesize the symbolic AST *) @@ -603,9 +601,7 @@ let eval_binary_op_symbolic (config : config) (binop : binop) (op1 : operand) | Ne | Eq -> raise (Failure "Unreachable")) | _ -> raise (Failure "Invalid inputs for binop") in - let res_sv = - { sv_kind = FunCallRet; sv_id = res_sv_id; sv_ty = res_sv_ty } - in + let res_sv = { sv_id = res_sv_id; sv_ty = res_sv_ty } in (* Call the continuattion *) let v = mk_typed_value_from_symbolic_value res_sv in let expr = cf (Ok v) ctx in @@ -769,7 +765,7 @@ let eval_rvalue_aggregate (config : config) (aggregate_kind : aggregate_kind) array we introduce here might be duplicated in the generated code: by introducing a symbolic value we introduce a let-binding in the generated code. *) - let saggregated = mk_fresh_symbolic_typed_value Aggregate ty in + let saggregated = mk_fresh_symbolic_typed_value ty in (* Call the continuation *) match cf saggregated ctx with | None -> None |