Maj terminée. Pour consulter la release notes associée voici le lien :
https://about.gitlab.com/releases/2021/07/07/critical-security-release-gitlab-14-0-4-released/

Commit f314e026 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Fix incorrect use of i_degree by plot.

parent 6d2b8ec4
Pipeline #244594 passed with stages
in 19 minutes and 46 seconds
......@@ -403,7 +403,7 @@ Ltac unify_eq native :=
end
end.
Ltac plot1_aux1 prec x1 x2 w h native tac_b :=
Ltac plot1_aux1 prec x1 x2 w h d native tac_b :=
let x1 := reify x1 constr:(@nil R) in
let x2 := reify x2 constr:(@nil R) in
let ox := eval vm_compute in (I.lower (T.eval_bnd prec x1)) in
......@@ -431,20 +431,20 @@ Ltac plot1_aux1 prec x1 x2 w h native tac_b :=
let y1y2 := tac_b prec ox dx w in
let thr := eval vm_compute in (F.div_UP prec (F.sub_UP prec (snd y1y2) (fst y1y2)) (F.fromZ_DN prec (Zpos h))) in
apply (sample_plot_correct prec) with
(deg := 10%nat) (nb := w) (l := p)
(deg := d) (nb := w) (l := p)
(check := fun yi => F'.le' (F.sub_UP prec (I.upper yi) (I.lower yi)) thr)
(1 := I.singleton_correct ox)
(2 := I.singleton_correct dx) ;
unify_eq native
end.
Ltac plot2_aux prec x1 x2 w native tac_t tac_b :=
Ltac plot2_aux prec x1 x2 w d native tac_t tac_b :=
match goal with
| |- plot2 ?f ?ox ?dx ?oy' ?dy' (Zpos ?h) ?p2 =>
let p1 := fresh "__p1" in
evar (p1 : list I.type) ;
let Hp := fresh "__Hp" in
assert (Hp: plot1 f ox dx p1) by plot1_aux1 prec x1 x2 w h native tac_t ;
assert (Hp: plot1 f ox dx p1) by plot1_aux1 prec x1 x2 w h d native tac_t ;
revert Hp ;
let y1y2 := tac_b prec in
let oy := constr:(fst y1y2) in
......@@ -487,7 +487,7 @@ Ltac do_plot f x1 x2 prec degree width height native :=
let p := fresh "__p2" in
evar (p : list (Z * Z)) ;
refine (_: plot2 f _ _ _ _ (Zpos height) p) ;
plot2_aux prec x1 x2 width native plot_get_threshold plot_get_bounds.
plot2_aux prec x1 x2 width degree native plot_get_threshold plot_get_bounds.
Ltac do_plot_y f x1 x2 y1 y2 prec degree width height native :=
let p := fresh "__p2" in
......@@ -497,6 +497,6 @@ Ltac do_plot_y f x1 x2 y1 y2 prec degree width height native :=
let y2 := eval vm_compute in (I.upper (T.eval_bnd prec y2)) in
evar (p : list (Z * Z)) ;
refine (_: plot2 f _ _ _ _ (Zpos height) p) ;
plot2_aux prec x1 x2 width native ltac:(plot_y_get_threshold y1 y2) ltac:(plot_y_get_bounds y1 y2).
plot2_aux prec x1 x2 width degree native ltac:(plot_y_get_threshold y1 y2) ltac:(plot_y_get_bounds y1 y2).
End PlotTacticAux.
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