From 8dfb226aef3b45108695e782b3f3af7e77b848e1 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 18 Feb 2020 15:04:15 +0100
Subject: [PATCH] [kernel] Ghost_cfg do not share visited stmts when CFGs can
be shared
---
src/kernel_internals/typing/ghost_cfg.ml | 7 +++++--
tests/cil/ghost_cfg.c | 10 ++++++++++
tests/cil/oracle/ghost_cfg.0.res.oracle | 3 +++
tests/cil/oracle/ghost_cfg.1.res.oracle | 2 +-
4 files changed, 19 insertions(+), 3 deletions(-)
diff --git a/src/kernel_internals/typing/ghost_cfg.ml b/src/kernel_internals/typing/ghost_cfg.ml
index d86eae1f0ae..c94252aec4d 100644
--- a/src/kernel_internals/typing/ghost_cfg.ml
+++ b/src/kernel_internals/typing/ghost_cfg.ml
@@ -114,8 +114,8 @@ let alteredCFG stmt =
let checkGhostCFG bhv withGhostStart noGhost =
let rec do_check visited withGhostStart noGhostStart =
match (nextSync withGhostStart), (nextSync noGhostStart) with
- | Stmt withGhost, Stmt _ when StmtSet.mem withGhost visited -> visited
| Stmt withGhost, Stmt noGhost ->
+ let is_visited = StmtSet.mem withGhost visited in
let visited = StmtSet.add withGhost visited in
let withGhost =
StmtSet.contains_single_elt (nextNonGhostSync withGhost)
@@ -124,6 +124,9 @@ let checkGhostCFG bhv withGhostStart noGhost =
| Some s1, s2 when not (Stmt.equal s1 (Get_orig.stmt bhv s2)) ->
alteredCFG withGhostStart ; visited
+ (* Note: this test is deferred so that bad stmts are detected above *)
+ | Some _, _ when is_visited -> visited
+
| Some ({ skind = If(_) } as withGhost), noGhost ->
let wgThen, wgElse = Cil.separate_if_succs withGhost in
let ngThen, ngElse = Cil.separate_if_succs noGhost in
@@ -141,7 +144,7 @@ let checkGhostCFG bhv withGhostStart noGhost =
let visited = List.fold_left2 do_check visited wgSuccsNG ngSuccs in
List.fold_left (fun v s -> do_check v s ngDef) visited mustDefault
- | Some ({ skind=Loop(_,wgb,_,_,_) }), { skind=Loop (_, ngb,_,_,_) } ->
+ | Some ({ skind=Loop(_,wgb,_,_,_) }), { skind=Loop (_,ngb,_,_,_) } ->
begin match wgb.bstmts, ngb.bstmts with
| s1 :: _ , s2 :: _ -> do_check visited s1 s2
| _, _ -> visited
diff --git a/tests/cil/ghost_cfg.c b/tests/cil/ghost_cfg.c
index 002354fe668..2ba5406612e 100644
--- a/tests/cil/ghost_cfg.c
+++ b/tests/cil/ghost_cfg.c
@@ -109,6 +109,16 @@ int ghost_return() {
return 0;
}
+void shared_cfgs(int x) {
+ switch (x) {
+ /*@ ghost case 3: ; */
+ case 2: ;
+ x = 5;
+ default: ;
+ x ++;
+ }
+}
+
#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 c4bf9a5dc2d..9b3c7cfa41c 100644
--- a/tests/cil/oracle/ghost_cfg.0.res.oracle
+++ b/tests/cil/oracle/ghost_cfg.0.res.oracle
@@ -26,5 +26,8 @@
Ghost code breaks CFG starting at:
/*@ ghost __retres = 1; */
/*@ ghost goto return_label; */
+[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:114: Warning:
+ Ghost code breaks CFG starting at:
+ /*@ ghost case 3: ; */
[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 9a2f4f8338f..3248acc0fd5 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:117: User Error:
+[kernel] tests/cil/ghost_cfg.c:127: 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