From 0f7a6598a67a711c180afec658b29a9fb861d926 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 15 Jan 2019 11:40:57 +0100
Subject: [PATCH] [Eva] simplifies slightly the detection of missing unroll
annotations
---
.../value/engine/partitioned_dataflow.ml | 21 ++++++++-----------
1 file changed, 9 insertions(+), 12 deletions(-)
diff --git a/src/plugins/value/engine/partitioned_dataflow.ml b/src/plugins/value/engine/partitioned_dataflow.ml
index 34b0444509e..0fefd04e9a5 100644
--- a/src/plugins/value/engine/partitioned_dataflow.ml
+++ b/src/plugins/value/engine/partitioned_dataflow.ml
@@ -111,19 +111,16 @@ module Make_Dataflow
let unroll (stmt : stmt) : int =
let local_unroll = match Unroll_annots.get_unroll_terms stmt with
| [] ->
- let loop_attr_and_wkey =
- if Cil.hasAttribute "for" stmt.sattr then
- Some ("for", Value_parameters.wkey_missing_loop_unroll_for)
- else if Cil.hasAttribute "while" stmt.sattr then
- Some ("while", Value_parameters.wkey_missing_loop_unroll)
- else if Cil.hasAttribute "dowhile" stmt.sattr then
- Some ("dowhile", Value_parameters.wkey_missing_loop_unroll)
- else None
- in
+ let is_attribute a = Cil.hasAttribute a stmt.sattr in
begin
- match loop_attr_and_wkey with
- | None -> ()
- | Some (loop_kind, wkey) ->
+ match List.filter is_attribute ["for" ; "while" ; "dowhile"] with
+ | [] -> ()
+ | loop_kind :: _ ->
+ let wkey =
+ if loop_kind = "for"
+ then Value_parameters.wkey_missing_loop_unroll_for
+ else Value_parameters.wkey_missing_loop_unroll
+ in
Value_parameters.warning
~wkey ~source:(fst (Cil_datatype.Stmt.loc stmt)) ~once:true
"%s loop without unroll annotation" loop_kind
--
GitLab