From 9948f28ca94cd1ce6159ab9630914d060dc5fad1 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 17 Feb 2020 14:14:50 +0100
Subject: [PATCH] [kernel] fix ghost status of goto generated by oneret
transformation
---
src/kernel_internals/typing/oneret.ml | 2 +-
tests/cil/ghost_cfg.c | 6 ++++++
tests/cil/oracle/ghost_cfg.0.res.oracle | 4 ++++
tests/cil/oracle/ghost_cfg.1.res.oracle | 2 +-
4 files changed, 12 insertions(+), 2 deletions(-)
diff --git a/src/kernel_internals/typing/oneret.ml b/src/kernel_internals/typing/oneret.ml
index e789fd76600..b0cd7d596d5 100644
--- a/src/kernel_internals/typing/oneret.ml
+++ b/src/kernel_internals/typing/oneret.ml
@@ -373,7 +373,7 @@ let oneret ?(callback: callback option) (f: fundec) : unit =
the statement contract(s) will apply.
*)
let sgref = ref (getRetStmt ()) in
- let sg = mkStmt (Goto (sgref, loc)) in
+ let sg = mkStmt ~ghost:s.ghost (Goto (sgref, loc)) in
haveGoto := true;
let b_stmts =
match !returns_assert with
diff --git a/tests/cil/ghost_cfg.c b/tests/cil/ghost_cfg.c
index 694c59b9371..002354fe668 100644
--- a/tests/cil/ghost_cfg.c
+++ b/tests/cil/ghost_cfg.c
@@ -103,6 +103,12 @@ void switch_loses_assertion (int c) {
return;
}
+int ghost_return() {
+ // the following ghost statement makes the function returning 1 instead of 0
+ //@ ghost return 1;
+ return 0;
+}
+
#endif
#ifdef CANT_CHECK
diff --git a/tests/cil/oracle/ghost_cfg.0.res.oracle b/tests/cil/oracle/ghost_cfg.0.res.oracle
index eebfbb855dc..e1befb2ba50 100644
--- a/tests/cil/oracle/ghost_cfg.0.res.oracle
+++ b/tests/cil/oracle/ghost_cfg.0.res.oracle
@@ -22,5 +22,9 @@
[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:100: Warning:
Ghost code breaks CFG starting at:
case 1: /*@ ghost x ++; */
+[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:108: Warning:
+ Ghost code breaks CFG starting at:
+ /*@ ghost __retres = 1; */
+ /*@ ghost goto return_label; */
[kernel] Warning: warning ghost:bad-use treated as deferred error. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/cil/oracle/ghost_cfg.1.res.oracle b/tests/cil/oracle/ghost_cfg.1.res.oracle
index 0ead348826c..9a2f4f8338f 100644
--- a/tests/cil/oracle/ghost_cfg.1.res.oracle
+++ b/tests/cil/oracle/ghost_cfg.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/cil/ghost_cfg.c (with preprocessing)
-[kernel] tests/cil/ghost_cfg.c:111: User Error:
+[kernel] tests/cil/ghost_cfg.c:117: User Error:
'goto X;' would jump from normal statement to ghost code
[kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
--
GitLab