Commit 4d07e5a8 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'bugfix/v0.88' into next

parents f0929e1c 03e92b88
This diff is collapsed.
......@@ -1829,6 +1829,7 @@ Lemma nth_bit_pred_high :
to_uint i < size ->
to_uint i < Z.of_nat n ->
nth_bv (sub (lsl (of_int 1%Z) (Z.of_nat n)) (of_int 1%Z)) i = true.
Proof.
induction n;intros.
assert (Z.of_nat 0 <= to_uint i) by apply to_uint_bounds.
omega.
......@@ -1844,8 +1845,8 @@ Lemma nth_bit_pred_high :
case (Z_lt_le_dec (to_uint i) 1); intro.
right.
assert (to_uint i = 0).
pose (to_uint_bounds i).
auto with zarith.
assert (H' := to_uint_bounds i).
omega.
rewrite H1; apply nth_zeros_is_hd.
left.
......@@ -1933,10 +1934,11 @@ Lemma mask_correctness :
forall (j:Z),
(j < size -> (to_uint i) <= j -> j < (to_uint i + to_uint n)%Z -> nth mask j = true)
/\ (j < to_uint i \/ j >= to_uint i + to_uint n -> nth mask j = false).
Proof.
split;intros.
rewrite lsl_bv_is_lsl.
pose (to_uint_bounds i).
pose (size_in_range).
assert (a := to_uint_bounds i).
assert (u := size_in_range).
rewrite uint_in_range_power in u.
rewrite Lsl_nth_high; auto with zarith.
assert (j - to_uint i = to_uint (sub (of_int j) i)).
......@@ -1955,8 +1957,8 @@ Lemma mask_correctness :
apply Lsl_nth_low; auto with zarith.
rewrite lsl_bv_is_lsl.
pose (to_uint_bounds i) as u.
pose (to_uint_bounds n) as v.
assert (u := to_uint_bounds i).
assert (v := to_uint_bounds n).
pose size_in_range as w; rewrite uint_in_range_power in w.
assert (0 <= j) by auto with zarith.
......@@ -1983,6 +1985,7 @@ Qed.
(* Why3 goal *)
Lemma eq_sub_equiv : forall (a:t) (b:t) (i:t) (n:t), (eq_sub a b (to_uint i)
(to_uint n)) <-> (eq_sub_bv a b i n).
Proof.
intros a b i n.
unfold eq_sub, eq_sub_bv.
transitivity (eq_aux (bw_and b (lsl_bv (sub (lsl_bv (of_int 1) n) (of_int 1)) i))
......@@ -2007,7 +2010,7 @@ Lemma eq_sub_equiv : forall (a:t) (b:t) (i:t) (n:t), (eq_sub a b (to_uint i)
case (Z_lt_ge_dec j size); intro.
pose (to_uint_bounds i) as u; unfold uint_in_range in u.
assert (u := to_uint_bounds i); unfold uint_in_range in u.
assert (0 <= j < Z.of_nat size_nat) by auto with zarith.
pose (H j H1).
fold nth in e; rewrite Nth_bw_and, Nth_bw_and in e by auto.
......
[ATP alt-ergo]
name = "Alt-Ergo"
exec = "alt-ergo"
exec = "alt-ergo-2.2.0"
exec = "alt-ergo-2.0.0"
exec = "alt-ergo-1.30"
exec = "alt-ergo-1.01"
version_switch = "-version"
version_regexp = "^\\([0-9.]+\\)$"
version_ok = "2.0.0"
version_old = "1.30"
version_old = "1.30"
version_old = "1.01"
command = "%e -timelimit %t %f"
command_steps = "%e -steps-bound %S %f"
......@@ -528,6 +528,7 @@ compile_time_support = true
exec = "coqtop -batch"
version_switch = "-v"
version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
version_ok = "8.8.0"
version_ok = "^8\.7\.[0-2]$"
version_ok = "8.6.1"
version_ok = "8.6"
......
......@@ -166,33 +166,31 @@ let rec num_lines acc tr =
let rec print_transf fmt depth max_depth provers tr =
fprintf fmt "<tr>";
for _i=1 to 0 (* depth-1 *) do fprintf fmt "<td></td>" done;
fprintf fmt "<td style=\"background-color:#%a\" colspan=\"%d\">"
(color_of_status ~dark:false) (Opt.inhabited tr.S.transf_verified)
(max_depth - depth + 1);
(* for i=1 to depth-1 do fprintf fmt "&nbsp;&nbsp;&nbsp;&nbsp;" done; *)
fprintf fmt "%s</td>" tr.transf_name ;
for _i=1 (* depth *) to (*max_depth - 1 + *) List.length provers do
for _i=1 to List.length provers do
fprintf fmt "<td style=\"background-color:#E0E0E0\"></td>"
done;
fprintf fmt "</tr>@\n";
fprintf fmt "<tr><td rowspan=\"%d\">&nbsp;&nbsp;</td>" (num_lines 0 tr);
let nl = num_lines 0 tr in
if nl > 0 then begin
fprintf fmt "<tr><td rowspan=\"%d\">&nbsp;&nbsp;</td>" nl;
let (_:bool) = List.fold_left
(fun needs_tr g ->
print_goal fmt needs_tr (depth+1) max_depth provers g;
true)
false tr.transf_goals
in ()
end
and print_goal fmt needs_tr depth max_depth provers g =
if needs_tr then fprintf fmt "<tr>";
(* for i=1 to 0 (\* depth-1 *\) do fprintf fmt "<td></td>" done; *)
fprintf fmt "<td style=\"background-color:#%a\" colspan=\"%d\">"
(color_of_status ~dark:false) (Opt.inhabited (S.goal_verified g))
(max_depth - depth + 1);
(* for i=1 to depth-1 do fprintf fmt "&nbsp;&nbsp;&nbsp;&nbsp;" done; *)
fprintf fmt "%s</td>" (S.goal_user_name g);
(* for i=depth to max_depth-1 do fprintf fmt "<td></td>" done; *)
print_results fmt provers (goal_external_proofs g);
fprintf fmt "</tr>@\n";
PHstr.iter
......@@ -201,7 +199,7 @@ let rec num_lines acc tr =
let print_theory fn fmt th =
let depth = theory_depth th in
if depth > 0 then
if depth > 0 then begin
let provers = Hprover.create 9 in
provers_stats provers th;
let provers =
......@@ -224,13 +222,13 @@ let rec num_lines acc tr =
fprintf fmt "</span></h2>@\n";
fprintf fmt "<table border=\"1\"><tr><td colspan=\"%d\">Obligations</td>" depth;
(* fprintf fmt "<table border=\"1\"><tr><td>Obligations</td>"; *)
List.iter
(fun pr -> fprintf fmt "<td text-rotation=\"90\">%a</td>" print_prover pr)
provers;
fprintf fmt "</tr>@\n";
List.iter (print_goal fmt true 1 depth provers) th.theory_goals;
fprintf fmt "</table>@\n"
end
let print_file fmt f =
(* fprintf fmt "<h1>File %s</h1>@\n" f.file_name; *)
......
......@@ -612,6 +612,7 @@ theory SingleFull
clone export GenFloatSpecFull with
type t = single,
constant min = min_single,
constant max = max_single,
constant max_representable_integer = max_int
......@@ -627,6 +628,7 @@ theory DoubleFull
clone export GenFloatSpecFull with
type t = double,
constant min = min_double,
constant max = max_double,
constant max_representable_integer = max_int
......
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