diff --git a/src/plugins/e-acsl/exit_points.ml b/src/plugins/e-acsl/exit_points.ml index 3c1d1625376f0a930bbe2b54ff22a41acea66d74..55af3ebb56d1d46dc76aa2f3cac03c6d526f6251 100644 --- a/src/plugins/e-acsl/exit_points.ml +++ b/src/plugins/e-acsl/exit_points.ml @@ -126,10 +126,12 @@ class jump_context = object (_) add_exit stmt !sref; add_labelled !sref stmt; Cil.DoChildren - | _ when (List.length stmt.labels) > 0 -> - add_locals stmt (List.flatten locals); + | Instr(_) | Return(_) | If(_) | Block(_) | UnspecifiedSequence(_) + | Throw(_) | TryCatch(_) | TryFinally(_) | TryExcept(_) -> + (match stmt.labels with + | [] -> () + | _ :: _ -> add_locals stmt (List.flatten locals)); Cil.DoChildren - | _ -> Cil.DoChildren end let generate fct =