From b2f1c397b6e31925f0435fa347a2bf15c92e226e Mon Sep 17 00:00:00 2001 From: Thibault Martin <thibault.martin@cea.fr> Date: Mon, 7 Oct 2019 10:20:13 +0100 Subject: [PATCH] =?UTF-8?q?Retrait=20du=20param=C3=A8tre=20optionel=20pour?= =?UTF-8?q?=20getRetVar?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/kernel_internals/typing/oneret.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/kernel_internals/typing/oneret.ml b/src/kernel_internals/typing/oneret.ml index b38c76261b4..eb1304e6708 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 -- GitLab