From 4016ad5be8b95b265ead77034f357af6a985724a Mon Sep 17 00:00:00 2001
From: Thibault Martin <thibault.martin@cea.fr>
Date: Mon, 7 Oct 2019 15:09:17 +0200
Subject: [PATCH] Update la location quand anciennement unknown
---
src/kernel_internals/typing/oneret.ml | 15 ++++++++-------
1 file changed, 8 insertions(+), 7 deletions(-)
diff --git a/src/kernel_internals/typing/oneret.ml b/src/kernel_internals/typing/oneret.ml
index d90fd7e2f48..e789fd76600 100644
--- a/src/kernel_internals/typing/oneret.ml
+++ b/src/kernel_internals/typing/oneret.ml
@@ -199,13 +199,14 @@ let oneret ?(callback: callback option) (f: fundec) : unit =
let retVar : varinfo option ref = ref None in
fun loc ->
match !retVar with
- Some rv -> rv
- | None -> begin
- let rv = makeLocalVar ~loc f "__retres" retTyp in
- (* don't collide *)
- retVar := Some rv;
- rv
- end
+ | None ->
+ let rv = makeLocalVar ~loc f "__retres" retTyp in (* don't collide *)
+ retVar := Some rv;
+ rv
+ | Some rv ->
+ if rv.vdecl = Cil_datatype.Location.unknown then
+ rv.vdecl <- loc;
+ rv
in
let convert_result p =
let vis = object
--
GitLab