From f0316e78295bbc4600a49c222f0883cbbe104000 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 9 Jun 2021 16:54:04 +0200
Subject: [PATCH] [wp] Populate terminates true for declarations
---
src/plugins/wp/cfgAnnot.ml | 4 +---
.../oracle/terminates_call_options.1.res.oracle | 12 ++++++------
.../terminates_call_options.1.res.oracle | 12 ++++++------
3 files changed, 13 insertions(+), 15 deletions(-)
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 39d30a060ee..207a87b2c82 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -215,8 +215,6 @@ let get_terminates_clause kf =
| None when Kernel_function.is_in_libc kf ->
if not @@ Wp_parameters.TerminatesFCDeclarations.get ()
then Assumed Logic_const.pfalse
- else if not @@ Kernel_function.is_definition kf
- then Assumed Logic_const.ptrue
else populate_true ()
| None when Kernel_function.is_definition kf ->
if not @@ Wp_parameters.TerminatesDefinitions.get ()
@@ -225,7 +223,7 @@ let get_terminates_clause kf =
| None ->
if not @@ Wp_parameters.TerminatesExtDeclarations.get ()
then Assumed Logic_const.pfalse
- else Assumed Logic_const.ptrue
+ else populate_true ()
| Some p ->
defined p
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle
index 5a67b6c24f5..d367e2cc027 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.1.res.oracle
@@ -6,14 +6,14 @@
Missing terminates clause for definition, populates 'terminates \true'
[wp] tests/wp_acsl/terminates_call_options.c:32: Warning:
Missing terminates clause for no_spec_generates_goal, populates 'terminates \true'
-[wp] tests/wp_acsl/terminates_call_options.c:24: Warning:
- Missing terminates clause on call to declaration, defaults to \true
+[wp] tests/wp_acsl/terminates_call_options.c:17: Warning:
+ Missing terminates clause for declaration, populates 'terminates \true'
[wp] tests/wp_acsl/terminates_call_options.c:33: Warning:
Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp_acsl/terminates_call_options.c:39: Warning:
- Missing terminates clause on call to exit, defaults to \true
-[wp] tests/wp_acsl/terminates_call_options.c:38: Warning:
- Missing terminates clause on call to div, defaults to \true
+[wp] FRAMAC_SHARE/libc/stdlib.h:475: Warning:
+ Missing terminates clause for exit, populates 'terminates \true'
+[wp] FRAMAC_SHARE/libc/stdlib.h:606: Warning:
+ Missing terminates clause for div, populates 'terminates \true'
------------------------------------------------------------
Function call_declaration
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle
index 027ae6502d5..e6da7db09de 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.1.res.oracle
@@ -6,14 +6,14 @@
Missing terminates clause for definition, populates 'terminates \true'
[wp] tests/wp_acsl/terminates_call_options.c:32: Warning:
Missing terminates clause for no_spec_generates_goal, populates 'terminates \true'
-[wp] tests/wp_acsl/terminates_call_options.c:24: Warning:
- Missing terminates clause on call to declaration, defaults to \true
+[wp] tests/wp_acsl/terminates_call_options.c:17: Warning:
+ Missing terminates clause for declaration, populates 'terminates \true'
[wp] tests/wp_acsl/terminates_call_options.c:33: Warning:
Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp_acsl/terminates_call_options.c:39: Warning:
- Missing terminates clause on call to exit, defaults to \true
-[wp] tests/wp_acsl/terminates_call_options.c:38: Warning:
- Missing terminates clause on call to div, defaults to \true
+[wp] FRAMAC_SHARE/libc/stdlib.h:475: Warning:
+ Missing terminates clause for exit, populates 'terminates \true'
+[wp] FRAMAC_SHARE/libc/stdlib.h:606: Warning:
+ Missing terminates clause for div, populates 'terminates \true'
[wp] 5 goals scheduled
[wp] [Qed] Goal typed_definition_assigns : Valid
[wp] [Qed] Goal typed_call_declaration_terminates : Valid
--
GitLab