summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-02 16:31:39 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-02 16:31:39 +0200
commit756c17d03b94919bfeaad55e2903e56dbac807bb (patch)
tree72f2405d6159a14817622dbd0291dc3781b1eb38
parentbc679afc4ac59c256a1b5f200078e495c188d066 (diff)
downloadscade-analyzer-756c17d03b94919bfeaad55e2903e56dbac807bb.tar.gz
scade-analyzer-756c17d03b94919bfeaad55e2903e56dbac807bb.zip
Add message when a step goes on BOT, ie. contradiction in assumes.
-rw-r--r--abstract/abs_interp.ml30
-rw-r--r--abstract/abs_interp_edd.ml33
2 files changed, 38 insertions, 25 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index 0db128f..c3db657 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -412,19 +412,23 @@ end = struct
let i = dd_singleton st.d_vars z in
let j = cycle st st.cl i in
- let cases = ref [] in
- Hashtbl.iter (fun case _ -> cases := case::(!cases)) j.data;
- List.iter
- (fun case ->
- let i' = set_target_case st i case in
- let j = cycle st st.cl i' in
- Hashtbl.iter (fun _ q -> add_case st q) j.data)
- !cases;
-
- st.delta <- List.filter ((<>) case) st.delta;
-
- if st.opt.verbose_ci then
- Format.printf "-> @[<hov>%a@]@." print_st st;
+ if Hashtbl.length j.data = 0 then
+ Format.printf "@.WARNING: contradictory hypotheses!@.@."
+ else begin
+ let cases = ref [] in
+ Hashtbl.iter (fun case _ -> cases := case::(!cases)) j.data;
+ List.iter
+ (fun case ->
+ let i' = set_target_case st i case in
+ let j = cycle st st.cl i' in
+ Hashtbl.iter (fun _ q -> add_case st q) j.data)
+ !cases;
+
+ st.delta <- List.filter ((<>) case) st.delta;
+
+ if st.opt.verbose_ci then
+ Format.printf "-> @[<hov>%a@]@." print_st st;
+ end
done;
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index cdcdab2..1eac551 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -946,17 +946,21 @@ end = struct
let d2 = edd_apply_cl x e.cl in
let dc = pass_cycle e d2 in
- let y = edd_star_new x (edd_accumulate e x dc) in
+ if dc.root = DBot then begin
+ Format.printf "@.WARNING: contradictory hypotheses!@.@.";
+ x
+ end else begin
+ let y = edd_star_new x (edd_accumulate e x dc) in
- if e.opt.vverbose_ci then
- Format.printf "d2 %a@. dc %a@. y %a@."
- edd_print d2 edd_print dc edd_print y;
-
- if e.opt.verbose_ci then
- Format.printf " -> %a@." edd_print y;
+ if e.opt.vverbose_ci then
+ Format.printf "d2 %a@. dc %a@. y %a@."
+ edd_print d2 edd_print dc edd_print y;
- if not (edd_eq x y) then ch_it (n+1) y else y
+ if e.opt.verbose_ci then
+ Format.printf " -> %a@." edd_print y;
+ if not (edd_eq x y) then ch_it (n+1) y else y
+ end
| Some i ->
let path = edd_extract_path x i in
let x = edd_unstar x i in
@@ -993,12 +997,17 @@ end = struct
let fj = pass_cycle e (edd_apply_cl z e.cl) in
- let r = edd_star_new x (edd_accumulate e x fj) in
+ if fj.root = DBot then begin
+ Format.printf "@.WARNING: contradictory hypotheses!@.@.";
+ x
+ end else begin
+ let r = edd_star_new x (edd_accumulate e x fj) in
- if e.opt.verbose_ci then
- Format.printf " -> %a@." edd_print r;
+ if e.opt.verbose_ci then
+ Format.printf " -> %a@." edd_print r;
- ch_it (n+1) r
+ ch_it (n+1) r
+ end
in
let init_acc = edd_star_new (edd_bot e.data.ve) e.data in