From fb42dae6d78704503674cc760376481abff8e307 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 31 Mar 2020 11:08:32 +0200
Subject: [PATCH] [ghost] Fixes error msg for ignored ghost-else
---
src/kernel_internals/parsing/cparser.mly | 4 +++-
tests/syntax/ghost_else_bad.c | 4 ++--
tests/syntax/oracle/ghost_else_bad.1.res.oracle | 2 ++
3 files changed, 7 insertions(+), 3 deletions(-)
diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly
index 73fd674857b..6f2547db91f 100644
--- a/src/kernel_internals/parsing/cparser.mly
+++ b/src/kernel_internals/parsing/cparser.mly
@@ -923,7 +923,9 @@ else_part:
%prec ghost_else_no_else /* To force the non ghost else to be attached to the current if */
| LGHOST_ELSE annotated_statement RGHOST ELSE annotated_statement
{
- Format.eprintf "Warning: %a: Invalid ghost else ignored@." Cil_datatype.Location.pretty $1 ;
+ let loc = Cil_datatype.Location.of_lexing_loc (Parsing.symbol_start_pos (), Parsing.symbol_end_pos ()) in
+ Kernel.warning ~wkey:Kernel.wkey_ghost_bad_use ~source:(fst loc)
+ "Invalid ghost else ignored@." ;
in_block $5
}
diff --git a/tests/syntax/ghost_else_bad.c b/tests/syntax/ghost_else_bad.c
index 8f6bf609bff..00a3bc684d1 100644
--- a/tests/syntax/ghost_else_bad.c
+++ b/tests/syntax/ghost_else_bad.c
@@ -1,6 +1,6 @@
/* run.config
OPT: -no-autoload-plugins -cpp-extra-args="-DERROR_LOC_WITH_COMMENTS"
- OPT: -no-autoload-plugins -cpp-extra-args="-DALREADY_HAS_ELSE" -print
+ OPT: -no-autoload-plugins -cpp-extra-args="-DALREADY_HAS_ELSE" -print -kernel-warn-key ghost:bad-use=feedback
OPT: -no-autoload-plugins -cpp-extra-args="-DBAD_ANNOT_POSITION"
*/
@@ -22,7 +22,7 @@ void if_ghost_else_block_comments_then_error(int x, int y) {
#endif
-#ifdef ALREADY_HAS_ELSE
+#ifdef ALREADY_HAS_ELSE
// Must warn that the ghost else cannot appear since there is already a else
// Thus the ghost else is ignored and the resulting code does not comprise it
diff --git a/tests/syntax/oracle/ghost_else_bad.1.res.oracle b/tests/syntax/oracle/ghost_else_bad.1.res.oracle
index fae04332c74..80c7b0204ac 100644
--- a/tests/syntax/oracle/ghost_else_bad.1.res.oracle
+++ b/tests/syntax/oracle/ghost_else_bad.1.res.oracle
@@ -1,4 +1,6 @@
[kernel] Parsing tests/syntax/ghost_else_bad.c (with preprocessing)
+[kernel:ghost:bad-use] tests/syntax/ghost_else_bad.c:32:
+ Invalid ghost else ignored
/* Generated by Frama-C */
void if_ghost_else_block_bad(int x, int y)
{
--
GitLab