Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Bug fix: report not_precise when a value cannot be rounded

parent b6578c9a
......@@ -9,3 +9,37 @@
contents u < length a) /\
0 <= contents l
###
### Debug: inferred invariants ###
(((contents l1 <= 0 /\ length a1 <= (1 + contents u1)) /\ contents l1 = 0 \/
(((((((2 <= length a1 /\ 3 <= (length a1 + contents l1)) /\ 0 < contents l1) /\
contents l1 < length a1) /\
2 <= (length a1 + contents u1)) /\
contents l1 <= (1 + contents u1)) /\
0 < (contents l1 + contents u1)) /\
0 <= contents u1) /\
(contents u1 + 2) <= length a1 \/
((((((((0 < length a1 /\ 0 < (length a1 + contents l1)) /\
contents l1 < length a1) /\
contents l1 <= 0) /\
0 <= (length a1 + contents u1)) /\
contents l1 <= (1 + contents u1)) /\
0 <= (1 + (contents l1 + contents u1))) /\
0 <= (1 + contents u1)) /\
(contents u1 + 2) <= length a1) /\
contents l1 = 0 \/
(((((((0 < length a1 /\ 2 <= (length a1 + contents l1)) /\ 0 < contents l1) /\
contents l1 <= length a1) /\
length a1 <= (1 + contents u1)) /\
0 < (length a1 + contents u1)) /\
contents l1 <= (1 + contents u1)) /\
0 < (contents l1 + contents u1)) /\
0 <= contents u1) /\
contents u1 < length a1) /\
0 <= contents l1
###
### Debug: inferred invariants ###
(((0 = contents l2 /\ contents l2 = 0 \/ 0 < contents l2 /\ 0 <= contents u2) /\
1 = 1) /\
0 = 0) /\
0 <= contents l2
###
......@@ -225,12 +225,14 @@ module Make_from_apron(M:sig
done;
!vars
exception Not_int
let rec int_of_s s =
let open Apron.Scalar in
match s with
| Float f ->
let i = int_of_float f in
assert (float_of_int i = f);
if float_of_int i <> f then raise Not_int;
i
| Mpqf t ->
int_of_s (Float (Mpqf.to_float t))
......@@ -249,8 +251,7 @@ module Make_from_apron(M:sig
if not (Coeff.equal_int (Lincons1.get_cst l) 0) then
begin
let i = Lincons1.get_cst l |> function
| Coeff.Scalar s ->
int_of_s s
| Coeff.Scalar s -> int_of_s s
| _ -> assert false
in
let l' = Lincons1.copy l in
......@@ -307,38 +308,34 @@ module Make_from_apron(M:sig
else if typ = Lincons1.SUPEQ then [Lincons1.SUP, -1]
else assert false
in
precise := !precise && begin
List.fold_left (fun p (ty, new_coeff) ->
p &&
let cp = Lincons1.copy line in
let cst = Lincons1.get_cst cp in
let cst =
if new_coeff = -1 then
Coeff.neg cst
else if new_coeff = 1 then
cst
else
assert false in
Lincons1.set_cst cp cst;
Lincons1.set_typ cp ty;
Lincons1.iter (fun coeff var ->
let coeff =
if new_coeff = -1 then
Coeff.neg coeff
else if new_coeff = 1 then
coeff
else
assert false in
Lincons1.set_coeff cp var coeff) line;
let a = Lincons1.array_make (Lincons1.get_env cp) 1 in
Lincons1.array_set a 0 cp;
let new_c = meet_lincons_array man c a in
let new_c = round_integers man (Lincons1.get_env cp) new_c in
is_leq man new_c b) true opp_typ
end;
let aux p (ty, new_coeff) = p &&
let cp = Lincons1.copy line in
let cst = Lincons1.get_cst cp in
let cst =
if new_coeff = -1 then Coeff.neg cst
else if new_coeff = 1 then cst
else assert false in
Lincons1.set_cst cp cst;
Lincons1.set_typ cp ty;
Lincons1.iter (fun coeff var ->
let coeff =
if new_coeff = -1 then Coeff.neg coeff
else if new_coeff = 1 then coeff
else assert false in
Lincons1.set_coeff cp var coeff) line;
let a = Lincons1.array_make (Lincons1.get_env cp) 1 in
Lincons1.array_set a 0 cp;
let new_c = meet_lincons_array man c a in
begin
try
let new_c = round_integers man (Lincons1.get_env cp) new_c in
is_leq man new_c b
with Not_int -> false
end
in
precise := !precise && List.fold_left aux true opp_typ;
done;
if !precise then Some c
else None
if !precise then Some c else None
end
......
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