From 90f5dc58a45745965ad96fa8abd246687c0e43e0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 17 May 2019 14:39:12 +0200
Subject: [PATCH] [rte] Do not visit variable declarations; fixes a crash.
---
src/plugins/rte/visit.ml | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml
index 664c6cce892..f75e2ce715c 100644
--- a/src/plugins/rte/visit.ml
+++ b/src/plugins/rte/visit.ml
@@ -112,6 +112,11 @@ class annot_visitor kf flags on_alarm = object (self)
let on_alarm ~invalid a = on_alarm stmt ~invalid a in
fgen ~remove_trivial:flags.Flags.remove_trivial ~on_alarm
+ (* Do not visit variable declarations, as no alarm should be emitted here,
+ and there is no statement to emit an alarm anyway ([generate_assertion]
+ or [Alarms.register] would then crash). *)
+ method !vvdec _ = Cil.SkipChildren
+
method! vstmt s = match s.skind with
| UnspecifiedSequence l ->
(* UnspecifiedSequences may contain lvals for side-effects, that
--
GitLab