Skip to content
Snippets Groups Projects
Commit e028702c authored by Patrick Baudin's avatar Patrick Baudin
Browse files

[wp] improves is_cint_simplifier

parent d985937a
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 344 additions and 518 deletions
src/plugins/wp/Cint.ml
+ 273
− 155
View file @ e028702c
......@@ -815,177 +815,295 @@ let c_int_bounds_ival f =
let max_reduce_quantifiers = 1000
(** We know that t is a predicate which is the opened body of a forall *)
let reduce_bound v tv dom t : term =
let module Exc = struct
exception True
exception False
exception Unknown of Integer.t
end in
try
let red i () =
match repr (QED.e_subst_var v (e_zint i) t) with
| True -> ()
| False -> raise Exc.False
| _ -> raise (Exc.Unknown i) in
let min_bound = try
Ival.fold_int red dom (); raise Exc.True
with Exc.Unknown i -> i in
let max_bound = try
Ival.fold_int_decrease red dom (); raise Exc.True
with Exc.Unknown i -> i in
(** we try to reduce the bounds of the domains, when trivially false *)
let dom_red = Ival.inject_range (Some min_bound) (Some max_bound) in
assert ( Ival.is_included dom_red dom);
if Ival.equal dom_red dom
then t
else
(e_imply [e_leq (e_zint min_bound) tv;
e_leq tv (e_zint max_bound)]
t)
with
| Exc.True -> e_true
| Exc.False -> e_false
module Polarity = struct
type t = Pos | Neg | Both
let flip = function | Pos -> Neg | Neg -> Pos | Both -> Both
let from_bool = function | false -> Neg | true -> Pos
end
let is_cint_simplifier = object (self)
module Dom = struct
type t = Ival.t Tmap.t
let is_top_ival = Ival.equal Ival.top
val mutable domain : Ival.t Tmap.t = Tmap.empty
let top = Tmap.empty
method private print fmt =
let print fmt dom =
Tmap.iter (fun k v ->
Format.fprintf fmt "%a: %a,@ " Lang.F.pp_term k Ival.pretty v)
domain
method name = "Remove redundant is_cint"
method copy = {< domain = domain >}
method private narrow_dom t v =
domain <-
Tmap.change (fun _ p ->
function
| None -> Some p
| Some old -> Some (Ival.narrow p old))
t v domain
method assume p =
let rec aux t =
match Lang.F.repr t with
| _ when not (is_prop t) -> ()
| Fun(g,[a]) ->
begin try
let ubound = c_int_bounds_ival (is_cint g) in
self#narrow_dom a ubound
with Not_found -> ()
dom
let find t dom = Tmap.find t dom
let get t dom = try find t dom with Not_found -> Ival.top
let narrow t v dom =
if Ival.is_bottom v then raise Lang.Contradiction
else if is_top_ival v then dom
else Tmap.change (fun _ v old ->
match old with | None -> Some v
| (Some old) as old' ->
let v = Ival.narrow v old in
if Ival.is_bottom v then raise Lang.Contradiction;
if Ival.equal v old then old'
else Some v) t v dom
let add t v dom =
if Ival.is_bottom v then raise Lang.Contradiction;
if is_top_ival v then dom else Tmap.add t v dom
let remove t dom = Tmap.remove t dom
let assume_cmp =
let module Local = struct
type t = Integer of Ival.t | Term of Ival.t option
end in fun cmp t1 t2 dom ->
let encode t = match Lang.F.repr t with
| Kint z -> Local.Integer (Ival.inject_singleton z)
| _ -> Local.Term (try Some (Tmap.find t dom) with Not_found -> None)
in
let term_dom = function
| Some v -> v
| None -> Ival.top
in
match encode t1, encode t2 with
| Local.Integer cst1, Local.Integer cst2 -> (* assume cmp cst1 cst2 *)
if Abstract_interp.Comp.False = Ival.forward_comp_int cmp cst1 cst2
then raise Lang.Contradiction;
dom
| Local.Term None, Local.Term None ->
dom (* nothing can be collected *)
| Local.Term opt1, Local.Integer cst2 ->
let v1 = term_dom opt1 in
add t1 (Ival.backward_comp_int_left cmp v1 cst2) dom
| Local.Integer cst1, Local.Term opt2 ->
let v2 = term_dom opt2 in
let cmp_sym = Abstract_interp.Comp.sym cmp in
add t2 (Ival.backward_comp_int_left cmp_sym v2 cst1) dom
| Local.Term opt1, Local.Term opt2 ->
let v1 = term_dom opt1 in
let v2 = term_dom opt2 in
let cmp_sym = Abstract_interp.Comp.sym cmp in
add t1 (Ival.backward_comp_int_left cmp v1 v2)
(add t2 (Ival.backward_comp_int_left cmp_sym v2 v1) dom)
let assume_literal t dom = match Lang.F.repr t with
| Eq(a,b) -> assume_cmp Abstract_interp.Comp.Eq a b dom
| Leq(a,b) -> assume_cmp Abstract_interp.Comp.Le a b dom
| Lt(a,b) -> assume_cmp Abstract_interp.Comp.Lt a b dom
| Fun(g,[a]) -> begin try
let ubound =
c_int_bounds_ival (is_cint g) (* may raise Not_found *) in
narrow a ubound dom
with Not_found -> dom
end
| Not p -> begin match Lang.F.repr p with
| Fun(g,[a]) -> begin try (* just checks for a contraction *)
let ubound =
c_int_bounds_ival (is_cint g) (* may raise Not_found *) in
let v = find a dom (* may raise Not_found *) in
if Ival.is_included v ubound then raise Lang.Contradiction;
dom
with Not_found -> dom
end
| And _ -> Lang.F.QED.f_iter aux t
| _ -> ()
| _ -> dom
end
| _ -> dom
end
let is_cint_simplifier =
let reduce_bound ~add_bonus quant v tv dom t : term =
(** Returns [new_t] such that [c_bind quant (alpha,t)]
equals [c_bind quant v (alpha,new_t)]
under the knowledge that [(not t) ==> (var in dom)].
Note: [~add_bonus] has not effect on the correctness of the transformation.
It is a parameter that can be used in order to get better results.
Bonus: Add additionnal hypothesis when we could deduce better constraint
on the variable *)
let module Tool = struct
exception Stop
exception Empty
exception Unknown of Integer.t
type t = { when_empty: unit -> term;
add_hyp: term list -> term -> term;
when_true: bool ref -> unit;
when_false: bool ref -> unit;
when_stop: unit -> term;
}
end in
let tools = Tool.(match quant with
| Forall -> { when_empty=(fun () -> e_true);
add_hyp =(fun hyps t -> e_imply hyps t);
when_true=(fun bonus -> bonus := add_bonus);
when_false=(fun _ -> raise Stop);
when_stop=(fun () -> e_false);
}
| Exists ->{ when_empty= (fun () -> e_false);
add_hyp =(fun hyps t -> e_and (t::hyps));
when_true=(fun _ -> raise Stop);
when_false=(fun bonus -> bonus := add_bonus);
when_stop=(fun () -> e_true);
}
| _ -> assert false)
in
aux (Lang.F.e_prop p)
if Vars.mem v (vars t) then try
let bonus_min = ref false in
let bonus_max = ref false in
let dom = if Ival.cardinal_is_less_than dom max_reduce_quantifiers then
(* try to reduce the domain when [var] is still in [t] *)
let red reduced i () =
match repr (QED.e_subst_var v (e_zint i) t) with
| True -> tools.Tool.when_true reduced
| False -> tools.Tool.when_false reduced
| _ -> raise (Tool.Unknown i) in
let min_bound = try Ival.fold_int (red bonus_min) dom ();
raise Tool.Empty with Tool.Unknown i -> i in
let max_bound = try Ival.fold_int_decrease (red bonus_max) dom ();
raise Tool.Empty with Tool.Unknown i -> i in
let red_dom = Ival.inject_range (Some min_bound) (Some max_bound) in
Ival.narrow dom red_dom
else dom
in begin match Ival.min_and_max dom with
| None, None -> t (* Cannot be reduced *)
| Some min, None -> (* May be reduced to [min ...] *)
if !bonus_min then tools.Tool.add_hyp [e_leq (e_zint min) tv] t
else t
| None, Some max -> (* May be reduced to [... max] *)
if !bonus_max then tools.Tool.add_hyp [e_leq tv (e_zint max)] t
else t
| Some min, Some max ->
if Integer.equal min max then (* Reduced to only one value: [min] *)
QED.e_subst_var v (e_zint min) t
else if Integer.lt min max then
let h = if !bonus_min then [e_leq (e_zint min) tv] else []
in
let h = if !bonus_max then (e_leq tv (e_zint max))::h else h
in tools.Tool.add_hyp h t
else assert false (* Abstract_interp.Error_Bottom raised *)
end
with
| Tool.Stop -> tools.Tool.when_stop ()
| Tool.Empty -> tools.Tool.when_empty ()
| Abstract_interp.Error_Bottom -> tools.Tool.when_empty ()
| Abstract_interp.Error_Top -> t
else (* [alpha] is no more in [t] *)
if Ival.is_bottom dom then tools.Tool.when_empty () else t
in
let module Polarity = struct
type t = Pos | Neg | Both
let flip = function | Pos -> Neg | Neg -> Pos | Both -> Both
let from_bool = function | false -> Neg | true -> Pos
end
in object (self)
method target _ = ()
method fixpoint = ()
val mutable domain : Dom.t = Dom.top
method private simplify ~is_goal p =
let pool = Lang.get_pool () in
method name = "Remove redundant is_cint"
method copy = {< domain = domain >}
let reduce op var_domain base =
let dom =
match Lang.F.repr base with
| Kint z -> Ival.inject_singleton z
| _ ->
try Tmap.find base domain
with Not_found -> Ival.top
method target _ = ()
method fixpoint = ()
method assume p =
Lang.iter_confident_literals
(fun p -> domain <- Dom.assume_literal p domain) (Lang.F.e_prop p)
method private simplify ~is_goal p =
let pool = Lang.get_pool () in
let reduce op var_domain base =
let dom =
match Lang.F.repr base with
| Kint z -> Ival.inject_singleton z
| _ ->
try Tmap.find base domain
with Not_found -> Ival.top
in
var_domain := Ival.backward_comp_int_left op !var_domain dom
in
var_domain := Ival.backward_comp_int_left op !var_domain dom
in
let rec reduce_on_neg var var_domain t =
match Lang.F.repr t with
| _ when not (is_prop t) -> ()
| Leq(a,b) when Lang.F.equal a var ->
reduce Abstract_interp.Comp.Le var_domain b
| Leq(b,a) when Lang.F.equal a var ->
reduce Abstract_interp.Comp.Ge var_domain b
| Lt(a,b) when Lang.F.equal a var ->
reduce Abstract_interp.Comp.Lt var_domain b
| Lt(b,a) when Lang.F.equal a var ->
reduce Abstract_interp.Comp.Gt var_domain b
| And l -> List.iter (reduce_on_neg var var_domain) l
| _ -> ()
in
let reduce_on_pos var var_domain t =
match Lang.F.repr t with
| Imply (l,_) -> List.iter (reduce_on_neg var var_domain) l
| _ -> ()
in
let rec walk ~term_pol t =
let walk_flip_pol t = walk ~term_pol:(Polarity.flip term_pol) t
and walk_same_pol t = walk ~term_pol t
and walk_both_pol t = walk ~term_pol:Polarity.Both t
let rec reduce_on_neg var var_domain t =
match Lang.F.repr t with
| _ when not (is_prop t) -> ()
| Leq(a,b) when Lang.F.equal a var ->
reduce Abstract_interp.Comp.Le var_domain b
| Leq(b,a) when Lang.F.equal a var ->
reduce Abstract_interp.Comp.Ge var_domain b
| Lt(a,b) when Lang.F.equal a var ->
reduce Abstract_interp.Comp.Lt var_domain b
| Lt(b,a) when Lang.F.equal a var ->
reduce Abstract_interp.Comp.Gt var_domain b
| And l -> List.iter (reduce_on_neg var var_domain) l
| Not p -> reduce_on_pos var var_domain p
| _ -> ()
and reduce_on_pos var var_domain t =
match Lang.F.repr t with
| Neq _ | Leq _ | Lt _ -> reduce_on_neg var var_domain (e_not t)
| Imply (l,p) -> List.iter (reduce_on_neg var var_domain) l;
reduce_on_pos var var_domain p
| Or l -> List.iter (reduce_on_pos var var_domain) l;
| Not p -> reduce_on_neg var var_domain p
| _ -> ()
in
match repr t with
| _ when not (is_prop t) -> t
| Bind((Forall|Exists),_,_) ->
let ctx,t = e_open ~pool ~lambda:false t in
let ctx_with_dom =
List.map (fun ((quant,var) as qv) -> match tau_of_var var with
| Int ->
let tvar = (e_var var) in
let var_domain = ref Ival.top in
if quant = Forall
then reduce_on_pos tvar var_domain t
else reduce_on_neg tvar var_domain t;
domain <- Tmap.add tvar !var_domain domain;
qv, Some (tvar, var_domain)
| _ -> qv, None) ctx
in
let t = walk_same_pol t in
let f_close t = function
| (quant,var), None -> e_bind quant var t
| (quant,var), Some (tvar,var_domain) ->
domain <- Tmap.remove tvar domain;
(** Bonus: Add additionnal hypothesis in forall when we could deduce
better constraint on the variable *)
let t = if quant = Forall &&
term_pol = Polarity.Pos &&
Ival.cardinal_is_less_than !var_domain max_reduce_quantifiers
then reduce_bound var tvar !var_domain t
else t in
e_bind quant var t
in
List.fold_left f_close t ctx_with_dom
| Fun(g,[a]) ->
(** Here we simplifies the cints which are redoundant *)
begin try
let ubound = c_int_bounds_ival (is_cint g) in
let dom = (Tmap.find a domain) in
if Ival.is_included dom ubound
then e_true
else t
with Not_found -> t
end
| Imply (l1,l2) -> e_imply (List.map walk_flip_pol l1) (walk_same_pol l2)
| Not p -> e_not (walk_flip_pol p)
| And _ | Or _ -> Lang.F.QED.f_map walk_same_pol t
| _ ->
Lang.F.QED.f_map ~pool ~forall:false ~exists:false walk_both_pol t in
Lang.F.p_bool (walk ~term_pol:(Polarity.from_bool is_goal) (Lang.F.e_prop p))
(* [~term_pol] gives the polarity of the term [t] from the top level.
That informs about how should be considered the quantifiers
of [t]
*)
let rec walk ~term_pol t =
let walk_flip_pol t = walk ~term_pol:(Polarity.flip term_pol) t
and walk_same_pol t = walk ~term_pol t
and walk_both_pol t = walk ~term_pol:Polarity.Both t
in
match repr t with
| _ when not (is_prop t) -> t
| Bind((Forall|Exists),_,_) ->
let ctx,t = e_open ~pool ~lambda:false t in
let ctx_with_dom =
List.map (fun ((quant,var) as qv) -> match tau_of_var var with
| Int ->
let tvar = (e_var var) in
let var_domain = ref Ival.top in
if quant = Forall
then reduce_on_pos tvar var_domain t
else reduce_on_neg tvar var_domain t;
domain <- Dom.add tvar !var_domain domain;
qv, Some (tvar, var_domain)
| _ -> qv, None) ctx
in
let t = walk_same_pol t in
let f_close t = function
| (quant,var), None -> e_bind quant var t
| (quant,var), Some (tvar,var_domain) ->
domain <- Dom.remove tvar domain;
(** Bonus: Add additionnal hypothesis in forall when we could deduce
better constraint on the variable *)
let add_bonus = match term_pol with
| Polarity.Both -> false
| _ -> (term_pol=Polarity.Pos) = (quant=Forall)
in
let t = reduce_bound ~add_bonus quant var tvar !var_domain t in
e_bind quant var t
in
List.fold_left f_close t ctx_with_dom
| Fun(g,[a]) ->
(** Here we simplifies the cints which are redoundant *)
begin try
let ubound = c_int_bounds_ival (is_cint g) in
let dom = (Tmap.find a domain) in
if Ival.is_included dom ubound
then e_true
else t
with Not_found -> t
end
| Imply (l1,l2) -> e_imply (List.map walk_flip_pol l1) (walk_same_pol l2)
| Not p -> e_not (walk_flip_pol p)
| And _ | Or _ -> Lang.F.QED.f_map walk_same_pol t
| _ ->
Lang.F.QED.f_map ~pool ~forall:false ~exists:false walk_both_pol t in
Lang.F.p_bool (walk ~term_pol:(Polarity.from_bool is_goal) (Lang.F.e_prop p))
method simplify_exp (e : term) = e
method simplify_exp (e : term) = e
method simplify_hyp p = self#simplify ~is_goal:false p
method simplify_hyp p = self#simplify ~is_goal:false p
method simplify_goal p = self#simplify ~is_goal:true p
method simplify_goal p = self#simplify ~is_goal:true p
method simplify_branch p = p
method simplify_branch p = p
method infer = []
end
method infer = []
end
let mask_simplifier =
......
src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle
+ 3
− 6
View file @ e028702c
......@@ -165,20 +165,17 @@ Prove: exists i : Z. forall i_1 : Z. (is_uint8(i_1) ->
------------------------------------------------------------
Goal Check 'ko,Let1,intro_let' (file tests/wp_acsl/simpl_is_type.i, line 92):
Prove: exists i : Z. forall i_1 : Z. ((10 <= i_1) -> ((i_1 <= 10) ->
P_P(i_1, i, 1.0))).
Prove: exists i : Z. P_P(10, i, 1.0).
------------------------------------------------------------
Goal Check 'ko,Let2,intro_let' (file tests/wp_acsl/simpl_is_type.i, line 93):
Prove: exists i : Z. forall i_1 : Z. ((i_1 <= 0) -> ((0 <= i_1) ->
(((-5) <= i_1) -> P_P(i_1, i, 1.0)))).
Prove: exists i : Z. P_P(0, i, 1.0).
------------------------------------------------------------
Goal Check 'ko,Let3,intro_let' (file tests/wp_acsl/simpl_is_type.i, line 94):
Prove: exists i : Z. forall i_1 : Z. ((255 <= i_1) -> ((i_1 <= 255) ->
((i_1 <= 599) -> P_P(i_1, i, 1.0)))).
Prove: exists i : Z. P_P(255, i, 1.0).
------------------------------------------------------------
......
src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle
+ 6
− 6
View file @ e028702c
......@@ -11,7 +11,7 @@
[wp] [Qed] Goal typed_main_requires_qed_ok_Struct_Simple_a : Valid
[wp] [Qed] Goal typed_main_requires_qed_ok_Struct_Simple_b : Valid
[wp] [Qed] Goal typed_main_requires_qed_ok_Simple_Array_0 : Valid
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_Simple_Array_1 : Valid
[wp] [Qed] Goal typed_main_requires_qed_ok_Simple_Array_1 : Valid
[wp] [Qed] Goal typed_main_requires_qed_ok_With_Array_Struct_5 : Valid
[wp] [Qed] Goal typed_main_requires_qed_ok_With_Array_Struct_3 : Valid
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_Sc_eq : Valid
......@@ -25,19 +25,19 @@
[wp] [Qed] Goal typed_main_requires_qed_ok_2 : Valid
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_3 : Valid
[wp] [Qed] Goal typed_main_requires_qed_ok_todo : Valid
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_4 : Valid
[wp] [Qed] Goal typed_main_requires_qed_ok_4 : Valid
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_5 : Valid
[wp] [Qed] Goal typed_main_requires_qed_ok_direct_init_union : Valid
[wp] Proved goals: 24 / 24
Qed: 17
Alt-Ergo: 7
Qed: 19
Alt-Ergo: 5
[wp] Report in: 'tests/wp_acsl/oracle_qualif/init_value.0.report.json'
[wp] Report out: 'tests/wp_acsl/result_qualif/init_value.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
main 14 6 (28..40) 20 100%
main 16 4 (28..40) 20 100%
fa1 1 - 1 100%
fa2 1 - 1 100%
fa3 1 - 1 100%
fs1 - 1 (160..184) 1 100%
fs1 - 1 (112..136) 1 100%
-------------------------------------------------------------
src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
+ 1
− 3
View file @ e028702c
......@@ -172,9 +172,7 @@ Assume {
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
((m[i_1].F1_T_a) = 0))).
(* Call Effects *)
Have: (forall i_1 : Z. ((i_1 != 1) -> (smatrix_1[i_1] = smatrix_0[i_1]))) /\
(forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
(((i_1 < 0) \/ (5 <= i_1)) -> (smatrix_1[1][i_1] = m[i_1]))))).
Have: forall i_1 : Z. ((i_1 != 1) -> (smatrix_1[i_1] = smatrix_0[i_1])).
}
Prove: (m[i].F1_T_a) = 0.
......
src/plugins/wp/tests/wp_hoare/oracle/reference_array.res.oracle
+ 4
− 11
View file @ e028702c
......@@ -230,9 +230,7 @@ Assume {
(* Call 'reset_5' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) -> (m[i_1] = 0))).
(* Call Effects *)
Have: (forall i_1 : Z. ((i_1 != 0) -> (tt_0[i_1] = tt_1[i_1]))) /\
(forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
(((i_1 < 0) \/ (5 <= i_1)) -> (m_1[i_1] = m[i_1]))))).
Have: forall i_1 : Z. ((i_1 != 0) -> (tt_0[i_1] = tt_1[i_1])).
(* Call 'add_5' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
(reg_add_0[i_1] = (reg_load_0[i_1] + m[i_1])))).
......@@ -243,19 +241,16 @@ Prove: m_1[i] = reg_load_0[i].
Goal Post-condition 'Preset' in 'calls_on_array_dim_2_to_1':
Let m = tt_0[0].
Let m_1 = tt_1[0].
Assume {
(* Goal *)
When: (0 <= i) /\ (i <= 4).
(* Call 'load_5' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
(m_1[i_1] = reg_load_0[i_1]))).
(tt_1[0][i_1] = reg_load_0[i_1]))).
(* Call 'reset_5' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) -> (m[i_1] = 0))).
(* Call Effects *)
Have: (forall i_1 : Z. ((i_1 != 0) -> (tt_1[i_1] = tt_0[i_1]))) /\
(forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
(((i_1 < 0) \/ (5 <= i_1)) -> (m_1[i_1] = m[i_1]))))).
Have: forall i_1 : Z. ((i_1 != 0) -> (tt_1[i_1] = tt_0[i_1])).
(* Call 'add_5' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
(reg_add_0[i_1] = (reg_load_0[i_1] + m[i_1])))).
......@@ -276,9 +271,7 @@ Assume {
(* Call 'reset_5' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) -> (m[i_1] = 0))).
(* Call Effects *)
Have: (forall i_1 : Z. ((i_1 != 0) -> (tt_0[i_1] = tt_1[i_1]))) /\
(forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
(((i_1 < 0) \/ (5 <= i_1)) -> (m_1[i_1] = m[i_1]))))).
Have: forall i_1 : Z. ((i_1 != 0) -> (tt_0[i_1] = tt_1[i_1])).
(* Call 'add_5' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 4) ->
(reg_add_0[i_1] = (reg_load_0[i_1] + m[i_1])))).
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
+ 1
− 1
View file @ e028702c
......@@ -110,7 +110,7 @@ Functions WP Alt-Ergo Total Success
init 6 4 (80..104) 10 100%
init_t1 6 4 (12..24) 10 100%
init_t2_v1 9 8 (40..52) 17 100%
init_t2_v2 9 8 (32..44) 17 100%
init_t2_v2 9 8 (24..36) 17 100%
init_t2_v3 7 8 (28..40) 15 100%
init_t2_bis_v1 7 4 (208..256) 11 100%
init_t2_bis_v2 7 4 (192..240) 11 100%
......
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