From 479248161ff08341a5d6cef72007cc3e1d496b43 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 25 Feb 2019 17:14:06 +0100
Subject: [PATCH] [ACSL] fixes cabs2cil/logic_typing communication on label
environment
More precisely, ensures that the statement returned by `find_label l` actually
contains label `l`
---
src/kernel_internals/typing/cabs2cil.ml | 12 ++++++------
1 file changed, 6 insertions(+), 6 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 8725e512b03..82e1679d6b5 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -1519,13 +1519,13 @@ struct
try
ref (H.find labels s)
with Not_found when List.mem s !label_current ->
- let my_ref =
- ref
- (mkEmptyStmt
- (* just a placeholder that will never be used. no need to
- check for ghost status here. *)
- ~ghost:false ~valid_sid ~loc:(cabslu "_find_label") ())
+ (* just a placeholder that will never be used. no need to
+ check for ghost status here. *)
+ let my_stmt =
+ mkEmptyStmt ~ghost:false ~valid_sid ~loc:(cabslu "_find_label") ()
in
+ my_stmt.labels <- [Label(s,cabslu "_find_label",true)];
+ let my_ref = ref my_stmt in
addGoto s my_ref; my_ref
end
--
GitLab