diff --git a/src/kernel_internals/typing/oneret.ml b/src/kernel_internals/typing/oneret.ml index b38c76261b4ceed564667a13ac787e484cf5d01b..eb1304e67086d9d2da413bb90e67b3dbeb56838c 100644 --- a/src/kernel_internals/typing/oneret.ml +++ b/src/kernel_internals/typing/oneret.ml @@ -197,7 +197,7 @@ let oneret ?(callback: callback option) (f: fundec) : unit = let lastloc = ref Cil_datatype.Location.unknown in let getRetVar = let retVar : varinfo option ref = ref None in - fun ?(loc=Cil_datatype.Location.unknown) ()-> + fun loc -> match !retVar with Some rv -> rv | None -> begin @@ -212,7 +212,7 @@ let oneret ?(callback: callback option) (f: fundec) : unit = inherit Cil.nopCilVisitor method! vterm_lhost = function | TResult _ -> - let v = getRetVar () in + let v = getRetVar Cil_datatype.Location.unknown in ChangeTo (TVar (cvar_to_lvar v)) | TMem _ | TVar _ -> DoChildren end @@ -268,7 +268,7 @@ let oneret ?(callback: callback option) (f: fundec) : unit = (* Must create a statement *) let rv = if hasRet then - Some (new_exp ~loc (Lval(Var (getRetVar ()), NoOffset))) + Some (new_exp ~loc (Lval(Var (getRetVar loc), NoOffset))) else None in mkStmt (Return (rv, loc)) @@ -339,7 +339,7 @@ let oneret ?(callback: callback option) (f: fundec) : unit = * an instruction that sets the return value (if any). *) s.skind <- begin match retval with - Some rval -> Instr (Set((Var (getRetVar ~loc ()), NoOffset), rval, loc)) + Some rval -> Instr (Set((Var (getRetVar loc), NoOffset), rval, loc)) | None -> Instr (Skip loc) end; let returns_assert = ref ptrue in @@ -348,7 +348,7 @@ let oneret ?(callback: callback option) (f: fundec) : unit = returns_stack; (match retval with | Some _ -> - let lvar = Cil.cvar_to_lvar (getRetVar()) in + let lvar = Cil.cvar_to_lvar (getRetVar loc) in Stack.iter (fun (_,_,ca) -> adjust_assigns_clause loc lvar ca.annot_content) returns_stack