diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml index 664c6cce8929d7a36618b53fc429e11033cf2c19..f75e2ce715ce303c7e0a7d2460a7214e280bdd7e 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