Skip to content

GitLab

why3
why3
Commit 4a9f618e authored by Cláudio Belo Lourenço's avatar Cláudio Belo Lourenço
Browse files
Options

Bug fix: ignore domain's constraints containing apron variables not mapped to Why3 terms

parent cda26419
Hide whitespace changes
Inline Side-by-side
Showing with 109 additions and 97 deletions
bench/infer/auto_array1.oracle
View file @ 4a9f618e
### Debug: inferred invariants ###
(((((forall w1:int.
w1 < 0 \/ 2 = (elts a @ w1) /\ (elts a @ w1) = 2 \/ x <= w1) /\
w1 < 0 \/
2 = (elts a @ w1) /\ (elts a @ w1) = 2 \/ length (make x 2) <= w1) /\
length (make x 2) = length a) /\
x = length a) /\
2 = 2) /\
x = length a) /\
x = length (make x 2)
length (make x 2) = x) /\
length (make x 2) = length a
###
### Debug: inferred invariants ###
(((forall w2:int.
((((w2 < 0 /\ x1 <= length (make x1 2)) /\
length a1 <= length (make x1 2)) /\
length (make x1 2) <= x1) /\
length (make x1 2) <= length a1) /\
((((w2 < 0 /\ length (make x1 2) <= x1) /\ x1 <= length (make x1 2)) /\
length (make x1 2) <= length a1) /\
length a1 <= length (make x1 2)) /\
length (make x1 2) = length a1 \/
(((x1 <= x1 /\ 2 <= (elts a1 @ w2)) /\ (elts a1 @ w2) <= 2) /\
((((2 <= (elts a1 @ w2) /\ (elts a1 @ w2) <= 2) /\ x1 <= x1) /\ x1 <= x1) /\
length (make x1 (elts a1 @ w2)) = length a1) /\
(elts a1 @ w2) = 2 \/
((((((x1 <= w2 /\ length a1 <= w2) /\ x1 <= length (make x1 2)) /\
length a1 <= length (make x1 2)) /\
length (make x1 2) <= w2) /\
length (make x1 2) <= x1) /\
length (make x1 2) <= length a1) /\
((((((length (make x1 2) <= w2 /\ length (make x1 2) <= x1) /\
x1 <= length (make x1 2)) /\
x1 <= w2) /\
length (make x1 2) <= length a1) /\
length a1 <= length (make x1 2)) /\
length a1 <= w2) /\
length (make x1 2) = length a1) /\
x1 = length a1) /\
length a1 <= x1) /\
......@@ -32,67 +33,76 @@ x1 <= length a1
###
### Debug: inferred invariants ###
(((((((((forall w4:int.
w4 < 0 \/ 10 = (elts a3 @ w4) /\ (elts a3 @ w4) = 10 \/ n <= w4) /\
w4 < 0 \/
10 = (elts a3 @ w4) /\ (elts a3 @ w4) = 10 \/
length (make n 10) <= w4) /\
(elts a3 @ 5) = b) /\
5 = 5) /\
length (make n 10) = length a3) /\
n = length a3) /\
10 = 10) /\
0 <= n) /\
b = (elts a3 @ 5)) /\
n = length a3) /\
n = length (make n 10)
0 <= length (make n 10)) /\
(elts a3 @ 5) = b) /\
length (make n 10) = n) /\
length (make n 10) = length a3
###
### Debug: inferred invariants ###
(((((((((forall w5:int.
((((((((((w5 < 0 /\ w5 < n1) /\ w5 < length a4) /\
w5 < length (make n1 10)) /\
n1 <= length (make n1 10)) /\
0 <= (n1 + length (make n1 10))) /\
length a4 <= length (make n1 10)) /\
0 <= (length a4 + length (make n1 10))) /\
0 <= length (make n1 10)) /\
length (make n1 10) <= n1) /\
length (make n1 10) <= length a4) /\
((((((((((0 <= length (make n1 10) /\ w5 < length (make n1 10)) /\
w5 < 0) /\
length (make n1 10) <= n1) /\
0 <= (length (make n1 10) + n1)) /\
w5 < n1) /\
n1 <= length (make n1 10)) /\
length (make n1 10) <= length a4) /\
0 <= (length (make n1 10) + length a4)) /\
w5 < length a4) /\
length a4 <= length (make n1 10)) /\
length (make n1 10) = length a4 \/
((((((((((((n1 <= n1 /\ 0 <= (n1 + n1)) /\ 0 <= (length a4 + n1)) /\
n1 <= n1) /\
10 <= (n1 + (elts a4 @ w5))) /\
10 <= (length a4 + (elts a4 @ w5))) /\
10 <= (n1 + (elts a4 @ w5))) /\
10 <= (elts a4 @ w5)) /\
(elts a4 @ w5) <= (10 + n1)) /\
(elts a4 @ w5) <= (10 + length a4)) /\
(elts a4 @ w5) <= (10 + n1)) /\
(elts a4 @ w5) <= 10) /\
(((((((((((10 <= (n1 + (elts a4 @ w5)) /\ 10 <= (elts a4 @ w5)) /\
(elts a4 @ w5) <= (10 + n1)) /\
(elts a4 @ w5) <= 10) /\
n1 <= n1) /\
0 <= (n1 + n1)) /\
(elts a4 @ w5) <= (10 + n1)) /\
10 <= ((elts a4 @ w5) + n1)) /\
n1 <= n1) /\
(elts a4 @ w5) <= (10 + length a4)) /\
10 <= ((elts a4 @ w5) + length a4)) /\
length (make n1 (elts a4 @ w5)) = length a4) /\
(elts a4 @ w5) = 10 \/
(((((((((((((0 <= w5 /\ 0 <= (w5 + n1)) /\ n1 <= w5) /\
0 <= (w5 + length a4)) /\
length a4 <= w5) /\
0 <= (w5 + length (make n1 10))) /\
n1 <= length (make n1 10)) /\
0 <= (n1 + length (make n1 10))) /\
length a4 <= length (make n1 10)) /\
0 <= (length a4 + length (make n1 10))) /\
0 <= length (make n1 10)) /\
length (make n1 10) <= w5) /\
length (make n1 10) <= n1) /\
length (make n1 10) <= length a4) /\
(((((((((((((0 <= length (make n1 10) /\ length (make n1 10) <= w5) /\
0 <= (length (make n1 10) + w5)) /\
0 <= w5) /\
length (make n1 10) <= n1) /\
0 <= (length (make n1 10) + n1)) /\
0 <= (w5 + n1)) /\
n1 <= length (make n1 10)) /\
n1 <= w5) /\
length (make n1 10) <= length a4) /\
0 <= (length (make n1 10) + length a4)) /\
0 <= (w5 + length a4)) /\
length a4 <= length (make n1 10)) /\
length a4 <= w5) /\
length (make n1 10) = length a4) /\
(elts a4 @ 5) = b1) /\
n1 = length a4) /\
(elts a4 @ 5) <= b1) /\
b1 <= (elts a4 @ 5)) /\
length a4 <= n1) /\
0 <= length a4) /\
0 <= (n1 + length a4)) /\
n1 <= length a4) /\
length a4 <= n1) /\
0 <= length a4) /\
0 <= (n1 + length a4)) /\
n1 <= length a4) /\
b1 <= (elts a4 @ 5)) /\
(elts a4 @ 5) <= b1) /\
0 <= n1
###
### Debug: inferred invariants ###
(((((length (make n2 10) = length a5 /\ n2 = length a5) /\ 10 = 10) /\ 5 = 5) /\
(elts a5 @ 5) = b2) /\
(((((((forall w6:int.
w6 < 0 \/ 10 = (elts a5 @ w6) /\ (elts a5 @ w6) = 10 \/ 0 <= w6) /\
(elts a5 @ 5) = b2) /\
5 = 5) /\
length (make n2 10) = length a5) /\
n2 = length a5) /\
10 = 10) /\
0 <= length a5) /\
0 <= n2
###
bench/infer/mccarthy.oracle
View file @ 4a9f618e
......@@ -83,10 +83,7 @@
contents e5 = 1 \/
(3 <= contents e5 /\ contents n5 <= 111) /\ 11 = 11 \/
((2 = contents e5 /\ contents n5 <= 111) /\ 2 = contents e5) /\ 11 = 11 \/
91 <= contents n5 /\ 10 = 10 \/
((((0 < o66 /\ o66 < 0) /\ 3 <= contents e5) /\ 23 <= contents n5) /\
contents n5 <= 21) /\
10 = 10) /\
91 <= contents n5 /\ 10 = 10) /\
1 = 1) /\
0 <= contents e5
###
bench/infer/mult.oracle
View file @ 4a9f618e
### Debug: inferred invariants ###
(0 = contents i /\ contents i = 0 \/
((contents i = (2 * (2 * 0)) /\ (2 * 0) <= 9) /\ (2 * (2 * 0)) = contents i) /\
(((2 * (2 * 0)) = contents i /\ (2 * 0) <= 9) /\ (2 * (2 * 0)) = contents i) /\
2 = 2 \/
((2 * 0) <= 9 /\ (2 * (2 * 0)) <= 9) /\ 2 = 2 \/
(contents i = (2 * 0) /\ (2 * 0) = contents i) /\ 2 = 2 \/
(2 * 0) = contents i /\ 2 = 2 \/
((2 * 0) <= 9 /\ (2 * (2 * 0)) <= 9) /\ 2 = 2 \/
((2 * 0) <= 9 /\ (2 * (2 * 0)) <= 9) /\ 2 = 2) /\
0 = 0
......@@ -14,9 +14,9 @@ forall w2:int.
((((2 * 0) <= 9 /\ ((2 * 0) + (2 * (2 * 0))) <= 18) /\ (2 * (2 * 0)) <= 9) /\
contents i1 <= contents i1) /\
contents i1 <= contents i1 \/
(contents i1 <= (2 * 0) /\ (2 * 0) <= contents i1) /\ (2 * 0) = contents i1 \/
(((2 * 0) <= 9 /\ contents i1 <= (2 * (2 * 0))) /\
(2 * (2 * 0)) <= contents i1) /\
((2 * 0) <= contents i1 /\ contents i1 <= (2 * 0)) /\ (2 * 0) = contents i1 \/
(((2 * 0) <= 9 /\ (2 * (2 * 0)) <= contents i1) /\
contents i1 <= (2 * (2 * 0))) /\
(2 * (2 * 0)) = contents i1
###
### Debug: inferred invariants ###
......
bench/infer/uf6.oracle
View file @ 4a9f618e
### Debug: inferred invariants ###
(((((_2 = 5 /\ ll _1 = 0) /\ 0 = 0) /\ 0 <= contents k) /\ contents k <= 3) /\
5 = _2) /\
0 = ll _1
0 = ll _1) /\
5 = _2
###
### Debug: inferred invariants ###
((((((((((((((((((_6 = 5 /\ ll _5 = 0) /\ ll _5 <= 0) /\ ll _5 <= contents k1) /\
(contents k1 + ll _5) <= 3) /\
(ll _5 + 5) <= _6) /\
(_6 + ll _5) <= 5) /\
0 <= ll _5) /\
0 <= (contents k1 + ll _5)) /\
contents k1 <= (3 + ll _5)) /\
5 <= (_6 + ll _5)) /\
_6 <= (5 + ll _5)) /\
contents k1 <= 3) /\
(contents k1 + 2) <= _6) /\
(_6 + contents k1) <= 8) /\
0 <= contents k1) /\
5 <= (_6 + contents k1)) /\
_6 <= (5 + contents k1)) /\
_6 <= 5) /\
5 <= _6
((((((((((((((((((_6 = 5 /\ ll _5 = 0) /\ contents k1 <= 3) /\
(contents k1 + 2) <= _6) /\
(_6 + contents k1) <= 8) /\
contents k1 <= (3 + ll _5)) /\
(ll _5 + contents k1) <= 3) /\
0 <= contents k1) /\
5 <= (_6 + contents k1)) /\
_6 <= (5 + contents k1)) /\
0 <= (ll _5 + contents k1)) /\
ll _5 <= contents k1) /\
_6 <= 5) /\
_6 <= (5 + ll _5)) /\
(ll _5 + _6) <= 5) /\
5 <= _6) /\
5 <= (ll _5 + _6)) /\
(ll _5 + 5) <= _6) /\
ll _5 <= 0) /\
0 <= ll _5
###
### Debug: inferred invariants ###
(((((((0 = contents k2 /\ contents k2 = 0 \/
......@@ -28,8 +29,8 @@
_10 = 5) /\
ll _9 = 0) /\
0 = 0) /\
0 = ll _9) /\
contents k2 <= 3) /\
0 <= contents k2) /\
5 = _10
contents k2 <= 3) /\
0 <= contents k2) /\
5 = _10) /\
0 = ll _9
###
src/infer/domain.ml
View file @ 4a9f618e
......@@ -175,8 +175,12 @@ module Make_from_apron(M:sig
let n = Lincons1.array_length l in
let t = ref (Term.t_true) in
for i = 0 to n - 1 do
let v = lincons_to_term (Lincons1.array_get l i) variable_mapping in
t := t_and_simp !t v;
try
(* Sometimes Apron inserts variables that are not
referrenced and that are not mapped to Why3 terms. *)
let v = lincons_to_term (Lincons1.array_get l i) variable_mapping in
t := t_and_simp !t v
with Not_found -> ()
done;
!t
in
......
src/infer/uf_domain.ml
View file @ 4a9f618e
......@@ -629,7 +629,7 @@ module Make(S:sig
if Ty.ty_equal (t_type t) ty_int ||
Ty.ty_equal (t_type t) ty_bool then begin
let reg_name =
Format.asprintf "%d%a" !var_id Pretty.print_term t in
Format.asprintf "z%d%a" !var_id Pretty.print_term t in
let v = Var.of_string reg_name in
assert (not (Environment.mem_var uf_man.env v));
ensure_variable uf_man v t;
......@@ -638,7 +638,7 @@ module Make(S:sig
else
let subv = get_subvalues t None in
let name_var t1 t2 =
Format.asprintf "%d%a.%a"
Format.asprintf "z%d%a.%a"
!var_id Pretty.print_term t1 Pretty.print_term t2 in
List.iter (fun (t2, _) ->
let v = Var.of_string (name_var t t2) in
......@@ -670,13 +670,13 @@ module Make(S:sig
match pv.pv_ity.ity_node, (t_type pv_t).ty_node with
| _ when Ty.ty_equal (t_type pv_t) ty_int ->
let reg_name =
Format.asprintf "%d%a" !var_id print_term pv_t in
Format.asprintf "z%d%a" !var_id print_term pv_t in
let v = Var.of_string reg_name in
assert (not (Environment.mem_var uf_man.env v));
ensure_variable uf_man v pv_t;
uf_man.apron_mapping <- Mterm.add pv_t v uf_man.apron_mapping
| _ when Ty.ty_equal (t_type pv_t) ty_bool ->
let reg_name = Format.asprintf "%d%a" !var_id print_term pv_t in
let reg_name = Format.asprintf "z%d%a" !var_id print_term pv_t in
let v = Var.of_string reg_name in
assert (not (Environment.mem_var uf_man.env v));
ensure_variable uf_man v pv_t;
......@@ -688,7 +688,7 @@ module Make(S:sig
let subv_pv = get_subvalues pv_t (Some reg.reg_its) in
let proj_list =
List.fold_left2 (fun acc (t_reg, rs) (t_pv, _) ->
let name = Format.asprintf "r$%a.%a" print_reg_name reg
let name = Format.asprintf "zr$%a.%a" print_reg_name reg
print_term t_reg in
let var = Var.of_string name in
ensure_variable uf_man var t_pv;
......@@ -708,7 +708,7 @@ module Make(S:sig
| Ityapp _, _ ->
let subv = get_subvalues pv_t None in
List.iter (fun (t, _) ->
let name = Format.asprintf "%d%a.%a" !var_id
let name = Format.asprintf "z%d%a.%a" !var_id
print_pv pv print_term t in
let var = Var.of_string name in
ensure_variable uf_man var t;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment