Commit 76a31a83 authored by Allan Blanchard's avatar Allan Blanchard

[wp] Removed option -wp-bits (now always enabled)

parent de09f05c
......@@ -24,6 +24,8 @@
Plugin WP <next-release>
#########################
- WP [2020-XX-XX] Removed option -wp-bits (now always enabled)
#########################
Plugin WP 22.0 (Titanium)
#########################
......
......@@ -800,41 +800,40 @@ type l_builtin = {
let () =
Context.register
begin fun () ->
if Wp_parameters.Bits.get () then
begin
let mk_builtin n f ?eq ?leq smp = n, { f ; eq; leq; smp } in
(* From [smp_mk_bit_stdlib], the built-in [f_bit_stdlib] is such that there is
no creation of [e_fun f_bit_stdlib args] *)
let bi_lbit_stdlib = mk_builtin "f_bit_stdlib" f_bit_stdlib smp_mk_bit_stdlib in
let bi_lbit = mk_builtin "f_bit" f_bit_positive smp_bitk_positive in
let bi_lnot = mk_builtin "f_lnot" f_lnot ~eq:smp_eq_with_lnot
(smp1 Integer.lognot) in
let bi_lxor = mk_builtin "f_lxor" f_lxor ~eq:smp_eq_with_lxor
(smp2 f_lxor Integer.logxor) in
let bi_lor = mk_builtin "f_lor" f_lor ~eq:smp_eq_with_lor
(smp2 f_lor Integer.logor) in
let bi_land = mk_builtin "f_land" f_land ~eq:smp_eq_with_land ~leq:smp_leq_with_land
smp_land in
let bi_lsl = mk_builtin "f_lsl" f_lsl ~eq:smp_eq_with_lsl ~leq:smp_leq_with_lsl
(smp_shift Integer.shift_left) in
let bi_lsr = mk_builtin "f_lsr" f_lsr ~eq:smp_eq_with_lsr ~leq:smp_leq_with_lsr
(smp_shift Integer.shift_right) in
List.iter
begin fun (_name, { f; eq; leq; smp }) ->
F.set_builtin f smp ;
(match eq with
| None -> ()
| Some eq -> F.set_builtin_eq f eq);
(match leq with
| None -> ()
| Some leq -> F.set_builtin_leq f leq)
end
[bi_lbit_stdlib ; bi_lbit; bi_lnot; bi_lxor; bi_lor; bi_land; bi_lsl; bi_lsr];
begin
let mk_builtin n f ?eq ?leq smp = n, { f ; eq; leq; smp } in
(* From [smp_mk_bit_stdlib], the built-in [f_bit_stdlib] is such that there is
no creation of [e_fun f_bit_stdlib args] *)
let bi_lbit_stdlib = mk_builtin "f_bit_stdlib" f_bit_stdlib smp_mk_bit_stdlib in
let bi_lbit = mk_builtin "f_bit" f_bit_positive smp_bitk_positive in
let bi_lnot = mk_builtin "f_lnot" f_lnot ~eq:smp_eq_with_lnot
(smp1 Integer.lognot) in
let bi_lxor = mk_builtin "f_lxor" f_lxor ~eq:smp_eq_with_lxor
(smp2 f_lxor Integer.logxor) in
let bi_lor = mk_builtin "f_lor" f_lor ~eq:smp_eq_with_lor
(smp2 f_lor Integer.logor) in
let bi_land = mk_builtin "f_land" f_land ~eq:smp_eq_with_land ~leq:smp_leq_with_land
smp_land in
let bi_lsl = mk_builtin "f_lsl" f_lsl ~eq:smp_eq_with_lsl ~leq:smp_leq_with_lsl
(smp_shift Integer.shift_left) in
let bi_lsr = mk_builtin "f_lsr" f_lsr ~eq:smp_eq_with_lsr ~leq:smp_leq_with_lsr
(smp_shift Integer.shift_right) in
List.iter
begin fun (_name, { f; eq; leq; smp }) ->
F.set_builtin f smp ;
(match eq with
| None -> ()
| Some eq -> F.set_builtin_eq f eq);
(match leq with
| None -> ()
| Some leq -> F.set_builtin_leq f leq)
end
[bi_lbit_stdlib ; bi_lbit; bi_lnot; bi_lxor; bi_lor; bi_land; bi_lsl; bi_lsr];
Lang.For_export.set_builtin_eq f_land export_eq_with_land
end
Lang.For_export.set_builtin_eq f_land export_eq_with_land
end
end
(* ACSL Semantics *)
......
......@@ -543,13 +543,6 @@ module Prenex =
let help = "Normalize nested foralls into prenex-form"
end)
let () = Parameter_customize.set_group wp_simplifier
module Bits =
True(struct
let option_name = "-wp-bits"
let help = "Use bit-test simplifications."
end)
let () = Parameter_customize.set_group wp_simplifier
module SimplifyIsCint =
True(struct
......
......@@ -85,7 +85,6 @@ module Clean: Parameter_sig.Bool
module Filter: Parameter_sig.Bool
module Parasite: Parameter_sig.Bool
module Prenex: Parameter_sig.Bool
module Bits: Parameter_sig.Bool
module Ground: Parameter_sig.Bool
module Reduce: Parameter_sig.Bool
module ExtEqual : Parameter_sig.Bool
......
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