From c5578b46cec883962d8548f6c05ae8d4dc9ec820 Mon Sep 17 00:00:00 2001 From: Allan Blanchard <allan.blanchard@cea.fr> Date: Wed, 9 Jun 2021 16:06:51 +0200 Subject: [PATCH] [wp] Typos in a test doc --- .../terminates_call_options.0.res.oracle | 24 +++++++++---------- .../terminates_call_options.1.res.oracle | 20 ++++++++-------- .../terminates_call_options.0.res.oracle | 8 +++---- .../terminates_call_options.1.res.oracle | 12 +++++----- .../tests/wp_acsl/terminates_call_options.c | 5 ++-- 5 files changed, 35 insertions(+), 34 deletions(-) diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.0.res.oracle index 70f61d7719b..d0ad66e5c95 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_call_options.0.res.oracle @@ -2,20 +2,20 @@ [kernel] Parsing tests/wp_acsl/terminates_call_options.c (with preprocessing) [wp] Running WP plugin... [wp] Warning: Missing RTE guards -[wp] tests/wp_acsl/terminates_call_options.c:23: Warning: +[wp] tests/wp_acsl/terminates_call_options.c:24: Warning: Missing terminates clause on call to declaration, defaults to \false -[wp] tests/wp_acsl/terminates_call_options.c:28: Warning: +[wp] tests/wp_acsl/terminates_call_options.c:29: Warning: Missing terminates clause on call to definition, defaults to \false -[wp] tests/wp_acsl/terminates_call_options.c:38: Warning: +[wp] tests/wp_acsl/terminates_call_options.c:39: Warning: Missing terminates clause on call to exit, defaults to \false -[wp] tests/wp_acsl/terminates_call_options.c:37: Warning: +[wp] tests/wp_acsl/terminates_call_options.c:38: Warning: Missing terminates clause on call to div, defaults to \false ------------------------------------------------------------ Function call_declaration ------------------------------------------------------------ -Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 21) in 'call_declaration': -Call Effect at line 23 +Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 22) in 'call_declaration': +Call Effect at line 24 Prove: false. ------------------------------------------------------------ @@ -23,8 +23,8 @@ Prove: false. Function call_definition ------------------------------------------------------------ -Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 26) in 'call_definition': -Call Effect at line 28 +Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 27) in 'call_definition': +Call Effect at line 29 Prove: false. ------------------------------------------------------------ @@ -40,14 +40,14 @@ Prove: true. Function libc_call ------------------------------------------------------------ -Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 35) in 'libc_call' (1/2): -Call Effect at line 37 +Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 36) in 'libc_call' (1/2): +Call Effect at line 38 Prove: false. ------------------------------------------------------------ -Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 35) in 'libc_call' (2/2): -Call Effect at line 38 +Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 36) in 'libc_call' (2/2): +Call Effect at line 39 Prove: false. ------------------------------------------------------------ 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 a48bad2bd1e..5a67b6c24f5 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 @@ -2,23 +2,23 @@ [kernel] Parsing tests/wp_acsl/terminates_call_options.c (with preprocessing) [wp] Running WP plugin... [wp] Warning: Missing RTE guards -[wp] tests/wp_acsl/terminates_call_options.c:19: Warning: +[wp] tests/wp_acsl/terminates_call_options.c:20: Warning: Missing terminates clause for definition, populates 'terminates \true' -[wp] tests/wp_acsl/terminates_call_options.c:31: Warning: +[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:23: Warning: +[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:32: Warning: +[wp] tests/wp_acsl/terminates_call_options.c:33: Warning: Missing assigns clause (assigns 'everything' instead) -[wp] tests/wp_acsl/terminates_call_options.c:38: Warning: +[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:37: Warning: +[wp] tests/wp_acsl/terminates_call_options.c:38: Warning: Missing terminates clause on call to div, defaults to \true ------------------------------------------------------------ Function call_declaration ------------------------------------------------------------ -Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 21) in 'call_declaration': +Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 22) in 'call_declaration': Prove: true. ------------------------------------------------------------ @@ -26,7 +26,7 @@ Prove: true. Function call_definition ------------------------------------------------------------ -Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 26) in 'call_definition': +Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 27) in 'call_definition': Prove: true. ------------------------------------------------------------ @@ -42,7 +42,7 @@ Prove: true. Function libc_call ------------------------------------------------------------ -Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 35) in 'libc_call': +Goal Termination-condition (file tests/wp_acsl/terminates_call_options.c, line 36) in 'libc_call': Prove: true. ------------------------------------------------------------ @@ -51,7 +51,7 @@ Prove: true. ------------------------------------------------------------ Goal Termination-condition (generated) in 'no_spec_generates_goal': -Effect at line 32 +Effect at line 33 Prove: false. ------------------------------------------------------------ diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.0.res.oracle index 014de1caf3f..61733f7adaf 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_call_options.0.res.oracle @@ -2,13 +2,13 @@ [kernel] Parsing tests/wp_acsl/terminates_call_options.c (with preprocessing) [wp] Running WP plugin... [wp] Warning: Missing RTE guards -[wp] tests/wp_acsl/terminates_call_options.c:23: Warning: +[wp] tests/wp_acsl/terminates_call_options.c:24: Warning: Missing terminates clause on call to declaration, defaults to \false -[wp] tests/wp_acsl/terminates_call_options.c:28: Warning: +[wp] tests/wp_acsl/terminates_call_options.c:29: Warning: Missing terminates clause on call to definition, defaults to \false -[wp] tests/wp_acsl/terminates_call_options.c:38: Warning: +[wp] tests/wp_acsl/terminates_call_options.c:39: Warning: Missing terminates clause on call to exit, defaults to \false -[wp] tests/wp_acsl/terminates_call_options.c:37: Warning: +[wp] tests/wp_acsl/terminates_call_options.c:38: Warning: Missing terminates clause on call to div, defaults to \false [wp] 5 goals scheduled [wp] [Qed] Goal typed_definition_assigns : Valid 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 780952849c8..027ae6502d5 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 @@ -2,17 +2,17 @@ [kernel] Parsing tests/wp_acsl/terminates_call_options.c (with preprocessing) [wp] Running WP plugin... [wp] Warning: Missing RTE guards -[wp] tests/wp_acsl/terminates_call_options.c:19: Warning: +[wp] tests/wp_acsl/terminates_call_options.c:20: Warning: Missing terminates clause for definition, populates 'terminates \true' -[wp] tests/wp_acsl/terminates_call_options.c:31: Warning: +[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:23: Warning: +[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:32: Warning: +[wp] tests/wp_acsl/terminates_call_options.c:33: Warning: Missing assigns clause (assigns 'everything' instead) -[wp] tests/wp_acsl/terminates_call_options.c:38: Warning: +[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:37: Warning: +[wp] tests/wp_acsl/terminates_call_options.c:38: Warning: Missing terminates clause on call to div, defaults to \true [wp] 5 goals scheduled [wp] [Qed] Goal typed_definition_assigns : Valid diff --git a/src/plugins/wp/tests/wp_acsl/terminates_call_options.c b/src/plugins/wp/tests/wp_acsl/terminates_call_options.c index d26bc0ac61d..7ccee59bcb1 100644 --- a/src/plugins/wp/tests/wp_acsl/terminates_call_options.c +++ b/src/plugins/wp/tests/wp_acsl/terminates_call_options.c @@ -9,8 +9,9 @@ #include <stdlib.h> -// -wp-external-declaration-terminates <--- default to FALSE -// -wp-definition-terminates <--- default to FALSE +// -wp-declarations-terminate <--- default to FALSE +// -wp-definitions-terminate <--- default to FALSE +// -wp-frama-c-stdlib-terminate <--- default to FALSE //@ assigns \nothing ; void declaration(void); -- GitLab