From 5e4953b2526ade3738917795fe4f1e55b9023c36 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Wed, 1 Mar 2017 11:14:30 +0100
Subject: [PATCH] Small opt with pattern matching
---
src/plugins/e-acsl/exit_points.ml | 8 +++++---
1 file changed, 5 insertions(+), 3 deletions(-)
diff --git a/src/plugins/e-acsl/exit_points.ml b/src/plugins/e-acsl/exit_points.ml
index 3c1d1625376..55af3ebb56d 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 =
--
GitLab