Skip to content
Snippets Groups Projects
Commit 4016ad5b authored by Thibault Martin's avatar Thibault Martin Committed by Virgile Prevosto
Browse files

Update la location quand anciennement unknown

parent ee78fde6
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/kernel_internals/typing/oneret.ml
+ 8
− 7
View file @ 4016ad5b
...@@ -199,13 +199,14 @@ let oneret ?(callback: callback option) (f: fundec) : unit = ...@@ -199,13 +199,14 @@ let oneret ?(callback: callback option) (f: fundec) : unit =
let retVar : varinfo option ref = ref None in let retVar : varinfo option ref = ref None in
fun loc -> fun loc ->
match !retVar with match !retVar with
Some rv -> rv | None ->
| None -> begin let rv = makeLocalVar ~loc f "__retres" retTyp in (* don't collide *)
let rv = makeLocalVar ~loc f "__retres" retTyp in retVar := Some rv;
(* don't collide *) rv
retVar := Some rv; | Some rv ->
rv if rv.vdecl = Cil_datatype.Location.unknown then
end rv.vdecl <- loc;
rv
in in
let convert_result p = let convert_result p =
let vis = object let vis = object
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment