From 33ae18312f14de1e72970ccacb645c3d84b61d86 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 6 Feb 2020 15:16:02 +0100
Subject: [PATCH] [ghost] Take care of assertions when checking CFG
---
src/kernel_internals/typing/ghost_cfg.ml | 19 ++++++++++++++++---
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, 30 insertions(+), 4 deletions(-)
diff --git a/src/kernel_internals/typing/ghost_cfg.ml b/src/kernel_internals/typing/ghost_cfg.ml
index 997a7564318..13eef5e3004 100644
--- a/src/kernel_internals/typing/ghost_cfg.ml
+++ b/src/kernel_internals/typing/ghost_cfg.ml
@@ -29,6 +29,14 @@ module StmtSet = Stmt.Hptset
let error = Kernel.warning ~wkey:Kernel.wkey_ghost_bad_use
+
+let annot_attr = "has_annot"
+
+(* For no ghost project, we add an attribute each stmt that has annotations. *)
+let has_annot stmt =
+ Annotations.code_annot stmt <> [] ||
+ Cil.hasAttribute annot_attr stmt.sattr
+
let noGhostBlock b =
let noGhostVisitor = object (self)
inherit genericCilVisitor (refresh (Project.current()))
@@ -44,10 +52,15 @@ let noGhostBlock b =
end else
begin match s.skind with
| Switch(e, block, cases, loc) ->
- let cases = List.filter (fun s -> not (self#original s).ghost) cases in
+ let cases = List.filter
+ (fun s -> not (self#original s).ghost) cases
+ in
s.skind <- Switch(e, block, cases, loc) ;
DoChildren
- | _ -> DoChildren
+ | _ ->
+ let original = self#original s in
+ s.sattr <- if has_annot original then [AttrAnnot annot_attr] else [] ;
+ DoChildren
end
method getBehavior () = self#behavior
@@ -62,7 +75,7 @@ type follower =
let sync stmt =
match stmt.skind with
(* We ignore blocks: their successors are their 1st stmt so we visit them *)
- | Instr(Skip(_)) | Block(_) | Continue(_) | Break(_) -> false
+ | Instr(Skip(_)) | Block(_) | Continue(_) | Break(_) -> has_annot stmt
| _ -> true
let nextSync stmt =
diff --git a/tests/cil/ghost_cfg.c b/tests/cil/ghost_cfg.c
index a2faa9ed8c4..694c59b9371 100644
--- a/tests/cil/ghost_cfg.c
+++ b/tests/cil/ghost_cfg.c
@@ -93,6 +93,16 @@ int ghost_goto_ghost(){
return 0;
}
+void switch_loses_assertion (int c) {
+ //@ ghost int x = 1;
+ switch (c) {
+ case 0: return;
+ //@ ghost case 1: x++; /*@ assert x == 2; */ break;
+ default: /*@ assert x == 1; */ break;
+ }
+ return;
+}
+
#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 66c3a703667..eebfbb855dc 100644
--- a/tests/cil/oracle/ghost_cfg.0.res.oracle
+++ b/tests/cil/oracle/ghost_cfg.0.res.oracle
@@ -19,5 +19,8 @@
[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:89: Warning:
Ghost code breaks CFG starting at:
/*@ ghost goto X; */
+[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:100: Warning:
+ Ghost code breaks CFG starting at:
+ case 1: /*@ ghost x ++; */
[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 286d7589654..0ead348826c 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:101: User Error:
+[kernel] tests/cil/ghost_cfg.c:111: 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