From 6ef40b9d6b135cba095628a0a6b1baf0de16938c Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 6 Sep 2021 10:52:31 +0200
Subject: [PATCH] [e-acsl] ignore functions with only terminates
---
.../e-acsl/src/project_initializer/prepare_ast.ml | 14 ++++++++++++--
1 file changed, 12 insertions(+), 2 deletions(-)
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
index d3b9353faf6..7d9589cab9a 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -598,6 +598,13 @@ let unduplicable_functions =
Datatype.String.Set.empty
white_list
+(* Note: it might not have terminates at all, the point is just to ignore it. *)
+let spec_has_only_terminates spec =
+ spec.spec_variant = None &&
+ List.for_all Cil.is_empty_behavior spec.spec_behavior &&
+ spec.spec_disjoint_behaviors = [] &&
+ spec.spec_complete_behaviors = []
+
let must_duplicate kf vi =
(* it is not already duplicated *)
not (Dup_functions.mem vi)
@@ -614,8 +621,11 @@ let must_duplicate kf vi =
not (Functions.instrument kf)
||
(* or: *)
- ((* it has a function contract *)
- not (Cil.is_empty_funspec (Annotations.funspec ~populate:false kf))
+ ( let spec = Annotations.funspec ~populate:false kf in
+ (* it has a function contract *)
+ not (Cil.is_empty_funspec spec)
+ && (* there are some annotations that might be treated *)
+ not (spec_has_only_terminates spec)
&& (* its annotations must be monitored *)
Functions.check kf))
--
GitLab