Commit fdd2a762 authored by Loïc Correnson's avatar Loïc Correnson

Merge branch 'feature/blanchard/wp/remove-bits-option' into 'master'

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

Closes #225

See merge request frama-c/frama-c!2930
parents 81629a4d 76a31a83
...@@ -24,6 +24,8 @@ ...@@ -24,6 +24,8 @@
Plugin WP <next-release> Plugin WP <next-release>
######################### #########################
- WP [2020-XX-XX] Removed option -wp-bits (now always enabled)
######################### #########################
Plugin WP 22.0 (Titanium) Plugin WP 22.0 (Titanium)
######################### #########################
......
...@@ -800,41 +800,40 @@ type l_builtin = { ...@@ -800,41 +800,40 @@ type l_builtin = {
let () = let () =
Context.register Context.register
begin fun () -> begin fun () ->
if Wp_parameters.Bits.get () then begin
begin let mk_builtin n f ?eq ?leq smp = n, { f ; eq; leq; smp } in
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
(* 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] *)
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_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_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
let bi_lnot = mk_builtin "f_lnot" f_lnot ~eq:smp_eq_with_lnot (smp1 Integer.lognot) in
(smp1 Integer.lognot) in let bi_lxor = mk_builtin "f_lxor" f_lxor ~eq:smp_eq_with_lxor
let bi_lxor = mk_builtin "f_lxor" f_lxor ~eq:smp_eq_with_lxor (smp2 f_lxor Integer.logxor) in
(smp2 f_lxor Integer.logxor) in let bi_lor = mk_builtin "f_lor" f_lor ~eq:smp_eq_with_lor
let bi_lor = mk_builtin "f_lor" f_lor ~eq:smp_eq_with_lor (smp2 f_lor Integer.logor) in
(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
let bi_land = mk_builtin "f_land" f_land ~eq:smp_eq_with_land ~leq:smp_leq_with_land smp_land in
smp_land in let bi_lsl = mk_builtin "f_lsl" f_lsl ~eq:smp_eq_with_lsl ~leq:smp_leq_with_lsl
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
(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
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
(smp_shift Integer.shift_right) in
List.iter
List.iter begin fun (_name, { f; eq; leq; smp }) ->
begin fun (_name, { f; eq; leq; smp }) -> F.set_builtin f smp ;
F.set_builtin f smp ; (match eq with
(match eq with | None -> ()
| None -> () | Some eq -> F.set_builtin_eq f eq);
| Some eq -> F.set_builtin_eq f eq); (match leq with
(match leq with | None -> ()
| None -> () | Some leq -> F.set_builtin_leq f leq)
| Some leq -> F.set_builtin_leq f leq) end
end [bi_lbit_stdlib ; bi_lbit; bi_lnot; bi_lxor; bi_lor; bi_land; bi_lsl; bi_lsr];
[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 Lang.For_export.set_builtin_eq f_land export_eq_with_land
end end
end end
(* ACSL Semantics *) (* ACSL Semantics *)
......
...@@ -543,13 +543,6 @@ module Prenex = ...@@ -543,13 +543,6 @@ module Prenex =
let help = "Normalize nested foralls into prenex-form" let help = "Normalize nested foralls into prenex-form"
end) 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 let () = Parameter_customize.set_group wp_simplifier
module SimplifyIsCint = module SimplifyIsCint =
True(struct True(struct
......
...@@ -85,7 +85,6 @@ module Clean: Parameter_sig.Bool ...@@ -85,7 +85,6 @@ module Clean: Parameter_sig.Bool
module Filter: Parameter_sig.Bool module Filter: Parameter_sig.Bool
module Parasite: Parameter_sig.Bool module Parasite: Parameter_sig.Bool
module Prenex: Parameter_sig.Bool module Prenex: Parameter_sig.Bool
module Bits: Parameter_sig.Bool
module Ground: Parameter_sig.Bool module Ground: Parameter_sig.Bool
module Reduce: Parameter_sig.Bool module Reduce: Parameter_sig.Bool
module ExtEqual : 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