From 028d4a7cd53da44c908eebc2ef1eef8235471034 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thibault.martin@cea.fr>
Date: Fri, 4 Oct 2019 17:10:44 +0100
Subject: [PATCH] Ajout de location pour __retres
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
__retres a maintenant pour location celle de la première occurence de Return
---
src/kernel_internals/typing/oneret.ml | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/src/kernel_internals/typing/oneret.ml b/src/kernel_internals/typing/oneret.ml
index 93f6d99db42..b38c76261b4 100644
--- a/src/kernel_internals/typing/oneret.ml
+++ b/src/kernel_internals/typing/oneret.ml
@@ -197,11 +197,12 @@ 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 () ->
+ fun ?(loc=Cil_datatype.Location.unknown) ()->
match !retVar with
Some rv -> rv
| None -> begin
let rv = makeLocalVar f "__retres" retTyp in (* don't collide *)
+ rv.vdecl <- loc;
retVar := Some rv;
rv
end
@@ -338,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 ()), NoOffset), rval, loc))
+ Some rval -> Instr (Set((Var (getRetVar ~loc ()), NoOffset), rval, loc))
| None -> Instr (Skip loc)
end;
let returns_assert = ref ptrue in
--
GitLab