diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 092c6039c77899f16c43862f59dccac0949fc8b3..40a333d4f62eaffcb04c379cb0a17d4b9daf48d9 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -1018,6 +1018,7 @@ module RteGen = struct
let get_unsignedDownCast_status = mk_fun "RteGen.get_unsignedDownCast_status"
let get_float_to_int_status = mk_fun "RteGen.get_float_to_int_status"
let get_finite_float_status = mk_fun "RteGen.get_finite_float_status"
+ let get_bool_value_status = mk_fun "RteGen.get_bool_value_status"
end
module PostdominatorsTypes = struct
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index 873a8c6eb4b31069846a9cead7452983943d2d76..10d1ff2e5404069f08ab1be8b998e20e5adc355f 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -896,6 +896,7 @@ module RteGen : sig
val get_unsignedDownCast_status : (unit -> status_accessor) ref
val get_float_to_int_status : (unit -> status_accessor) ref
val get_finite_float_status : (unit -> status_accessor) ref
+ val get_bool_value_status : (unit -> status_accessor) ref
end
diff --git a/src/plugins/rte/register.ml b/src/plugins/rte/register.ml
index 99e58a483d2556e4764d4e538a57dacac76ac0b1..20fd2a12824fd6dfbf1451168346f9c24e903d3d 100644
--- a/src/plugins/rte/register.ml
+++ b/src/plugins/rte/register.ml
@@ -95,6 +95,7 @@ let () =
nojournal_register get_unsignedDownCast_status Unsigned_downcast.accessor;
nojournal_register get_float_to_int_status Float_to_int.accessor;
nojournal_register get_finite_float_status Finite_float.accessor;
+ nojournal_register get_bool_value_status Bool_value.accessor ;
nojournal_register get_all_status all_statuses;
;;
diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml
index 33aeb7f6e7ddefbf1c12b08819c420c089b2fb48..664c6cce8929d7a36618b53fc429e11033cf2c19 100644
--- a/src/plugins/rte/visit.ml
+++ b/src/plugins/rte/visit.ml
@@ -445,7 +445,8 @@ let annotate ?flags kf =
comp Unsigned_overflow.accessor flags.unsigned_overflow |||
comp Unsigned_downcast.accessor flags.unsigned_downcast |||
comp Float_to_int.accessor flags.float_to_int |||
- comp Finite_float.accessor flags.finite_float
+ comp Finite_float.accessor flags.finite_float |||
+ comp Bool_value.accessor flags.bool_value
then begin
Options.feedback "annotating function %a" Kernel_function.pretty kf;
let warn = Options.Warn.get () in
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 60844cd373c47d043f1eec8643ecc8a6bb88df39..1bbd1d8265a90f971c869754a33f6d6ccca4c435 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -20,6 +20,8 @@
# <Prover>: prover
###############################################################################
+ - Wp [2019/04/26] Now requires -warn-invalid-bool
+ - Wp [2019/04/26] Removed option -wp-bool-range
- Wp [2019/04/24] Support for Why3 1.* and Coq 8.{7-9}
- Wp [2019/02/26] Support for @check ACSL annotations
- WP [2018/02/16] Filter out some variables from separation
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index 02c88290a4e5bf52db262ee8661d51cce8d337a2..db97213a0c468ae98b411ac54309ac9ee440f8c3 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -238,13 +238,14 @@ let match_power2_extraction = match_list_extraction match_power2
(* -------------------------------------------------------------------------- *)
(* rule A: to_a(to_b x) = to_b x when domain(b) is all included in domain(a) *)
-(* rule B: to_a(to_b x) = to_a x when size(b) is a multiple of size(a) *)
+(* rule B: to_a(to_b x) = to_a x when range(b) is a multiple of range(a)
+ AND a is not bool *)
-(* to_iota(e) where e = to_iota'(e') *)
-let simplify_f_to_conv f iota e conv e' =
+(* to_iota(e) where e = to_iota'(e'), only ranges for iota *)
+let simplify_range_comp f iota e conv e' =
let iota' = to_cint conv in
- let size' = Ctypes.i_bits iota' in
- let size = Ctypes.i_bits iota in
+ let size' = Ctypes.range iota' in
+ let size = Ctypes.range iota in
if size <= size'
then e_fun f [e']
(* rule B:
@@ -269,12 +270,12 @@ let simplify_f_to_bounds iota e =
let f_to_int = Ctypes.i_memo (fun iota -> make_fun_int "to" iota)
let configure_to_int iota =
- let f = f_to_int iota in
- let simplify e =
+
+ let simplify_range f iota e =
begin
try match F.repr e with
| Logic.Kint value ->
- let size = Integer.of_int (Ctypes.i_bits iota) in
+ let size = Integer.of_int (Ctypes.range iota) in
let signed = Ctypes.signed iota in
F.e_zint (Integer.cast ~size ~signed ~value)
| Logic.Fun( fland , es )
@@ -297,15 +298,22 @@ let configure_to_int iota =
| _ -> raise Not_found
end
| Logic.Fun( conv , [e'] ) -> (* unary op *)
- simplify_f_to_conv f iota e conv e'
+ simplify_range_comp f iota e conv e'
| _ -> raise Not_found
with Not_found ->
simplify_f_to_bounds iota e
end
in
- F.set_builtin_1 f simplify ;
-
- let simplify_leq x y =
+ let simplify_conv f iota e =
+ if iota = Ctypes.CBool then
+ match F.is_equal e F.e_zero with
+ | Yes -> F.e_zero
+ | No -> F.e_one
+ | Maybe -> raise Not_found
+ else
+ simplify_range f iota e
+ in
+ let simplify_leq f iota x y =
let lower,upper = Ctypes.bounds iota in
match F.repr y with
| Logic.Fun( conv , [_] )
@@ -324,7 +332,9 @@ let configure_to_int iota =
| _ -> raise Not_found
end
in
- F.set_builtin_leq f simplify_leq ;
+ let f = f_to_int iota in
+ F.set_builtin_1 f (simplify_conv f iota) ;
+ F.set_builtin_leq f (simplify_leq f iota) ;
to_cint_map := FunMap.add f iota !to_cint_map
@@ -485,14 +495,14 @@ let smp_bitk_positive = function
F.e_not (bitk_positive k a)
| Logic.Fun( conv , [a] ) (* when is_to_c_int conv *) ->
let iota = to_cint conv in
- let size = Ctypes.i_bits iota in
+ let range = Ctypes.range iota in
let signed = Ctypes.signed iota in
if signed then (* beware of sign-bit *)
- begin match is_leq k (e_int (size-2)) with
+ begin match is_leq k (e_int (range-2)) with
| Logic.Yes -> bitk_positive k a
| Logic.No | Logic.Maybe -> raise Not_found
end
- else begin match is_leq (e_int size) k with
+ else begin match is_leq (e_int range) k with
| Logic.Yes -> e_false
| Logic.No -> bitk_positive k a
| Logic.Maybe -> raise Not_found
diff --git a/src/plugins/wp/TacBitwised.ml b/src/plugins/wp/TacBitwised.ml
index bf9604878cc9858d958d7d8fde96ac300cfd9983..c49c61d292fe3732c9642389b32c1ce581cea0c6 100644
--- a/src/plugins/wp/TacBitwised.ml
+++ b/src/plugins/wp/TacBitwised.ml
@@ -108,7 +108,7 @@ let rec lookup push clause ~nbits ~priority p =
class autobitwise =
object(self)
- method private nbits = Ctypes.i_bits (Ctypes.c_ptr ())
+ method private nbits = Ctypes.range (Ctypes.c_ptr ())
method id = "wp:bitwised"
method title =
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index bde88014eff652f7934de930b483c41815ff837d..f26b90250538d28231b9fbbee1bd422d4f3fe95d 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -30,7 +30,7 @@ open Cil_datatype
module WpLog = Wp_parameters
type c_int =
- | Bool
+ | CBool
| UInt8
| SInt8
| UInt16
@@ -43,19 +43,19 @@ type c_int =
let compare_c_int : c_int -> c_int -> _ = Extlib.compare_basic
let signed = function
- | Bool -> false
+ | CBool -> false
| UInt8 | UInt16 | UInt32 | UInt64 -> false
| SInt8 | SInt16 | SInt32 | SInt64 -> true
-let i_bits = function
- | Bool -> 1
+let range = function
+ | CBool -> 1
| UInt8 | SInt8 -> 8
| UInt16 | SInt16 -> 16
| UInt32 | SInt32 -> 32
| UInt64 | SInt64 -> 64
-let i_bytes = function
- | Bool -> 1
+let sizeof_i = function
+ | CBool -> 1
| UInt8 | SInt8 -> 1
| UInt16 | SInt16 -> 2
| UInt32 | SInt32 -> 4
@@ -73,12 +73,12 @@ let is_char = function
| SInt8 -> not Cil.theMachine.Cil.theMachine.char_is_unsigned
| UInt16 | SInt16
| UInt32 | SInt32
- | UInt64 | SInt64 | Bool -> false
+ | UInt64 | SInt64 | CBool -> false
let c_int ikind =
let mach = Cil.theMachine.Cil.theMachine in
match ikind with
- | IBool -> if Wp_parameters.get_bool_range () then Bool else UInt8
+ | IBool -> CBool
| IChar -> if mach.char_is_unsigned then UInt8 else SInt8
| ISChar -> SInt8
| IUChar -> UInt8
@@ -97,8 +97,8 @@ let c_ptr () =
make_c_int false Cil.theMachine.Cil.theMachine.sizeof_ptr
let sub_c_int t1 t2 =
- if (signed t1 = signed t2) then i_bits t1 <= i_bits t2
- else (not(signed t1) && (i_bits t1 < i_bits t2))
+ if (signed t1 = signed t2) then range t1 <= range t2
+ else (not(signed t1) && (range t1 < range t2))
type c_float =
| Float32
@@ -106,7 +106,7 @@ type c_float =
let compare_c_float : c_float -> c_float -> _ = Extlib.compare_basic
-let f_bytes = function
+let sizeof_f = function
| Float32 -> 4
| Float64 -> 8
@@ -126,7 +126,7 @@ let c_float fkind =
| FDouble -> make_c_float mach.sizeof_double
| FLongDouble -> make_c_float mach.sizeof_longdouble
-let equal_float f1 f2 = f_bits f1 = f_bits f2
+let equal_float f1 f2 = (f1 = f2)
(* Array objects, with both the head view and the flatten view. *)
@@ -163,7 +163,7 @@ let idx = function
| SInt32 -> 5
| UInt64 -> 6
| SInt64 -> 7
- | Bool -> 8
+ | CBool -> 8
let i_memo f =
let m = Array.make 9 None in
@@ -186,7 +186,7 @@ let f_memo f =
| None -> let r = f z in m.(k) <- Some r ; r
let i_iter f =
- List.iter f [Bool;UInt8;SInt8;UInt16;SInt16;UInt32;SInt32;UInt64;SInt64]
+ List.iter f [CBool;UInt8;SInt8;UInt16;SInt16;UInt32;SInt32;UInt64;SInt64]
let f_iter f =
List.iter f [Float32;Float64]
@@ -195,23 +195,23 @@ let f_iter f =
(* --- Bounds --- *)
(* -------------------------------------------------------------------------- *)
-let i_bounds i =
- if signed i then
- let m = Integer.two_power_of_int (i_bits i - 1) in
- Integer.neg m , Integer.pred m
- else
- let m = Integer.two_power_of_int (i_bits i) in
- Integer.zero , Integer.pred m
-
-let bounds i = i_memo i_bounds i
+let bounds =
+ let i_bounds i =
+ if signed i then
+ let m = Integer.two_power_of_int (range i - 1) in
+ Integer.neg m , Integer.pred m
+ else
+ let m = Integer.two_power_of_int (range i) in
+ Integer.zero , Integer.pred m
+ in i_memo i_bounds
(* -------------------------------------------------------------------------- *)
(* --- Pretty Printers --- *)
(* -------------------------------------------------------------------------- *)
let pp_int fmt i =
- if i = Bool then Format.pp_print_string fmt "bool"
- else Format.fprintf fmt "%cint%d" (if signed i then 's' else 'u') (i_bits i)
+ if i = CBool then Format.pp_print_string fmt "bool"
+ else Format.fprintf fmt "%cint%d" (if signed i then 's' else 'u') (range i)
let pp_float fmt f = Format.fprintf fmt "float%d" (f_bits f)
@@ -445,9 +445,9 @@ let sizeof_defined = function
| _ -> true
let sizeof_object = function
- | C_int i -> i_bytes i
- | C_float f -> f_bytes f
- | C_pointer _ty -> i_bytes (c_ptr())
+ | C_int i -> sizeof_i i
+ | C_float f -> sizeof_f f
+ | C_pointer _ty -> sizeof_i (c_ptr())
| C_comp cinfo ->
let ctype = TComp(cinfo,Cil.empty_size_cache(),[]) in
(Cil.bitsSizeOf ctype / 8)
@@ -490,7 +490,7 @@ let field_offset fd =
(* with greater rank, whatever *)
(* their sign. *)
-let i_convert t1 t2 = if i_bits t1 < i_bits t2 then t2 else t1
+let i_convert t1 t2 = if range t1 < range t2 then t2 else t1
let f_convert t1 t2 = if f_bits t1 < f_bits t2 then t2 else t1
let promote a1 a2 =
diff --git a/src/plugins/wp/ctypes.mli b/src/plugins/wp/ctypes.mli
index 234bd3119eb79ed5bc5344a58d82893f6c5927a5..b09df11064c7352f237ebc29997f42b18528b8a3 100644
--- a/src/plugins/wp/ctypes.mli
+++ b/src/plugins/wp/ctypes.mli
@@ -28,7 +28,7 @@ open Cil_types
(** Runtime integers. *)
type c_int =
- | Bool
+ | CBool
| UInt8
| SInt8
| UInt16
@@ -97,9 +97,8 @@ val char : char -> int64
val constant : exp -> int64
val get_int : exp -> int64 option
-val i_bits : c_int -> int (** size in bits *)
-val i_bytes : c_int -> int (** size in bytes *)
val signed : c_int -> bool (** [true] if signed *)
+val range : c_int -> int (** range in 2^n *)
val bounds: c_int -> Integer.t * Integer.t (** domain, bounds included *)
(** All sizes are in bits *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle
index 789c01a6f59aa4dd26ca8c135f21bd2f89370f1b..70d1558a270afd984352f05fee911ed8f71bc1c3 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle
@@ -76,7 +76,7 @@ Prove: land(65535, a) != 21845.
Goal Post-condition for 'false' (file tests/wp_acsl/bitwise.i, line 91) in 'band_bool':
Assume {
- Type: is_uint8(a) /\ is_uint8(b).
+ Type: is_bool(a) /\ is_bool(b).
(* Pre-condition for 'false' *)
Have: (a != 1) \/ (b != 1).
}
@@ -142,7 +142,7 @@ Prove: true.
Goal Post-condition for 'false' (file tests/wp_acsl/bitwise.i, line 81) in 'bor_bool':
Assume {
- Type: is_uint8(a) /\ is_uint8(b).
+ Type: is_bool(a) /\ is_bool(b).
(* Pre-condition for 'false' *)
Have: (a != 1) /\ (b != 1).
}
@@ -155,7 +155,7 @@ Prove: (a = 0) /\ (b = 0).
Goal Post-condition for 'true' (file tests/wp_acsl/bitwise.i, line 78) in 'bor_bool':
Assume {
- Type: is_uint8(a) /\ is_uint8(b).
+ Type: is_bool(a) /\ is_bool(b).
(* Pre-condition for 'true' *)
Have: (a = 1) \/ (b = 1).
}
@@ -202,7 +202,7 @@ Prove: lnot(x) = b.
Goal Post-condition for 'false' (file tests/wp_acsl/bitwise.i, line 100) in 'bxor_bool':
Assume {
- Type: is_uint8(a) /\ is_uint8(b).
+ Type: is_bool(a) /\ is_bool(b).
(* Pre-condition for 'false' *)
Have: ((a != 0) \/ (b != 1)) /\ ((a != 1) \/ (b != 0)).
}
@@ -215,7 +215,7 @@ Prove: b = a.
Goal Post-condition for 'true' (file tests/wp_acsl/bitwise.i, line 97) in 'bxor_bool':
Assume {
- Type: is_uint8(a) /\ is_uint8(b).
+ Type: is_bool(a) /\ is_bool(b).
(* Pre-condition for 'true' *)
Have: ((a = 0) /\ (b = 1)) \/ ((a = 1) /\ (b = 0)).
}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle
index 8cc292011a2e990c06eb16a4358534a2838783b0..226cd7c529ab4ab1f5aabc3291e98501d6760e24 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle
@@ -12,7 +12,7 @@
[wp] [Qed] Goal typed_band_bit2_ensures_band4 : Valid
[wp] [Qed] Goal typed_band_bit3_ensures_band5 : Valid
[wp] [Qed] Goal typed_band_bit4_ensures_band6 : Valid
-[wp] [Alt-Ergo] Goal typed_band_bool_false_ensures : Unsuccess
+[wp] [Alt-Ergo] Goal typed_band_bool_false_ensures : Valid
[wp] [Qed] Goal typed_band_bool_true_ensures : Valid
[wp] [Qed] Goal typed_bnot_ensures : Valid
[wp] [Qed] Goal typed_bor_ensures : Valid
@@ -20,12 +20,12 @@
[wp] [Qed] Goal typed_bor_bit1_ensures_bor1 : Valid
[wp] [Qed] Goal typed_bor_bit2_ensures_bor2 : Valid
[wp] [Qed] Goal typed_bor_bit3_ensures_bor3 : Valid
-[wp] [Alt-Ergo] Goal typed_bor_bool_false_ensures : Unsuccess
+[wp] [Alt-Ergo] Goal typed_bor_bool_false_ensures : Valid
[wp] [Alt-Ergo] Goal typed_bor_bool_true_ensures : Valid
[wp] [Qed] Goal typed_bxor_ensures : Valid
[wp] [Qed] Goal typed_bxor_bit1_ensures : Valid
[wp] [Qed] Goal typed_bxor_bit2_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_bxor_bool_false_ensures : Unsuccess
+[wp] [Alt-Ergo] Goal typed_bxor_bool_false_ensures : Valid
[wp] [Qed] Goal typed_bxor_bool_true_ensures : Valid
[wp] [Qed] Goal typed_lshift_ensures : Valid
[wp] [Qed] Goal typed_lshift_shift1_ensures_lsl1 : Valid
@@ -33,9 +33,9 @@
[wp] [Qed] Goal typed_lshift_shift2_ensures_lsl3 : Valid
[wp] [Qed] Goal typed_rshift_ensures : Valid
[wp] [Qed] Goal typed_rshift_shift1_ensures_lsr1 : Valid
-[wp] Proved goals: 26 / 29
+[wp] Proved goals: 29 / 29
Qed: 25
- Alt-Ergo: 1 (unsuccess: 3)
+ Alt-Ergo: 4
[wp] Report in: 'tests/wp_acsl/oracle_qualif/bitwise.0.report.json'
[wp] Report out: 'tests/wp_acsl/result_qualif/bitwise.0.report.json'
-------------------------------------------------------------
@@ -46,7 +46,7 @@ bxor 3 - 3 100%
bnot 1 - 1 100%
lshift 4 - 4 100%
rshift 2 - 2 100%
-bor_bool - 1 (4..16) 2 50.0%
-band_bool 1 - 2 50.0%
-bxor_bool 1 - 2 50.0%
+bor_bool - 2 (8..20) 2 100%
+band_bool 1 1 (20..32) 2 100%
+bxor_bool 1 1 (8..20) 2 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/bool.i b/src/plugins/wp/tests/wp_plugin/bool.i
index 929c64489953a8bc22f2b39f9db7667cf080bda6..3c38f396a1cb35db75e4a0c97f7f623000297af9 100644
--- a/src/plugins/wp/tests/wp_plugin/bool.i
+++ b/src/plugins/wp/tests/wp_plugin/bool.i
@@ -1,11 +1,9 @@
/* run.config
- OPT: -wp-no-let -wp-no-bool-range
- OPT: -wp-no-let -wp-bool-range
+ OPT: -wp-no-let
*/
/* run.config_qualif
- OPT: -wp-no-let -wp-no-bool-range
- OPT: -wp-no-let -wp-bool-range
+ OPT: -wp-no-let
*/
@@ -15,7 +13,7 @@ int job(_Bool a, _Bool b) { return a+b; }
/*@ behavior true:
@ assumes a == 1 || b == 1;
@ ensures \result == 1;
- @ behavior false:
+ @ behavior false:
@ assumes !(a == 1 || b == 1);
@ ensures \result == 0;
*/
@@ -25,7 +23,7 @@ _Bool bor_bool(_Bool a, _Bool b) { return (_Bool)(((int)a | (int)b) != 0); }
/*@ behavior true:
@ assumes a == 1 && b == 1;
@ ensures \result == 1;
- @ behavior false:
+ @ behavior false:
@ assumes !(a == 1 && b == 1);
@ ensures \result == 0;
*/
@@ -34,7 +32,7 @@ _Bool band_bool(_Bool a, _Bool b) { return (_Bool)(((int)a & (int)b) != 0); }
/*@ behavior true:
@ assumes (a == 1 && b == 0) || (a == 0 && b == 1);
@ ensures \result == 1;
- @ behavior false:
+ @ behavior false:
@ assumes !((a == 1 && b == 0) || (a == 0 && b == 1)) ;
@ ensures \result == 0;
*/
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/bool.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/bool.0.res.oracle
deleted file mode 100644
index 68874ceaf821d834a858885852f28ca43f628961..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle/bool.0.res.oracle
+++ /dev/null
@@ -1,128 +0,0 @@
-# frama-c -wp -wp-no-let [...]
-[kernel] Parsing tests/wp_plugin/bool.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
-[wp] Warning: Missing RTE guards
-------------------------------------------------------------
- Function band_bool with behavior false
-------------------------------------------------------------
-
-Goal Post-condition for 'false' (file tests/wp_plugin/bool.i, line 30) in 'band_bool':
-Assume {
- Type: is_uint8(a) /\ is_uint8(a_1) /\ is_uint8(b) /\ is_uint8(b_1) /\
- is_uint8(band_bool_0) /\ is_uint8(retres_0).
- Have: (a_1 = a) /\ (b_1 = b).
- (* Pre-condition for 'false' *)
- Have: (a_1 != 1) \/ (b_1 != 1).
- Have: (if (land(a, b) = 0) then 0 else 1) = retres_0.
- (* Return *)
- Have: retres_0 = band_bool_0.
-}
-Prove: band_bool_0 = 0.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function band_bool with behavior true
-------------------------------------------------------------
-
-Goal Post-condition for 'true' (file tests/wp_plugin/bool.i, line 27) in 'band_bool':
-Assume {
- Type: is_uint8(a) /\ is_uint8(a_1) /\ is_uint8(b) /\ is_uint8(b_1) /\
- is_uint8(band_bool_0) /\ is_uint8(retres_0).
- Have: (a_1 = a) /\ (b_1 = b).
- (* Pre-condition for 'true' *)
- Have: (a_1 = 1) /\ (b_1 = 1).
- Have: (if (land(a, b) = 0) then 0 else 1) = retres_0.
- (* Return *)
- Have: retres_0 = band_bool_0.
-}
-Prove: band_bool_0 = 1.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function bor_bool with behavior false
-------------------------------------------------------------
-
-Goal Post-condition for 'false' (file tests/wp_plugin/bool.i, line 20) in 'bor_bool':
-Assume {
- Type: is_uint8(a) /\ is_uint8(a_1) /\ is_uint8(b) /\ is_uint8(b_1) /\
- is_uint8(bor_bool_0) /\ is_uint8(retres_0).
- Have: (a_1 = a) /\ (b_1 = b).
- (* Pre-condition for 'false' *)
- Have: (a_1 != 1) /\ (b_1 != 1).
- Have: (if ((a = 0) & (b = 0)) then 0 else 1) = retres_0.
- (* Return *)
- Have: retres_0 = bor_bool_0.
-}
-Prove: bor_bool_0 = 0.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function bor_bool with behavior true
-------------------------------------------------------------
-
-Goal Post-condition for 'true' (file tests/wp_plugin/bool.i, line 17) in 'bor_bool':
-Assume {
- Type: is_uint8(a) /\ is_uint8(a_1) /\ is_uint8(b) /\ is_uint8(b_1) /\
- is_uint8(bor_bool_0) /\ is_uint8(retres_0).
- Have: (a_1 = a) /\ (b_1 = b).
- (* Pre-condition for 'true' *)
- Have: (a_1 = 1) \/ (b_1 = 1).
- Have: (if ((a = 0) & (b = 0)) then 0 else 1) = retres_0.
- (* Return *)
- Have: retres_0 = bor_bool_0.
-}
-Prove: bor_bool_0 = 1.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function bxor_bool with behavior false
-------------------------------------------------------------
-
-Goal Post-condition for 'false' (file tests/wp_plugin/bool.i, line 39) in 'bxor_bool':
-Assume {
- Type: is_uint8(a) /\ is_uint8(a_1) /\ is_uint8(b) /\ is_uint8(b_1) /\
- is_uint8(bxor_bool_0) /\ is_uint8(retres_0).
- Have: (a_1 = a) /\ (b_1 = b).
- (* Pre-condition for 'false' *)
- Have: ((a_1 != 0) \/ (b_1 != 1)) /\ ((a_1 != 1) \/ (b_1 != 0)).
- Have: (if (b = a) then 0 else 1) = retres_0.
- (* Return *)
- Have: retres_0 = bxor_bool_0.
-}
-Prove: bxor_bool_0 = 0.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function bxor_bool with behavior true
-------------------------------------------------------------
-
-Goal Post-condition for 'true' (file tests/wp_plugin/bool.i, line 36) in 'bxor_bool':
-Assume {
- Type: is_uint8(a) /\ is_uint8(a_1) /\ is_uint8(b) /\ is_uint8(b_1) /\
- is_uint8(bxor_bool_0) /\ is_uint8(retres_0).
- Have: (a_1 = a) /\ (b_1 = b).
- (* Pre-condition for 'true' *)
- Have: ((a_1 = 0) /\ (b_1 = 1)) \/ ((a_1 = 1) /\ (b_1 = 0)).
- Have: (if (b = a) then 0 else 1) = retres_0.
- (* Return *)
- Have: retres_0 = bxor_bool_0.
-}
-Prove: bxor_bool_0 = 1.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function job
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_plugin/bool.i, line 12) in 'job':
-Assume {
- Type: is_uint8(a) /\ is_uint8(b) /\ is_sint32(job_0) /\
- is_sint32(retres_0).
- Have: (a + b) = retres_0.
- (* Return *)
- Have: retres_0 = job_0.
-}
-Prove: (0 <= job_0) /\ (job_0 <= 2).
-
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/bool.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/bool.res.oracle
similarity index 95%
rename from src/plugins/wp/tests/wp_plugin/oracle/bool.1.res.oracle
rename to src/plugins/wp/tests/wp_plugin/oracle/bool.res.oracle
index feb6965058e45327d31bd7bcea1975946210b74e..c80bbdfdc621cb262f494654e932dfd5f413cd53 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/bool.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/bool.res.oracle
@@ -7,7 +7,7 @@
Function band_bool with behavior false
------------------------------------------------------------
-Goal Post-condition for 'false' (file tests/wp_plugin/bool.i, line 30) in 'band_bool':
+Goal Post-condition for 'false' (file tests/wp_plugin/bool.i, line 28) in 'band_bool':
Assume {
Type: is_bool(a) /\ is_bool(a_1) /\ is_bool(b) /\ is_bool(b_1) /\
is_bool(band_bool_0) /\ is_bool(retres_0).
@@ -25,7 +25,7 @@ Prove: band_bool_0 = 0.
Function band_bool with behavior true
------------------------------------------------------------
-Goal Post-condition for 'true' (file tests/wp_plugin/bool.i, line 27) in 'band_bool':
+Goal Post-condition for 'true' (file tests/wp_plugin/bool.i, line 25) in 'band_bool':
Assume {
Type: is_bool(a) /\ is_bool(a_1) /\ is_bool(b) /\ is_bool(b_1) /\
is_bool(band_bool_0) /\ is_bool(retres_0).
@@ -43,7 +43,7 @@ Prove: band_bool_0 = 1.
Function bor_bool with behavior false
------------------------------------------------------------
-Goal Post-condition for 'false' (file tests/wp_plugin/bool.i, line 20) in 'bor_bool':
+Goal Post-condition for 'false' (file tests/wp_plugin/bool.i, line 18) in 'bor_bool':
Assume {
Type: is_bool(a) /\ is_bool(a_1) /\ is_bool(b) /\ is_bool(b_1) /\
is_bool(bor_bool_0) /\ is_bool(retres_0).
@@ -61,7 +61,7 @@ Prove: bor_bool_0 = 0.
Function bor_bool with behavior true
------------------------------------------------------------
-Goal Post-condition for 'true' (file tests/wp_plugin/bool.i, line 17) in 'bor_bool':
+Goal Post-condition for 'true' (file tests/wp_plugin/bool.i, line 15) in 'bor_bool':
Assume {
Type: is_bool(a) /\ is_bool(a_1) /\ is_bool(b) /\ is_bool(b_1) /\
is_bool(bor_bool_0) /\ is_bool(retres_0).
@@ -79,7 +79,7 @@ Prove: bor_bool_0 = 1.
Function bxor_bool with behavior false
------------------------------------------------------------
-Goal Post-condition for 'false' (file tests/wp_plugin/bool.i, line 39) in 'bxor_bool':
+Goal Post-condition for 'false' (file tests/wp_plugin/bool.i, line 37) in 'bxor_bool':
Assume {
Type: is_bool(a) /\ is_bool(a_1) /\ is_bool(b) /\ is_bool(b_1) /\
is_bool(bxor_bool_0) /\ is_bool(retres_0).
@@ -97,7 +97,7 @@ Prove: bxor_bool_0 = 0.
Function bxor_bool with behavior true
------------------------------------------------------------
-Goal Post-condition for 'true' (file tests/wp_plugin/bool.i, line 36) in 'bxor_bool':
+Goal Post-condition for 'true' (file tests/wp_plugin/bool.i, line 34) in 'bxor_bool':
Assume {
Type: is_bool(a) /\ is_bool(a_1) /\ is_bool(b) /\ is_bool(b_1) /\
is_bool(bxor_bool_0) /\ is_bool(retres_0).
@@ -115,7 +115,7 @@ Prove: bxor_bool_0 = 1.
Function job
------------------------------------------------------------
-Goal Post-condition (file tests/wp_plugin/bool.i, line 12) in 'job':
+Goal Post-condition (file tests/wp_plugin/bool.i, line 10) in 'job':
Assume {
Type: is_bool(a) /\ is_bool(b) /\ is_sint32(job_0) /\ is_sint32(retres_0).
Have: (a + b) = retres_0.
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/rte.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.0.res.oracle
index 00dfe9f2904865a995c497204fcbe1dee0d229d1..7eb7d1df64d15f0802d3c205dd74814362f05313 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/rte.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.0.res.oracle
@@ -5,6 +5,7 @@
[wp:rte] function job: generate rte for memory access
[wp:rte] function job: generate rte for division by zero
[wp:rte] function job: generate rte for signed overflow
+[wp] Warning: -wp-rte can annotate invalid bool value because -warn-invalid-bool is not set
[rte] annotating function job
[wp:rte] function job2: generate rte for memory access
[wp:rte] function job2: generate rte for division by zero
@@ -14,10 +15,7 @@
[wp:rte] function job3: generate rte for division by zero
[wp:rte] function job3: generate rte for signed overflow
[rte] annotating function job3
-[wp] tests/wp_plugin/rte.i:34: Warning:
- Option -wp-bool-range incompatiable with RTE (ignored)
-[wp] tests/wp_plugin/rte.i:34: Warning:
- Option -wp-bool-range incompatiable with RTE (ignored)
+[wp] Warning: Missing RTE guards
[wp] Goal typed_job_ensures : not tried
[wp] Goal typed_job_assert_rte_mem_access : not tried
[wp] Goal typed_job_assert_rte_mem_access_2 : not tried
@@ -26,7 +24,6 @@
[wp] Goal typed_job_assert_rte_mem_access_3 : not tried
[wp] Goal typed_job2_ensures : not tried
[wp] Goal typed_job3_ensures : not tried
-[wp] Goal typed_job3_assert_rte_bool_value : not tried
/* Generated by Frama-C */
/*@ axiomatic Obs {
predicate R(integer r) ;
@@ -60,7 +57,6 @@ _Bool X;
int job3(void)
{
int __retres;
- /*@ assert rte: bool_value: X == 0 || X == 1; */
__retres = (int)X;
return __retres;
}
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/rte.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.1.res.oracle
index 6468854c8f02b824a96b9c98a8e5475e265b11d2..3136da68bb235fb56970a9d05c9f02b05d682be7 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/rte.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.1.res.oracle
@@ -4,12 +4,15 @@
[wp] Loading driver 'share/wp.driver'
[wp:rte] function job: generate rte for memory access
[wp:rte] function job: generate rte for division by zero
+[wp:rte] function job: generate rte for invalid bool value
[rte] annotating function job
[wp:rte] function job2: generate rte for memory access
[wp:rte] function job2: generate rte for division by zero
+[wp:rte] function job2: generate rte for invalid bool value
[rte] annotating function job2
[wp:rte] function job3: generate rte for memory access
[wp:rte] function job3: generate rte for division by zero
+[wp:rte] function job3: generate rte for invalid bool value
[rte] annotating function job3
[wp] Goal typed_job_ensures : not tried
[wp] Goal typed_job_assert_rte_mem_access : not tried
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/rte.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.2.res.oracle
index 435bd15de2dd4548bf68167a5c121096acbf0443..ec0f537db15872e38aaeca0f1dee10c1a13c2932 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/rte.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.2.res.oracle
@@ -6,16 +6,19 @@
[wp:rte] function job: generate rte for division by zero
[wp:rte] function job: generate rte for signed overflow
[wp:rte] function job: generate rte for unsigned overflow
+[wp:rte] function job: generate rte for invalid bool value
[rte] annotating function job
[wp:rte] function job2: generate rte for memory access
[wp:rte] function job2: generate rte for division by zero
[wp:rte] function job2: generate rte for signed overflow
[wp:rte] function job2: generate rte for unsigned overflow
+[wp:rte] function job2: generate rte for invalid bool value
[rte] annotating function job2
[wp:rte] function job3: generate rte for memory access
[wp:rte] function job3: generate rte for division by zero
[wp:rte] function job3: generate rte for signed overflow
[wp:rte] function job3: generate rte for unsigned overflow
+[wp:rte] function job3: generate rte for invalid bool value
[rte] annotating function job3
[wp] Goal typed_job_ensures : not tried
[wp] Goal typed_job_assert_rte_mem_access : not tried
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/rte.3.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.3.res.oracle
index 0f7bf5b438530ec71343d9ad13f7699f140ff179..d5189e5215a283b655aa75b3a1ae42fa67f16bcb 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/rte.3.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.3.res.oracle
@@ -8,14 +8,17 @@
[wp] Warning: -wp-rte and model nat require kernel to warn against unsigned overflow
[wp] Warning: -wp-rte and model nat require kernel to warn against signed downcast
[wp] Warning: -wp-rte and model nat require kernel to warn against unsigned downcast
+[wp:rte] function job: generate rte for invalid bool value
[rte] annotating function job
[wp:rte] function job2: generate rte for memory access
[wp:rte] function job2: generate rte for division by zero
[wp:rte] function job2: generate rte for signed overflow
+[wp:rte] function job2: generate rte for invalid bool value
[rte] annotating function job2
[wp:rte] function job3: generate rte for memory access
[wp:rte] function job3: generate rte for division by zero
[wp:rte] function job3: generate rte for signed overflow
+[wp:rte] function job3: generate rte for invalid bool value
[rte] annotating function job3
[wp] Goal typed_nat_job_ensures : not tried
[wp] Goal typed_nat_job_assert_rte_mem_access : not tried
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/rte.4.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.4.res.oracle
index f2b78e1cab7eadf8dd166e940fe39f17721e4a3c..7a1f8d5436279e560433b649dcea25b9b81b151c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/rte.4.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.4.res.oracle
@@ -8,16 +8,19 @@
[wp:rte] function job: generate rte for unsigned overflow
[wp] Warning: -wp-rte and model nat require kernel to warn against signed downcast
[wp] Warning: -wp-rte and model nat require kernel to warn against unsigned downcast
+[wp:rte] function job: generate rte for invalid bool value
[rte] annotating function job
[wp:rte] function job2: generate rte for memory access
[wp:rte] function job2: generate rte for division by zero
[wp:rte] function job2: generate rte for signed overflow
[wp:rte] function job2: generate rte for unsigned overflow
+[wp:rte] function job2: generate rte for invalid bool value
[rte] annotating function job2
[wp:rte] function job3: generate rte for memory access
[wp:rte] function job3: generate rte for division by zero
[wp:rte] function job3: generate rte for signed overflow
[wp:rte] function job3: generate rte for unsigned overflow
+[wp:rte] function job3: generate rte for invalid bool value
[rte] annotating function job3
[wp] Goal typed_nat_job_ensures : not tried
[wp] Goal typed_nat_job_assert_rte_mem_access : not tried
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/rte.5.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.5.res.oracle
index f171879c60095d87502ac5e2b4cfaf1d27783e91..b8d50097f75d58ded23f025ff8962702cc2147a4 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/rte.5.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.5.res.oracle
@@ -5,13 +5,16 @@
[wp:rte] function job: missing rte for memory access
[wp:rte] function job: missing rte for division by zero
[wp:rte] function job: missing rte for signed overflow
+[wp:rte] function job: missing rte for invalid bool value
[wp] Warning: Missing RTE guards
[wp:rte] function job2: missing rte for memory access
[wp:rte] function job2: missing rte for division by zero
[wp:rte] function job2: missing rte for signed overflow
+[wp:rte] function job2: missing rte for invalid bool value
[wp:rte] function job3: missing rte for memory access
[wp:rte] function job3: missing rte for division by zero
[wp:rte] function job3: missing rte for signed overflow
+[wp:rte] function job3: missing rte for invalid bool value
[wp] Goal typed_nat_job_ensures : not tried
[wp] Goal typed_nat_job2_ensures : not tried
[wp] Goal typed_nat_job3_ensures : not tried
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/rte.6.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.6.res.oracle
index 892f3d6443df55894205cbbb0aefde7cd301ec57..b4f10b265197441ab9ed7eba8f949324d76cf0a5 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/rte.6.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.6.res.oracle
@@ -8,12 +8,15 @@
[wp] Warning: -wp-rte and model nat require kernel to warn against unsigned overflow
[wp] Warning: -wp-rte and model nat require kernel to warn against signed downcast
[wp] Warning: -wp-rte and model nat require kernel to warn against unsigned downcast
+[wp:rte] function job: generate rte for invalid bool value
[rte] annotating function job
[wp:rte] function job2: generate rte for division by zero
[wp:rte] function job2: generate rte for signed overflow
+[wp:rte] function job2: generate rte for invalid bool value
[rte] annotating function job2
[wp:rte] function job3: generate rte for division by zero
[wp:rte] function job3: generate rte for signed overflow
+[wp:rte] function job3: generate rte for invalid bool value
[rte] annotating function job3
[wp] Warning: Missing RTE guards
[wp] Goal typed_nat_job_ensures : not tried
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.0.res.oracle
deleted file mode 100644
index 8361dfbe06c2a3ca456908944745b3358bc40fa3..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.0.res.oracle
+++ /dev/null
@@ -1,25 +0,0 @@
-# frama-c -wp -wp-no-let -wp-timeout 90 -wp-steps 1500 [...]
-[kernel] Parsing tests/wp_plugin/bool.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
-[wp] Warning: Missing RTE guards
-[wp] 7 goals scheduled
-[wp] [Alt-Ergo] Goal typed_band_bool_false_ensures : Unsuccess
-[wp] [Qed] Goal typed_band_bool_true_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_bor_bool_false_ensures : Unsuccess
-[wp] [Alt-Ergo] Goal typed_bor_bool_true_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_bxor_bool_false_ensures : Unsuccess
-[wp] [Qed] Goal typed_bxor_bool_true_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_job_ensures : Unsuccess
-[wp] Proved goals: 3 / 7
- Qed: 2
- Alt-Ergo: 1 (unsuccess: 4)
-[wp] Report in: 'tests/wp_plugin/oracle_qualif/bool.0.report.json'
-[wp] Report out: 'tests/wp_plugin/result_qualif/bool.0.report.json'
--------------------------------------------------------------
-Functions WP Alt-Ergo Total Success
-job - - 1 0.0%
-bor_bool - 1 (4..16) 2 50.0%
-band_bool 1 - 2 50.0%
-bxor_bool 1 - 2 50.0%
--------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.res.oracle
similarity index 89%
rename from src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.1.res.oracle
rename to src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.res.oracle
index 04c1d1900f3eafd5005f09ee9ac19469ce4c9b02..81ddac40fbc8520741dd7ce823a79583b97c9964 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.res.oracle
@@ -14,8 +14,8 @@
[wp] Proved goals: 7 / 7
Qed: 2
Alt-Ergo: 5
-[wp] Report in: 'tests/wp_plugin/oracle_qualif/bool.1.report.json'
-[wp] Report out: 'tests/wp_plugin/result_qualif/bool.1.report.json'
+[wp] Report in: 'tests/wp_plugin/oracle_qualif/bool.0.report.json'
+[wp] Report out: 'tests/wp_plugin/result_qualif/bool.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
job - 1 (12..24) 1 100%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
index c1ef69535aed91d4f33ce7fbba751711bdbe85f1..397e221edae9e7c97ae3a4dec110fa7e54d22b5d 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
@@ -12,11 +12,11 @@
__retres ∈ [-2147483647..2147483647]
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_main_assert_Eva_signed_overflow : Unsuccess
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (unsuccess: 1)
[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
[wp] 0 goal scheduled
[wp] Proved goals: 0 / 0
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle
index 5bc109acf7a85a1b6883a74fd34729ddba7df872..2404c6c172d972e02516806b7836b8ed8d36fa25 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle
@@ -5,24 +5,20 @@
[rte] annotating function job
[rte] annotating function job2
[rte] annotating function job3
-[wp] tests/wp_plugin/rte.i:34: Warning:
- Option -wp-bool-range incompatiable with RTE (ignored)
-[wp] tests/wp_plugin/rte.i:34: Warning:
- Option -wp-bool-range incompatiable with RTE (ignored)
[wp] 6 goals scheduled
[wp] [Alt-Ergo] Goal typed_job_assert_rte_mem_access : Unsuccess
[wp] [Alt-Ergo] Goal typed_job_assert_rte_mem_access_2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_job_assert_rte_signed_overflow : Unsuccess
[wp] [Alt-Ergo] Goal typed_job_assert_rte_signed_overflow_2 : Unsuccess
[wp] [Qed] Goal typed_job_assert_rte_mem_access_3 : Valid
-[wp] [Alt-Ergo] Goal typed_job3_assert_rte_bool_value : Unsuccess
-[wp] Proved goals: 1 / 6
+[wp] [Alt-Ergo] Goal typed_job3_assert_rte_bool_value : Valid
+[wp] Proved goals: 2 / 6
Qed: 1
- Alt-Ergo: 0 (unsuccess: 5)
+ Alt-Ergo: 1 (unsuccess: 4)
[wp] Report in: 'tests/wp_plugin/oracle_qualif/rte.0.report.json'
[wp] Report out: 'tests/wp_plugin/result_qualif/rte.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
job 1 - 5 20.0%
-job3 - - 1 0.0%
+job3 - 1 (4..16) 1 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/rte.i b/src/plugins/wp/tests/wp_plugin/rte.i
index f20717efcbadf7f1ea1be762af3fb9e605b0e142..1b63b3768c83f5e7f9f053f2bf203a2a879e0851 100644
--- a/src/plugins/wp/tests/wp_plugin/rte.i
+++ b/src/plugins/wp/tests/wp_plugin/rte.i
@@ -1,6 +1,6 @@
/* run.config
CMD: @frama-c@ -wp -wp-prover none -wp-check -wp-share ./share -wp-msg-key shell -wp-msg-key rte
- OPT: -wp-rte -warn-invalid-bool -wp-bool-range -then -print -no-unicode
+ OPT: -wp-rte -no-warn-invalid-bool -then -print -no-unicode
OPT: -wp-rte -no-warn-signed-overflow -then -print -no-unicode
OPT: -wp-rte -warn-unsigned-overflow -then -print -no-unicode
OPT: -wp-rte -wp-model +nat -then -print -no-unicode
@@ -9,7 +9,7 @@
OPT: -wp-rte -rte-no-mem -wp-model +nat
*/
/* run.config_qualif
- OPT: -wp-rte -warn-invalid-bool -wp-bool-range -wp-prop=rte
+ OPT: -wp-rte -warn-invalid-bool -wp-prop=rte
*/
diff --git a/src/plugins/wp/wpRTE.ml b/src/plugins/wp/wpRTE.ml
index 30974a1edba460c7bed8feb8f91a76105ffb5afc..e3e8d851d6212aec2d862333b4f8b9009a76a768 100644
--- a/src/plugins/wp/wpRTE.ml
+++ b/src/plugins/wp/wpRTE.ml
@@ -24,9 +24,9 @@ let dkey = Wp_parameters.register_category "rte"
type t = {
name : string ;
- kernel : (unit -> bool) ;
- rtegen : string ;
cint : bool ;
+ kernel : (unit -> bool) ;
+ option : string ;
status : (unit -> Db.RteGen.status_accessor) ref ;
}
@@ -52,14 +52,14 @@ let configure ~update ~generate kf cint rte =
(* need RTE guard, but kernel option is set *)
if not (status rte.status kf) then
begin
- if option rte.rtegen then
+ if option rte.option then
let msg = if generate then "generate" else "missing" in
Wp_parameters.debug ~dkey "function %a: %s rte for %s"
Kernel_function.pretty kf msg rte.name ;
else
Wp_parameters.warning ~once:true ~current:false
"-wp-rte can annotate %s because %s is not set"
- rte.name rte.rtegen ;
+ rte.name rte.option ;
update := true ;
end
end
@@ -73,23 +73,27 @@ let configure ~update ~generate kf cint rte =
let generator =
[
{ name = "memory access" ;
- kernel = always ; rtegen = "-rte-mem" ; cint = false ;
+ kernel = always ; option = "-rte-mem" ; cint = false ;
status = Db.RteGen.get_memAccess_status } ;
{ name = "division by zero" ;
- kernel = always ; rtegen = "-rte-div" ; cint = false ;
+ kernel = always ; option = "-rte-div" ; cint = false ;
status = Db.RteGen.get_divMod_status } ;
{ name = "signed overflow" ; cint = true ;
- kernel = Kernel.SignedOverflow.get ; rtegen = "" ;
+ kernel = Kernel.SignedOverflow.get ; option = "" ;
status = Db.RteGen.get_signedOv_status } ;
{ name = "unsigned overflow" ; cint = true ;
- kernel = Kernel.UnsignedOverflow.get ; rtegen = "" ;
+ kernel = Kernel.UnsignedOverflow.get ; option = "" ;
status = Db.RteGen.get_unsignedOv_status } ;
- { name = "signed downcast" ; cint = true ; rtegen = "" ;
+ { name = "signed downcast" ; cint = true ; option = "" ;
kernel = Kernel.SignedDowncast.get ;
status = Db.RteGen.get_signed_downCast_status } ;
- { name = "unsigned downcast" ; cint = true ; rtegen = "" ;
+ { name = "unsigned downcast" ; cint = true ; option = "" ;
kernel = Kernel.UnsignedDowncast.get ;
status = Db.RteGen.get_unsignedDownCast_status } ;
+ { name = "invalid bool value" ; cint = false ;
+ option = "-warn-invalid-bool" ;
+ kernel = Kernel.InvalidBool.get ;
+ status = Db.RteGen.get_bool_value_status } ;
]
let generate kf model =
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 3ea59dcff6c5d945d25a6a9f9ab253da7373cd73..6e8fc4bb53dbaee7e025a402786555b89db78604 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -223,14 +223,6 @@ module ExtEqual =
let help = "Use extensional equality on compounds (hypotheses only)."
end)
-let () = Parameter_customize.set_group wp_model
-let () = Parameter_customize.is_invisible () (* experimental option *)
-module BoolRange =
- False(struct
- let option_name = "-wp-bool-range"
- let help = "Assumes _Bool values have no trap representations."
- end)
-
let () = Parameter_customize.set_group wp_model
module Overflows =
False(struct
@@ -909,7 +901,6 @@ let active_unless_rte option =
else true
let get_overflows () = Overflows.get () && active_unless_rte "-wp-overflows"
-let get_bool_range () = BoolRange.get () && active_unless_rte "-wp-bool-range"
let dkey = register_category "env"
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 88dfd0553b3f8aea5e6db86da44a6c4a8de29157..d9fd672e9b5225aaed8973ac6ec9678175ded356 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -146,7 +146,6 @@ val get_output : unit -> string
val get_output_dir : string -> string
val get_includes : unit -> string list
val make_output_dir : string -> unit
-val get_bool_range : unit -> bool
val get_overflows : unit -> bool
(** {2 Debugging Categories} *)
diff --git a/tests/rte/oracle/twofunc.res.oracle b/tests/rte/oracle/twofunc.res.oracle
index 982ec3917fd96c7489d38111850b074cdbf48fc5..58f6280ce2a0652e9d51261289831067a286bf40 100644
--- a/tests/rte/oracle/twofunc.res.oracle
+++ b/tests/rte/oracle/twofunc.res.oracle
@@ -130,7 +130,7 @@ int main(void)
[kernel] ================================
[kernel] printing status
[kernel] kf = f
-[kernel] - bool_value = false
+[kernel] - bool_value = true
[kernel] - finite_float = true
[kernel] - float_to_int = true
[kernel] - unsigned_downcast = false
@@ -145,7 +145,7 @@ int main(void)
[kernel] - mem_access = true
[kernel] - initialized = false
[kernel] kf = main
-[kernel] - bool_value = false
+[kernel] - bool_value = true
[kernel] - finite_float = true
[kernel] - float_to_int = true
[kernel] - unsigned_downcast = false
@@ -222,7 +222,7 @@ int main(void)
[kernel] ================================
[kernel] printing status
[kernel] kf = f
-[kernel] - bool_value = false
+[kernel] - bool_value = true
[kernel] - finite_float = true
[kernel] - float_to_int = true
[kernel] - unsigned_downcast = false
@@ -237,7 +237,7 @@ int main(void)
[kernel] - mem_access = true
[kernel] - initialized = false
[kernel] kf = main
-[kernel] - bool_value = false
+[kernel] - bool_value = true
[kernel] - finite_float = true
[kernel] - float_to_int = true
[kernel] - unsigned_downcast = false