From 5715c2fe48537fbfaa0a31fce5009eec0380f355 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 18 Feb 2020 18:49:27 +0100
Subject: [PATCH] [crowbar] again refine oracle
---
tests/crowbar/test_ghost_cfg.ml | 17 ++++++++++++++++-
1 file changed, 16 insertions(+), 1 deletion(-)
diff --git a/tests/crowbar/test_ghost_cfg.ml b/tests/crowbar/test_ghost_cfg.ml
index 45b2200aac3..1ae698b27bf 100644
--- a/tests/crowbar/test_ghost_cfg.ml
+++ b/tests/crowbar/test_ghost_cfg.ml
@@ -279,6 +279,8 @@ let ghost_case_breaks has_default other_cases =
method! vstmt s =
match s.skind with
| Break _ -> raise M.Has_break
+ | Loop _ | Switch _ -> (* a break there won't break the switch *)
+ Cil.SkipChildren
| _ -> Cil.DoChildren
end
in
@@ -288,6 +290,19 @@ let ghost_case_breaks has_default other_cases =
false
with M.Has_break -> true
+let rec no_ghost_case_breaks = function
+ | [] -> false (* should not happen, we have at least one non-ghost case before
+ default. *)
+ | stmts :: others ->
+ if (List.hd stmts).ghost then
+ begin
+ match (Extlib.last stmts).skind with
+ | Break _ -> false
+ | _ -> no_ghost_case_breaks others
+ end else true
+
+
+
let gen_case ghost should_break my_case cases env =
let (env,default,others) = cases env in
let ghost = ghost_status env ghost in
@@ -314,7 +329,7 @@ let gen_case ghost should_break my_case cases env =
| Case_no_default g1, (_, g2)::_ ->
(* fails iff switch is non-ghost, current case is, and doesn't break,
going to the next case. *)
- not g2 && g1 && not should_break
+ not g2 && g1 && not should_break && no_ghost_case_breaks others
| Case g1, (_,g2) :: _ ->
not g2 && g1 (* prevents taking the default clause.*)
in
--
GitLab