diff --git a/src/kernel_internals/typing/oneret.ml b/src/kernel_internals/typing/oneret.ml index e789fd76600c5ba79e5dede7e3253e075e634c82..b0cd7d596d53cccdc6ebe1d7eb5570103fe43831 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 694c59b9371b5017d9f40c1c03ebc92b02912f33..002354fe668613773fb9858468a214863d3cf9f6 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 eebfbb855dcededaf30827dd76a62c995e0e0e76..e1befb2ba50a9bd43fb801bd2a02c986e8a9b2be 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 0ead348826c41ca25cf5a2651ba6dee46193d46f..9a2f4f8338f820d8d2f5d506bce7b21b1347d035 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.