diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index c84b8efd2ccee6c157b8b327204f22ef6292294d..453741922dd8961a25955f802c7126330a47101c 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -381,6 +381,16 @@ let is_same_direction_binop dir op =
let is_same_direction_rel dir op =
update_direction_rel dir op <> Nothing
+let remove_no_op_coerce t =
+ match t.term_node with
+ | TLogic_coerce (ty,t) when Cil.no_op_coerce ty t -> t
+ | _ -> t
+
+let rec is_singleton t =
+ match t.term_node with
+ | TLogic_coerce(Ltype ({ lt_name = "set"},_), t') -> is_singleton t'
+ | _ -> not (Logic_const.is_set_type t.term_type)
+
(* when pretty-printing relation chains, a < b && b' < c, it can happen that
b has a coercion and b' hasn't or vice-versa (bc c is an integer and a and
b are ints for instance). We nevertheless want to
@@ -388,13 +398,7 @@ let is_same_direction_rel dir op =
removed any existing head coercion.
*)
let equal_mod_coercion t1 t2 =
- let t1 =
- match t1.term_node with TLogic_coerce(_,t1) -> t1 | _ -> t1
- in
- let t2 =
- match t2.term_node with TLogic_coerce(_,t2) -> t2 | _ -> t2
- in
- Cil_datatype.Term.equal t1 t2
+ Cil_datatype.Term.equal (remove_no_op_coerce t1) (remove_no_op_coerce t2)
(* Grab one of the labels of a statement *)
let rec pickLabel = function
@@ -2341,8 +2345,7 @@ class cil_printer () = object (self)
| Ttype ty ->
fprintf fmt "%a(%a)" self#pp_acsl_keyword "\\type" (self#typ None) ty
| Tunion l
- when ((List.for_all (fun t -> not(Logic_const.is_set_type t.term_type)) l)
- && (not state.print_cil_as_is)) ->
+ when (List.for_all is_singleton l) && (not state.print_cil_as_is) ->
fprintf fmt "{%a}" (Pretty_utils.pp_list ~sep:",@ " self#term) l
| Tunion locs ->
fprintf fmt "@[<hov 2>%a(@,%a)@]"
@@ -2392,13 +2395,11 @@ class cil_printer () = object (self)
pp_defn
(self#term_prec current_level) body
| TLogic_coerce(ty,t) ->
- let debug =
- Kernel.is_debug_key_enabled Kernel.dkey_print_logic_coercions
- in
- if debug then
- fprintf fmt "/* (coercion to:%a */" (self#logic_type None) ty;
+ if (not (Cil.no_op_coerce ty t)) ||
+ Kernel.is_debug_key_enabled Kernel.dkey_print_logic_coercions
+ then
+ fprintf fmt "(%a)" (self#logic_type None) ty;
self#term_prec current_level fmt t;
- if debug then fprintf fmt "/* ) */"
method private term_lval_prec contextprec fmt lv =
if Precedence.getParenthLevelLogic (TLval lv) > contextprec then
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index af7f23d2146b33e67ad6e3e195aa3a239a55d795..c088eed195f8144256271503379efb0343b517fd 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -4495,11 +4495,22 @@ let isCharConstPtrType t =
match t with
| Ctype ty -> isIntegralType ty
| Linteger -> true
- | Ltype ({lt_name = name},[]) ->
- name = Utf8_logic.boolean
- | Ltype (tdef,_) as ty when is_unrollable_ltdef tdef ->
- isLogicBooleanType (unroll_ltdef ty)
- | Lreal | Ltype _ | Lvar _ | Larrow _ -> false
+ | Ltype ({lt_name = name} as tdef,_) ->
+ name = Utf8_logic.boolean ||
+ ( is_unrollable_ltdef tdef && isLogicBooleanType (unroll_ltdef t))
+ | Lreal | Lvar _ | Larrow _ -> false
+
+let isBoolType typ = match unrollType typ with
+ | TInt (IBool, _) -> true
+ | _ -> false
+
+let rec isLogicPureBooleanType t =
+ match t with
+ | Ctype t -> isBoolType t
+ | Ltype ({lt_name = name} as def,_) ->
+ name = Utf8_logic.boolean ||
+ (is_unrollable_ltdef def && isLogicPureBooleanType (unroll_ltdef t))
+ | _ -> false
let rec isLogicIntegralType t =
match t with
@@ -4622,6 +4633,14 @@ let isCharConstPtrType t =
let () =
registerAttribute (Extlib.strip_underscore frama_c_init_obj) (AttrName false)
+ let no_op_coerce typ t =
+ match typ with
+ | Lreal -> true
+ | Linteger -> isLogicIntegralType t.term_type
+ | Ltype _ when Logic_const.is_boolean_type typ ->
+ isLogicPureBooleanType t.term_type
+ | Ltype ({lt_name="set"},_) -> true
+ | _ -> false
(**** Compute the type of an expression ****)
let rec typeOf (e: exp) : typ =
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 80d30d5792ce80a8e7b75929732394cd995b0d4e..bcb8991186ad056f30b552187d9ab42c0e35fec8 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -537,6 +537,16 @@ val isCharArrayType: typ -> bool
(** True if the argument is an integral type (i.e. integer or enum) *)
val isIntegralType: typ -> bool
+(** True if the argument is [_Bool]
+ @since Frama-C+dev
+*)
+val isBoolType: typ -> bool
+
+(** True if the argument is [_Bool] or [boolean].
+ @since Frama-C+dev
+ *)
+val isLogicPureBooleanType: logic_type -> bool
+
(** True if the argument is an integral or pointer type. *)
val isIntegralOrPointerType: typ -> bool
@@ -842,6 +852,13 @@ val isLogicZero: term -> bool
(** True if the given term is [\null] or a constant null pointer*)
val isLogicNull: term -> bool
+(** [no_op_coerce typ term] is [true] iff converting [term] to [typ] does
+ not modify its value.
+
+ @since Frama-C+dev
+*)
+val no_op_coerce: logic_type -> term -> bool
+
(** gives the value of a wide char literal. *)
val reduce_multichar: Cil_types.typ -> int64 list -> int64
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 49ffb79f66f68216a4917a8bae7187ca1341984e..727d6639ffd39c87b79ad04acfda62f86d667a62 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -1071,16 +1071,20 @@ struct
Cil_datatype.Logic_type.equal (Ctype ctyp1) (Ctype ctyp2)
let rec c_mk_cast ?(force=false) e oldt newt =
+ let loc = e.term_loc in
if is_same_c_type oldt newt then begin
- if force then
- Logic_utils.mk_cast ~loc:e.term_loc ~force newt e
- else e
+ if force then Logic_utils.mk_cast ~loc ~force newt e else e
end else begin
(* Watch out for constants *)
if isPointerType newt && isLogicNull e && not (isLogicZero e) then
(* \null can have any pointer type, see ACSL manual. *)
- { e with term_type = Ctype newt }
- else if isPointerType newt && isArrayType oldt && is_C_array e then begin
+ (if force then
+ Logic_const.term ~loc (TCastE (newt, e)) (Ctype newt)
+ else
+ { e with term_type = Ctype newt })
+ else if isPointerType newt && isArrayType oldt then begin
+ if not (is_C_array e) then
+ C.error loc "cannot cast logic array to pointer type";
let e = mk_logic_StartOf e in
let oldt = Logic_utils.logicCType e.term_type in
(* we have converted from array to ptr, but the pointed type might
@@ -1089,7 +1093,7 @@ struct
end else begin
match Cil.unrollType newt, e.term_node with
| TEnum (ei,[]), TConst (LEnum { eihost = ei'})
- when ei.ename = ei'.ename -> e
+ when ei.ename = ei'.ename && not force -> e
| _ ->
{ e with term_node =
(Logic_utils.mk_cast ~force newt e).term_node;
@@ -1161,20 +1165,24 @@ struct
| _ -> false
let logic_coerce t e =
- let set = make_set_type t in
+ let real_type = set_conversion t e.term_type in
let rec aux e =
match e.term_node with
| Tcomprehension(e,q,p) ->
- { e with term_type = set; term_node = Tcomprehension (aux e,q,p) }
+ { e with term_type = real_type;
+ term_node = Tcomprehension (aux e,q,p) }
| Tunion l ->
- { e with term_type = set; term_node = Tunion (List.map aux l) }
+ { e with term_type = real_type; term_node = Tunion (List.map aux l) }
| Tinter l ->
- { e with term_type = set; term_node = Tinter (List.map aux l) }
- | Tempty_set -> { e with term_type = set }
- | TLogic_coerce(_,e) ->
- { e with term_type = t; term_node = TLogic_coerce(t,e) }
- | _ when Cil.isLogicArithmeticType t -> Logic_utils.numeric_coerce t e
- | _ -> { e with term_type = t; term_node = TLogic_coerce(t,e) }
+ { e with term_type = real_type; term_node = Tinter (List.map aux l) }
+ | Tempty_set -> { e with term_type = real_type }
+ | TLogic_coerce(t2,e) when Cil.no_op_coerce t2 e ->
+ let e = aux e in
+ { e with term_type = real_type; term_node = TLogic_coerce(real_type,e) }
+ | _ when Cil.isLogicArithmeticType real_type ->
+ Logic_utils.numeric_coerce real_type e
+ | _ ->
+ { e with term_type = real_type; term_node = TLogic_coerce(real_type,e) }
in
if is_same_type e.term_type t then e else aux e
@@ -1196,10 +1204,20 @@ struct
in
lift_set convert_one_location t
- let rec mk_cast e newt =
+ let rec mk_cast ?(explicit=false) e newt =
+ let force = explicit in
let loc = e.term_loc in
- if is_same_type e.term_type newt then e
- else if is_enum_cst e newt then e
+ let truncate_info =
+ List.hd @@ Logic_env.find_all_logic_functions "\\truncate"
+ in
+ if is_same_type e.term_type newt then begin
+ if explicit then begin
+ match Logic_const.unroll_ltdef newt with
+ | Ctype cnewt ->
+ { e with term_node = TCastE(cnewt,e); term_type = newt }
+ | _ -> e
+ end else e
+ end else if is_enum_cst e newt then { e with term_type = newt }
else begin
match
(unroll_type e.term_type),
@@ -1207,15 +1225,17 @@ struct
(Logic_const.unroll_ltdef newt)
with
| Ctype oldt, Ctype newt ->
- c_mk_cast e oldt newt
+ c_mk_cast ~force e oldt newt
| t1, Ltype ({lt_name = name},[])
when name = Utf8_logic.boolean && is_integral_type t1 ->
- { e with
- term_node =
- TBinOp(Cil_types.Ne,
- mk_cast e Linteger,
- lzero ~loc ());
- term_type = Ltype(C.find_logic_type Utf8_logic.boolean,[]) }
+ let t2 = Ltype (C.find_logic_type Utf8_logic.boolean,[]) in
+ let e = mk_cast e Linteger in
+ Logic_const.term ~loc (TBinOp(Ne,e,lzero ~loc())) t2
+ | t1, Linteger when Logic_const.is_boolean_type t1 && explicit ->
+ logic_coerce Linteger e
+ | t1, Ctype t2 when Logic_const.is_boolean_type t1
+ && is_integral_type newt && explicit ->
+ Logic_const.term ~loc (TCastE (t2,e)) newt
| ty1, Ltype({lt_name="set"},[ty2])
when is_pointer_type ty1 &&
is_plain_pointer_type ty2 &&
@@ -1224,27 +1244,37 @@ struct
| Ltype({lt_name = "set"},[_]), Ltype({lt_name="set"},[ty2]) ->
let e = lift_set (fun e -> mk_cast e ty2) e in
{ e with term_type = make_set_type e.term_type}
+ (* extremely dirty cast to allow Eva to understand some libc
+ specifications *)
+ | Ltype({lt_name = "set"},[_]), Ctype ty2 when explicit ->
+ Logic_utils.mk_cast ~loc ty2 e
| _ , Ltype({lt_name = "set"},[ ty2 ]) ->
let e = mk_cast e ty2 in
logic_coerce (make_set_type e.term_type) e
| Linteger, Linteger | Lreal, Lreal -> e
| Linteger, Ctype t when isLogicPointerType newt && isLogicNull e ->
- c_mk_cast e intType t
+ c_mk_cast ~force e intType t
+ | Linteger, (Ctype newt) | Lreal, (Ctype newt) when explicit ->
+ Logic_utils.mk_cast ~loc newt e
| Linteger, Ctype t when isIntegralType t ->
- (try
- C.integral_cast t e
- with Failure s -> C.error loc "%s" s)
+ (try C.integral_cast t e with Failure s -> C.error loc "%s" s)
| Linteger, Ctype _ | Lreal, Ctype _ ->
C.error loc "invalid implicit cast from %a to C type %a"
Cil_printer.pp_logic_type e.term_type
Cil_printer.pp_logic_type newt
| Ctype t, Linteger when Cil.isIntegralType t -> logic_coerce Linteger e
+ | Ctype t, Linteger when Cil.isArithmeticType t && explicit ->
+ Logic_const.term
+ ~loc (Tapp(truncate_info,[], [logic_coerce Lreal e])) Linteger
| Ctype t, Lreal when isArithmeticType t -> logic_coerce Lreal e
| Ctype _, (Lreal | Linteger) ->
C.error loc "invalid implicit cast from %a to logic type %a"
Cil_printer.pp_logic_type e.term_type
Cil_printer.pp_logic_type newt
| Linteger, Lreal -> logic_coerce Lreal e
+ | Lreal, Linteger when explicit ->
+ let term_node = Tapp(truncate_info,[],[e]) in
+ Logic_const.term ~loc term_node Linteger
| Lreal, Linteger ->
C.error loc
"invalid cast from real to integer. \
@@ -1778,6 +1808,8 @@ struct
when Cil.isIntegralType t -> Linteger
| (Linteger, Ctype t | Ctype t, Linteger)
when Cil.isArithmeticType t -> Lreal
+ (* In ACSL, you can convert implicitely from integral to boolean =>
+ prefer boolean as common type when doing comparison. *)
| Ltype({lt_name = name},[]), t
when is_integral_type t && name = Utf8_logic.boolean ->
Ltype(C.find_logic_type Utf8_logic.boolean,[])
@@ -2395,7 +2427,6 @@ struct
in
normalize_updated_offset_term idx_typing env loc t normalizing_cont toff
and locations_set ctxt ~lift_set env loc l init_type =
- let module C = struct end in
let convert_ptr, locs, typ =
List.fold_left
(fun (convert_ptr,locs,typ) t ->
@@ -2415,7 +2446,6 @@ struct
let locs = List.rev_map (make_set_conversion convert_ptr) locs in
locs,typ
and lfun_app ctxt env loc f labels ttl =
- let module C = struct end in
try
let info = ctxt.find_logic_ctor f in
if labels <> [] then begin
@@ -2444,7 +2474,6 @@ struct
ctxt.error loc "symbol %s is a predicate, not a function" f
| Some t -> Tapp(info, label_assoc, tl), t
and term_node ctxt env loc pl =
- let module C = struct end in
let term = ctxt.type_term ctxt in
let term_ptr pl =
let t = term env pl in
@@ -2838,49 +2867,9 @@ struct
| PLcast (ty, t) ->
let t = term env t in
(* no casts of tsets in grammar *)
- let ct =
- Logic_const.unroll_ltdef (logic_type ctxt loc env ty)
- in
- (match ct with
- | (Ctype tnew) ->
- (match t.term_type with
- | Ctype told ->
- if isPointerType tnew && isArrayType told
- && not (is_C_array t) then
- ctxt.error loc "cannot cast logic array to pointer type";
- if Cil.isVoidPtrType told then
- (Logic_utils.mk_cast tnew t).term_node, ct
- else
- (c_mk_cast ~force:true t told tnew).term_node , ct
- | _ -> (Logic_utils.mk_cast tnew t).term_node, ct)
- | Linteger when is_arithmetic_type t.term_type ->
- let truncate_info =
- List.hd @@ Logic_env.find_all_logic_functions "\\truncate"
- in
- let term_node =
- match unroll_type t.term_type with
- | Lreal -> Tapp (truncate_info, [], [t])
- | Ctype ty when not (Cil.isIntegralType ty) ->
- (* arithmetic but not integral type: floating point.
- Coerce to real before applying truncate. *)
- Tapp (
- truncate_info, [],
- [ Logic_const.term ~loc:t.term_loc
- (TLogic_coerce(Lreal,t)) Lreal ])
- | Ctype _ ->
- (* an integral type by construction *)
- TLogic_coerce(Linteger, t)
- | Linteger -> (* coercion is a no-op. *) t.term_node
- | Ltype _ | Lvar _ | Larrow _ as ty ->
- Kernel.fatal
- "%a should not be considered an arithmetic type"
- Cil_printer.pp_logic_type ty
- in
- term_node, Linteger
- | Linteger | Lreal | Ltype _ | Lvar _ | Larrow _ ->
- ctxt.error loc "cannot cast from %a to %a"
- Cil_printer.pp_logic_type t.term_type
- Cil_printer.pp_logic_type ct)
+ let ct = Logic_const.unroll_ltdef (logic_type ctxt loc env ty) in
+ let { term_node; term_type } = mk_cast ~explicit:true t ct in
+ (term_node, term_type)
| PLcoercion (t,ty) ->
let t = term env t in
(match Logic_const.unroll_ltdef (logic_type ctxt loc env ty) with
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index 59d1fc9037353595777fb5883510555e39d98678..f30df04280448362252376dfc6aa835029466b64 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -291,8 +291,14 @@ sig
val type_of_field:
location -> string -> logic_type -> (term_offset * logic_type)
- (** @since Nitrogen-20111001 *)
- val mk_cast: Cil_types.term -> Cil_types.logic_type -> Cil_types.term
+ (**
+ @param explicit true if the cast is present in original source.
+ defaults to false
+ @since Nitrogen-20111001
+ @modify Frama-C+dev introduces explicit param
+ *)
+ val mk_cast:
+ ?explicit:bool -> Cil_types.term -> Cil_types.logic_type -> Cil_types.term
(** type-checks a term. *)
val term : Lenv.t -> Logic_ptree.lexpr -> term
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index c99bcaee9a110f7dfb6d1c89390e686da30bebca..25249cfdd3623fbd5c3e56d65731048d23e58691 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -304,7 +304,7 @@ let numeric_coerce ltyp t =
let oldt = unroll_type t.term_type in
if Cil_datatype.Logic_type.equal oldt ltyp then t
else match t.term_node with
- | TLogic_coerce(_,e) -> coerce e
+ | TLogic_coerce(t,e) when Cil.no_op_coerce t e -> coerce e
| TConst(Integer(i,_)) ->
(match oldt, ltyp with
| Ctype (TInt(ikind,_)), Linteger when Cil.fitsInInt ikind i ->
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 72aaae64939db4a472ba53182119724d895b22c0..e77caab5c5cef1c8d13189efc6d896b5aa67be47 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -604,6 +604,15 @@ let cast ~src_typ ~dst_typ v =
| TSFloat fkind, TSFloat _ ->
Cvalue.V.cast_float_to_float (Fval.kind fkind) v
+(* V.cast_int_to_int is unsound when the destination type is _Bool.
+ Use this function instead. *)
+let cast_to_bool r =
+ let contains_zero = V.contains_zero r.eover
+ and contains_non_zero = V.contains_non_zero r.eover in
+ let eover = V.interp_boolean ~contains_zero ~contains_non_zero in
+ { eover; eunder = under_from_over eover;
+ ldeps = r.ldeps; etype = TInt (IBool, []) }
+
(* -------------------------------------------------------------------------- *)
(* --- Inlining of defined logic functions and predicates --- *)
(* -------------------------------------------------------------------------- *)
@@ -835,15 +844,14 @@ let rec eval_term ~alarm_mode env t =
| TCastE (typ, t) ->
let r = eval_term ~alarm_mode env t in
- let eover, eunder =
- (* See if the cast does something. If not, we can keep eunder as is.*)
- if is_noop_cast ~src_typ:t.term_type ~dst_typ:typ
- then r.eover, r.eunder
- else
- let eover = cast ~src_typ:r.etype ~dst_typ:typ r.eover in
- eover, under_from_over eover
- in
- { etype = typ; ldeps = r.ldeps; eunder; eover }
+ (* See if the cast does something. If not, we can keep eunder as is.*)
+ if is_noop_cast ~src_typ:t.term_type ~dst_typ:typ
+ then { r with etype = typ }
+ else if Cil.isBoolType typ
+ then cast_to_bool r
+ else
+ let eover = cast ~src_typ:r.etype ~dst_typ:typ r.eover in
+ { etype = typ; ldeps = r.ldeps; eunder = under_from_over eover; eover }
| Tif (tcond, ttrue, tfalse) ->
eval_tif eval_term Cvalue.V.join Cvalue.V.meet ~alarm_mode env
@@ -887,9 +895,8 @@ let rec eval_term ~alarm_mode env t =
nothing to do, AND coercion from an integer type to a floating-point
type, that require a conversion. *)
(match Logic_const.plain_or_set Extlib.id ltyp with
- | Linteger ->
- assert (Logic_typing.is_integral_type t.term_type);
- r
+ | Linteger when Logic_typing.is_integral_type t.term_type
+ || Logic_const.is_boolean_type t.term_type -> r
| Ctype typ when Cil.isIntegralOrPointerType typ -> r
| Lreal ->
if Logic_typing.is_integral_type t.term_type
@@ -905,9 +912,14 @@ let rec eval_term ~alarm_mode env t =
ldeps = r.ldeps;
eunder = under_from_over eover;
eover; }
- | _ -> unsupported
- (Format.asprintf "logic coercion %a -> %a@."
- Printer.pp_logic_type t.term_type Printer.pp_logic_type ltyp)
+ | _ ->
+ if Logic_const.is_boolean_type ltyp
+ && Logic_typing.is_integral_type t.term_type
+ then cast_to_bool r
+ else
+ unsupported
+ (Format.asprintf "logic coercion %a -> %a@."
+ Printer.pp_logic_type t.term_type Printer.pp_logic_type ltyp)
)
(* TODO: the meaning of the label in \offset and \base_addr is not obvious
diff --git a/src/plugins/wp/Cmath.ml b/src/plugins/wp/Cmath.ml
index 73f81d6118262bce0d8ca3dd8dc02befcbab9597..e168c743a9bb81fa2ee5ed23cfc826440d9a8f6b 100644
--- a/src/plugins/wp/Cmath.ml
+++ b/src/plugins/wp/Cmath.ml
@@ -90,6 +90,9 @@ let builtin_truncate f e =
let int_of_real x = e_fun f_truncate [x]
let real_of_int x = e_fun f_real_of_int [x]
+let int_of_bool a = e_neq a F.e_zero (* if a != 0 then true else false *)
+let bool_of_int a = e_if a F.e_one F.e_zero (* if a then 1 else 0 *)
+
(* -------------------------------------------------------------------------- *)
(* --- Sign --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Cmath.mli b/src/plugins/wp/Cmath.mli
index 7c1510ffdc31ba5d0463ffb389a324544528f07e..c7ba3bd52e4ca8c4dc428a3f319503783e3562c9 100644
--- a/src/plugins/wp/Cmath.mli
+++ b/src/plugins/wp/Cmath.mli
@@ -27,6 +27,9 @@
open Lang
open Lang.F
+val int_of_bool : unop
+val bool_of_int : unop
+
val int_of_real : term -> term
val real_of_int : term -> term
diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index 9deb0c43059410fdd55a579123a83e1c2a05be6a..2c8f9c8028b3f78ca70d4d6b57f46f9b2641ea2f 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -587,7 +587,9 @@ struct
L.map
(fun x -> Cmath.int_of_real (Cfloat.real_of_float f x))
(C.logic env t)
- | L_bool|L_pointer _|L_array _ ->
+ | L_bool ->
+ L.map Cmath.bool_of_int (C.logic env t)
+ | L_pointer _|L_array _ ->
Warning.error "@[Logic cast from (%a) to (%a) not implemented yet@]"
Printer.pp_logic_type src_ltype Printer.pp_logic_type Linteger
@@ -595,7 +597,9 @@ struct
let src_ltype = Logic_utils.unroll_type ~unroll_typedef:false t.term_type in
match cvsort_of_ltype src_ltype with
| L_bool -> C.logic env t
- | L_integer | L_cint _ | L_real | L_cfloat _ | L_pointer _ | L_array _ ->
+ | L_integer | L_cint _ ->
+ L.map Cmath.int_of_bool (C.logic env t)
+ | L_real | L_cfloat _ | L_pointer _ | L_array _ ->
Warning.error "@[Logic cast from (%a) to (%a) not implemented yet@]"
Printer.pp_logic_type src_ltype Printer.pp_logic_type Logic_const.boolean_type
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.1.res.oracle
index eed072a4459086c18dbdce7451614a67e8aa2fe8..08da43a458417fc280047339c94f6cf5092d16b2 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/funvar_inv.1.res.oracle
@@ -17,10 +17,10 @@ Assume {
(* Heap *)
Have: linked(Malloc_0).
(* Initializer *)
- Init: Mint_0[global(L_i_23)] = 0.
+ Init: Mint_0[global(L_i_25)] = 0.
If v <= 3
Then { (* Else *) Have: Mint_0[f] = 0. Have: shift_sint32(a, v) = f. }
- Else { Have: global(L_i_23) = f. }
+ Else { Have: global(L_i_25) = f. }
}
Prove: a_1 = f.
@@ -37,10 +37,10 @@ Assume {
(* Heap *)
Have: linked(Malloc_0).
(* Initializer *)
- Init: Mint_0[global(L_i_23)] = 0.
+ Init: Mint_0[global(L_i_25)] = 0.
If v <= 3
Then { (* Else *) Have: Mint_0[f] = 0. Have: shift_sint32(a, v) = f. }
- Else { Have: global(L_i_23) = f. }
+ Else { Have: global(L_i_25) = f. }
}
Prove: a_1 = f.
@@ -64,11 +64,11 @@ Assume {
(* Heap *)
Have: linked(Malloc_0).
(* Initializer *)
- Init: Mint_0[global(L_i_28)] = 0.
+ Init: Mint_0[global(L_i_30)] = 0.
If v <= 3
Then { (* Else *) Have: Mint_0[f2_0] = 0. Have: shift_sint32(a, v) = f2_0.
}
- Else { Have: global(L_i_28) = f2_0. }
+ Else { Have: global(L_i_30) = f2_0. }
}
Prove: a_1 = f2_0.
@@ -85,11 +85,11 @@ Assume {
(* Heap *)
Have: linked(Malloc_0).
(* Initializer *)
- Init: Mint_0[global(L_i_28)] = 0.
+ Init: Mint_0[global(L_i_30)] = 0.
If v <= 3
Then { (* Else *) Have: Mint_0[f2_0] = 0. Have: shift_sint32(a, v) = f2_0.
}
- Else { Have: global(L_i_28) = f2_0. }
+ Else { Have: global(L_i_30) = f2_0. }
}
Prove: a_1 = f2_0.
@@ -113,10 +113,10 @@ Assume {
(* Heap *)
Have: linked(Malloc_0).
(* Initializer *)
- Init: Mint_0[global(L_i_33)] = 0.
+ Init: Mint_0[global(L_i_35)] = 0.
If v <= 3
Then { (* Else *) Have: Mint_0[g] = 0. Have: shift_sint32(a, v) = g. }
- Else { Have: global(L_i_33) = g. }
+ Else { Have: global(L_i_35) = g. }
}
Prove: a_1 = g.
@@ -133,10 +133,10 @@ Assume {
(* Heap *)
Have: linked(Malloc_0).
(* Initializer *)
- Init: Mint_0[global(L_i_33)] = 0.
+ Init: Mint_0[global(L_i_35)] = 0.
If v <= 3
Then { (* Else *) Have: Mint_0[g] = 0. Have: shift_sint32(a, v) = g. }
- Else { Have: global(L_i_33) = g. }
+ Else { Have: global(L_i_35) = g. }
}
Prove: a_1 = g.
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
index a3547cdccf7acb41cb77c368f97cbefbca8ec98c..a3cea5bd6984268aed68ac102feb1159c7e9c6d3 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
@@ -62,11 +62,11 @@ Prove: true.
------------------------------------------------------------
Goal Pre-condition 'qed_ok' in 'main':
-Let a = global(G_tr_31).
+Let a = global(G_tr_33).
Let a_1 = shift___anonstruct_Point_1(a, 2).
Let a_2 = shift___anonstruct_Point_1(a, 1).
Let a_3 = shift___anonstruct_Point_1(a, 0).
-Let a_4 = shiftfield_F4_bytes(global(G_buint_37)).
+Let a_4 = shiftfield_F4_bytes(global(G_buint_39)).
Let m = Array1_S1(a_3, 3, Mint_0).
Assume {
Type: IsArray1S1(m).
@@ -91,18 +91,18 @@ Assume {
(* Initializer *)
Init: Mint_0[shiftfield_F1_y(a_1)] = 31.
(* Heap *)
- Have: region(G_tr_31) <= 0.
+ Have: region(G_tr_33) <= 0.
}
Prove: P_P(m).
------------------------------------------------------------
Goal Pre-condition 'qed_ok' in 'main':
-Let a = global(G_tr_31).
+Let a = global(G_tr_33).
Let a_1 = shift___anonstruct_Point_1(a, 2).
Let a_2 = shift___anonstruct_Point_1(a, 1).
Let a_3 = shift___anonstruct_Point_1(a, 0).
-Let a_4 = shiftfield_F4_bytes(global(G_buint_37)).
+Let a_4 = shiftfield_F4_bytes(global(G_buint_39)).
Let m = Array1_S1(a_3, 3, Mint_0).
Assume {
Type: IsArray1S1(m).
@@ -127,18 +127,18 @@ Assume {
(* Initializer *)
Init: Mint_0[shiftfield_F1_y(a_1)] = 31.
(* Heap *)
- Have: region(G_tr_31) <= 0.
+ Have: region(G_tr_33) <= 0.
}
Prove: P_P(m).
------------------------------------------------------------
Goal Pre-condition 'qed_ok' in 'main':
-Let a = global(G_tr_31).
+Let a = global(G_tr_33).
Let a_1 = shift___anonstruct_Point_1(a, 2).
Let a_2 = shift___anonstruct_Point_1(a, 1).
Let a_3 = shift___anonstruct_Point_1(a, 0).
-Let a_4 = shiftfield_F4_bytes(global(G_buint_37)).
+Let a_4 = shiftfield_F4_bytes(global(G_buint_39)).
Let m = Array1_S1(a_3, 3, Mint_0).
Assume {
Type: IsArray1S1(m).
@@ -163,7 +163,7 @@ Assume {
(* Initializer *)
Init: Mint_0[shiftfield_F1_y(a_1)] = 31.
(* Heap *)
- Have: region(G_tr_31) <= 0.
+ Have: region(G_tr_33) <= 0.
}
Prove: P_P(m).
@@ -173,7 +173,7 @@ Goal Pre-condition 'qed_ok' in 'main':
tests/wp_acsl/logic.i:49: warning from wp:
- Warning: Hide sub-term definition
Reason: Logic cast from struct (Tint2) not implemented yet
-Assume { (* Heap *) Have: region(G_tr_31) <= 0. }
+Assume { (* Heap *) Have: region(G_tr_33) <= 0. }
Prove: (w.F1_y) = 11.
------------------------------------------------------------
@@ -182,7 +182,7 @@ Goal Pre-condition 'qed_ok' in 'main':
tests/wp_acsl/logic.i:50: warning from wp:
- Warning: Hide sub-term definition
Reason: Logic cast from struct (Point) not implemented yet
-Assume { (* Heap *) Have: region(G_tr_31) <= 0. }
+Assume { (* Heap *) Have: region(G_tr_33) <= 0. }
Prove: (w.F3_tab)[1] = 11.
------------------------------------------------------------
@@ -191,7 +191,7 @@ Goal Pre-condition 'qed_ok' in 'main':
tests/wp_acsl/logic.i:51: warning from wp:
- Warning: Hide sub-term definition
Reason: Logic cast to struct (Point) from (int [2]) not implemented yet
-Assume { (* Heap *) Have: region(G_tr_31) <= 0. }
+Assume { (* Heap *) Have: region(G_tr_33) <= 0. }
Prove: (w.F1_y) = 11.
------------------------------------------------------------
@@ -200,7 +200,7 @@ Goal Pre-condition 'qed_ok' in 'main':
tests/wp_acsl/logic.i:52: warning from wp:
- Warning: Hide sub-term definition
Reason: Logic cast from struct (Point) not implemented yet
-Assume { (* Heap *) Have: region(G_tr_31) <= 0. }
+Assume { (* Heap *) Have: region(G_tr_33) <= 0. }
Prove: w[1] = 11.
------------------------------------------------------------
@@ -209,7 +209,7 @@ Goal Pre-condition 'qed_ok' in 'main':
tests/wp_acsl/logic.i:53: warning from wp:
- Warning: Hide sub-term definition
Reason: Logic cast from struct (Tint2) not implemented yet
-Assume { (* Heap *) Have: region(G_tr_31) <= 0. }
+Assume { (* Heap *) Have: region(G_tr_33) <= 0. }
Prove: w[1] = 11.
------------------------------------------------------------
@@ -218,7 +218,7 @@ Goal Pre-condition 'qed_ok' in 'main':
tests/wp_acsl/logic.i:54: warning from wp:
- Warning: Hide sub-term definition
Reason: Logic cast from struct (Buint) not implemented yet
-Assume { (* Heap *) Have: region(G_tr_31) <= 0. }
+Assume { (* Heap *) Have: region(G_tr_33) <= 0. }
Prove: w = 134480385.
------------------------------------------------------------
@@ -227,11 +227,11 @@ Goal Pre-condition 'qed_ok' in 'main':
tests/wp_acsl/logic.i:55: warning from wp:
- Warning: Hide sub-term definition
Reason: Logic cast to struct (Buint) from (unsigned int) not implemented yet
-Let a = global(G_tr_31).
+Let a = global(G_tr_33).
Let a_1 = shift___anonstruct_Point_1(a, 2).
Let a_2 = shift___anonstruct_Point_1(a, 1).
Let a_3 = shift___anonstruct_Point_1(a, 0).
-Let a_4 = global(G_buint_37).
+Let a_4 = global(G_buint_39).
Let a_5 = shiftfield_F4_bytes(a_4).
Let a_6 = Load_S4(a_4, Mint_0).
Assume {
@@ -257,7 +257,7 @@ Assume {
(* Initializer *)
Init: Mint_0[shiftfield_F1_y(a_1)] = 31.
(* Heap *)
- Have: region(G_tr_31) <= 0.
+ Have: region(G_tr_33) <= 0.
}
Prove: EqS4(a_6, w).
@@ -267,7 +267,7 @@ Goal Pre-condition 'qed_ok' in 'main':
tests/wp_acsl/logic.i:56: warning from wp:
- Warning: Hide sub-term definition
Reason: Logic cast from struct (Tint6) not implemented yet
-Assume { (* Heap *) Have: region(G_tr_31) <= 0. }
+Assume { (* Heap *) Have: region(G_tr_33) <= 0. }
Prove: (w[1].F1_y) = 21.
------------------------------------------------------------
@@ -276,7 +276,7 @@ Goal Pre-condition 'qed_ok' in 'main':
tests/wp_acsl/logic.i:57: warning from wp:
- Warning: Hide sub-term definition
Reason: Logic cast to sized array (Triangle) from (int [6]) not implemented yet
-Assume { (* Heap *) Have: region(G_tr_31) <= 0. }
+Assume { (* Heap *) Have: region(G_tr_33) <= 0. }
Prove: (w[1].F1_y) = 21.
------------------------------------------------------------
@@ -285,7 +285,7 @@ Goal Pre-condition 'qed_ok' in 'main':
tests/wp_acsl/logic.i:58: warning from wp:
- Warning: Hide sub-term definition
Reason: Logic cast from struct (Tint6) not implemented yet
-Assume { (* Heap *) Have: region(G_tr_31) <= 0. }
+Assume { (* Heap *) Have: region(G_tr_33) <= 0. }
Prove: w[4] = 30.
------------------------------------------------------------
@@ -294,7 +294,7 @@ Goal Pre-condition 'qed_ok' in 'main':
tests/wp_acsl/logic.i:59: warning from wp:
- Warning: Hide sub-term definition
Reason: Logic cast from struct (Tint6) not implemented yet
-Assume { (* Heap *) Have: region(G_tr_31) <= 0. }
+Assume { (* Heap *) Have: region(G_tr_33) <= 0. }
Prove: w[1] = 11.
------------------------------------------------------------
@@ -303,7 +303,7 @@ Goal Pre-condition 'qed_ok' in 'main':
tests/wp_acsl/logic.i:60: warning from wp:
- Warning: Hide sub-term definition
Reason: Logic cast to sized array (int [2]) from (int [6]) not implemented yet
-Assume { (* Heap *) Have: region(G_tr_31) <= 0. }
+Assume { (* Heap *) Have: region(G_tr_33) <= 0. }
Prove: w[1] = 11.
------------------------------------------------------------
@@ -312,7 +312,7 @@ Goal Pre-condition 'qed_ok' in 'main':
tests/wp_acsl/logic.i:61: warning from wp:
- Warning: Hide sub-term definition
Reason: Logic cast from struct (Tint6) not implemented yet
-Assume { (* Heap *) Have: region(G_tr_31) <= 0. }
+Assume { (* Heap *) Have: region(G_tr_33) <= 0. }
Prove: (w.F3_tab)[1] = 11.
------------------------------------------------------------
@@ -321,7 +321,7 @@ Goal Pre-condition 'qed_ok' in 'main':
tests/wp_acsl/logic.i:62: warning from wp:
- Warning: Hide sub-term definition
Reason: Logic cast to struct (Tint2) from (int [6]) not implemented yet
-Assume { (* Heap *) Have: region(G_tr_31) <= 0. }
+Assume { (* Heap *) Have: region(G_tr_33) <= 0. }
Prove: (w.F3_tab)[1] = 11.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/unit_bool.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/unit_bool.res.oracle
index 1cb5211807364ba0a1e40558630a6e0ede78bbd2..d4de7cfa3f0f970563a557098110b87b7e45f8d3 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/unit_bool.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/unit_bool.res.oracle
@@ -2,6 +2,7 @@
[kernel] Parsing tests/wp_acsl/unit_bool.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
------------------------------------------------------------
Axiomatic 'Foo'
------------------------------------------------------------
@@ -11,3 +12,76 @@ Assume: 'f_def'
Prove: (L_f 1)
------------------------------------------------------------
+------------------------------------------------------------
+ Function boolean_casts
+------------------------------------------------------------
+
+Goal Check 'C0' (file tests/wp_acsl/unit_bool.i, line 12):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'C1' (file tests/wp_acsl/unit_bool.i, line 13):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'c0' (file tests/wp_acsl/unit_bool.i, line 14):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'c1' (file tests/wp_acsl/unit_bool.i, line 15):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'c2' (file tests/wp_acsl/unit_bool.i, line 16):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'X0' (file tests/wp_acsl/unit_bool.i, line 18):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'X1' (file tests/wp_acsl/unit_bool.i, line 19):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'x0' (file tests/wp_acsl/unit_bool.i, line 20):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'x1' (file tests/wp_acsl/unit_bool.i, line 21):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'x2' (file tests/wp_acsl/unit_bool.i, line 22):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'B0' (file tests/wp_acsl/unit_bool.i, line 24):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'B1' (file tests/wp_acsl/unit_bool.i, line 25):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'b0' (file tests/wp_acsl/unit_bool.i, line 26):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'b1' (file tests/wp_acsl/unit_bool.i, line 27):
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.0.report.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.0.report.json
index cce14a76fc5d3c4f15f0d5cc158f65973abdc826..7ca95e7dd10415727a170f4f6aba1b2ca49acf7e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.0.report.json
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.0.report.json
@@ -1,5 +1,6 @@
{ "wp:global": { "alt-ergo": { "total": 1, "valid": 1, "rank": 1 },
- "wp:main": { "total": 1, "valid": 1, "rank": 1 } },
+ "qed": { "total": 14, "valid": 14 },
+ "wp:main": { "total": 15, "valid": 15, "rank": 1 } },
"wp:axiomatics": { "Foo": { "lemma_f_1": { "alt-ergo": { "total": 1,
"valid": 1,
"rank": 1 },
@@ -11,4 +12,92 @@
"rank": 1 },
"wp:main": { "total": 1,
"valid": 1,
- "rank": 1 } } } } }
+ "rank": 1 } } } },
+ "wp:functions": { "boolean_casts": { "boolean_casts_check_b1": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "boolean_casts_check_b0": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "boolean_casts_check_B1": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "boolean_casts_check_B0": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "boolean_casts_check_x2": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "boolean_casts_check_x1": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "boolean_casts_check_x0": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "boolean_casts_check_X1": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "boolean_casts_check_X0": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "boolean_casts_check_c2": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "boolean_casts_check_c1": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "boolean_casts_check_c0": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "boolean_casts_check_C1": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "boolean_casts_check_C0": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 14,
+ "valid": 14 },
+ "wp:main": { "total": 14,
+ "valid": 14 } } } } }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle
index 6822d60dd5bcd79a8825366fa1c45c8f3e84b68b..9e87f031a9e560e54f18727f4b97a157236afc1e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle
@@ -2,10 +2,25 @@
[kernel] Parsing tests/wp_acsl/unit_bool.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
-[wp] 1 goal scheduled
+[wp] Warning: Missing RTE guards
+[wp] 15 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_f_1 : Valid
-[wp] Proved goals: 1 / 1
- Qed: 0
+[wp] [Qed] Goal typed_boolean_casts_check_C0 : Valid
+[wp] [Qed] Goal typed_boolean_casts_check_C1 : Valid
+[wp] [Qed] Goal typed_boolean_casts_check_c0 : Valid
+[wp] [Qed] Goal typed_boolean_casts_check_c1 : Valid
+[wp] [Qed] Goal typed_boolean_casts_check_c2 : Valid
+[wp] [Qed] Goal typed_boolean_casts_check_X0 : Valid
+[wp] [Qed] Goal typed_boolean_casts_check_X1 : Valid
+[wp] [Qed] Goal typed_boolean_casts_check_x0 : Valid
+[wp] [Qed] Goal typed_boolean_casts_check_x1 : Valid
+[wp] [Qed] Goal typed_boolean_casts_check_x2 : Valid
+[wp] [Qed] Goal typed_boolean_casts_check_B0 : Valid
+[wp] [Qed] Goal typed_boolean_casts_check_B1 : Valid
+[wp] [Qed] Goal typed_boolean_casts_check_b0 : Valid
+[wp] [Qed] Goal typed_boolean_casts_check_b1 : Valid
+[wp] Proved goals: 15 / 15
+ Qed: 14
Alt-Ergo: 1
[wp] Report in: 'tests/wp_acsl/oracle_qualif/unit_bool.0.report.json'
[wp] Report out: 'tests/wp_acsl/result_qualif/unit_bool.0.report.json'
@@ -13,3 +28,6 @@
Axiomatics WP Alt-Ergo Total Success
Axiomatic Foo - 1 (1..12) 1 100%
-------------------------------------------------------------
+Functions WP Alt-Ergo Total Success
+boolean_casts 14 - 14 100%
+-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/unit_bool.i b/src/plugins/wp/tests/wp_acsl/unit_bool.i
index 2892c9f8273a0d161d6b61fbcf01b8cb284efbb8..dd18aa4f3e0e4ff3ef1336c01f8d9db4b79efc7b 100644
--- a/src/plugins/wp/tests/wp_acsl/unit_bool.i
+++ b/src/plugins/wp/tests/wp_acsl/unit_bool.i
@@ -6,3 +6,24 @@
lemma f_1: f(1);
}*/
+
+
+_Bool boolean_casts(int x, _Bool y) {
+ //@ check C0: 0 == (integer) \false;
+ //@ check C1: 1 == (integer) \true ;
+ //@ check c0: \false == (boolean) 0;
+ //@ check c1: \true == (boolean) 1;
+ //@ check c2: \true == (boolean) 2;
+ int x0 = 0, x1=1, x2=2;
+ //@ check X0: x0 == (int) \false;
+ //@ check X1: x1 == (int) \true ;
+ //@ check x0: \false == (boolean) x0;
+ //@ check x1: \true == (boolean) x1;
+ //@ check x2: \true == (boolean) x2;
+ _Bool b0=0, b1=1;
+ //@ check B0: b0 == (_Bool) \false;
+ //@ check B1: b1 == (_Bool) \true ;
+ //@ check b0: \false == (boolean) b0;
+ //@ check b1: \true == (boolean) b1;
+ return 0;
+}
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1382.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1382.res.oracle
index c879e33dc86d5cf1f08b5f3112ca731ff604261f..fda8518f28c08a99a5d6e26f5a08d0087ab0fc40 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_1382.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1382.res.oracle
@@ -41,7 +41,7 @@ Assume {
(* Then *)
Have: i <= 99.
}
-Prove: global(G_dest_41) = w.
+Prove: global(G_dest_43) = w.
------------------------------------------------------------
@@ -66,6 +66,6 @@ Assume {
(* Then *)
Have: i <= 99.
}
-Prove: included(a, 4, global(G_dest_41), 1).
+Prove: included(a, 4, global(G_dest_43), 1).
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/logicarr.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/logicarr.res.oracle
index dc2bde48d0b1118904149a967f4acd118cf04921..1c6d6b15d610bef874863628f574230db7f93207 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/logicarr.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/logicarr.res.oracle
@@ -8,7 +8,7 @@
------------------------------------------------------------
Goal Post-condition 'PTR' in 'job':
-Let a = global(G_arr_31).
+Let a = global(G_arr_33).
Let a_1 = shift_sint32(a, i).
Let x = Mint_0[a_1].
Let a_2 = shift_sint32(a, 0).
@@ -26,7 +26,7 @@ Prove: P_p_pointer(m, Mint_0, a_2, i, j).
------------------------------------------------------------
Goal Post-condition 'ARR' in 'job':
-Let a = global(G_arr_31).
+Let a = global(G_arr_33).
Let a_1 = shift_sint32(a, i).
Let x = Mint_0[a_1].
Let a_2 = shift_sint32(a, 0).
@@ -45,7 +45,7 @@ Prove: P_p_arrays(m, i, m_1, j).
------------------------------------------------------------
Goal Post-condition 'DUM' in 'job':
-Let a = global(G_arr_31).
+Let a = global(G_arr_33).
Let a_1 = shift_sint32(a, i).
Let x = Mint_0[a_1].
Let a_2 = shift_sint32(a, 0).
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/logicref_simple.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/logicref_simple.res.oracle
index 95a881fa681b043535bc8b96d947a737b85cbedc..094d6b42af2141a0d537fbec570b2c26dd06324e 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/logicref_simple.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/logicref_simple.res.oracle
@@ -39,7 +39,7 @@ Prove: true.
------------------------------------------------------------
Goal Post-condition (file tests/wp_hoare/logicref_simple.i, line 19) in 'fsimple_array':
-Let a = global(G_t_31).
+Let a = global(G_t_33).
Let x = Mint_0[shift_sint32(a, 3)].
Assume {
Type: is_sint32(x) /\ is_sint32(1 + x).
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
index 7c09c9927c004037dde903f98a89aafaa9348cef..cd88f4ec2a0806048f28f3598a2984d530930e84 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/dynamic.res.oracle
@@ -77,7 +77,7 @@ Prove: true.
Goal Call point f1 f2 in 'call' at instruction (file tests/wp_plugin/dynamic.i, line 30):
Let a = Mptr_0[shiftfield_F1_S_f(closure_0)].
-Let a_1 = global(G_f2_26).
+Let a_1 = global(G_f2_28).
Let a_2 = global(G_f1_20).
Let x = Mint_0[shiftfield_F1_S_param(closure_0)].
Assume {
@@ -137,7 +137,7 @@ Assume {
(* Heap *)
Have: (region(p.base) <= 0) /\ framed(Mptr_0).
(* Else *)
- Have: G_g_44 = 0.
+ Have: G_g_46 = 0.
}
Prove: X = 1.
@@ -165,7 +165,7 @@ Prove: true.
Goal Call point h1 in 'missing_context' at instruction (file tests/wp_plugin/dynamic.i, line 87):
Assume { (* Heap *) Have: region(p.base) <= 0. }
-Prove: global(G_h1_57) = p.
+Prove: global(G_h1_59) = p.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/flash.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/flash.0.res.oracle
index 930cc582729969ad5210ed514054bf4a08bba553..db2c070f9c272093ac5f6e002c583a1257a29bba 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/flash.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/flash.0.res.oracle
@@ -14,9 +14,9 @@ Prove: true.
Goal Post-condition 'A_reads' in 'job':
Let x = 1 + OBSERVER_time_0.
-Let a = global(G_a_60).
+Let a = global(G_a_62).
Let a_1 = C_RdAt_int(a).
-Let a_2 = global(G_b_61).
+Let a_2 = global(G_b_63).
Let a_3 = C_RdAt_int(a_2).
Let a_4 = C_WrAt_int(a_2).
Let a_5 = L_RD_update(L_INDEX_init, a).
@@ -58,9 +58,9 @@ Prove: L_RD_access(a_7, a) = 2.
Goal Post-condition 'B_reads' in 'job':
Let x = 1 + OBSERVER_time_0.
-Let a = global(G_a_60).
+Let a = global(G_a_62).
Let a_1 = C_RdAt_int(a).
-Let a_2 = global(G_b_61).
+Let a_2 = global(G_b_63).
Let a_3 = C_RdAt_int(a_2).
Let a_4 = C_WrAt_int(a_2).
Let a_5 = L_RD_update(L_INDEX_init, a).
@@ -102,9 +102,9 @@ Prove: L_RD_access(a_7, a_2) = 1.
Goal Post-condition 'B_writes' in 'job':
Let x = 1 + OBSERVER_time_0.
-Let a = global(G_a_60).
+Let a = global(G_a_62).
Let a_1 = C_RdAt_int(a).
-Let a_2 = global(G_b_61).
+Let a_2 = global(G_b_63).
Let a_3 = C_RdAt_int(a_2).
Let a_4 = C_WrAt_int(a_2).
Let a_5 = L_RD_update(L_INDEX_init, a).
@@ -146,9 +146,9 @@ Prove: L_WR_access(a_7, a_2) = 1.
Goal Post-condition 'ReadValues' in 'job':
Let x = 1 + OBSERVER_time_0.
-Let a = global(G_a_60).
+Let a = global(G_a_62).
Let a_1 = C_RdAt_int(a).
-Let a_2 = global(G_b_61).
+Let a_2 = global(G_b_63).
Let a_3 = C_RdAt_int(a_2).
Let a_4 = C_WrAt_int(a_2).
Let a_5 = L_RD_update(L_INDEX_init, a).
@@ -191,9 +191,9 @@ Prove: (x_6 + L_RD_value(a_2, L_RD_access(a_5, a_2))
Goal Post-condition 'WriteValues' in 'job':
Let x = 1 + OBSERVER_time_0.
-Let a = global(G_a_60).
+Let a = global(G_a_62).
Let a_1 = C_RdAt_int(a).
-Let a_2 = global(G_b_61).
+Let a_2 = global(G_b_63).
Let a_3 = C_RdAt_int(a_2).
Let a_4 = C_WrAt_int(a_2).
Let a_5 = L_RD_update(L_INDEX_init, a).
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle
index 6399033a6b70c8b442341cc0ced5952f48e0b092..ed8294e3ee5f853d6a6e156a292bfdf0f91efe21 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle
@@ -16,9 +16,9 @@ Prove: true.
Goal Post-condition 'A_reads' in 'job':
Let x = 1 + OBSERVER_time_0.
-Let a = global(G_a_60).
+Let a = global(G_a_62).
Let a_1 = C_RdAt_int(a).
-Let a_2 = global(G_b_61).
+Let a_2 = global(G_b_63).
Let a_3 = C_RdAt_int(a_2).
Let a_4 = C_WrAt_int(a_2).
Let a_5 = ((const(0))[(a) <- (const(0))[a]+1]).
@@ -59,9 +59,9 @@ Prove: (a_7)[a] = 2.
Goal Post-condition 'B_reads' in 'job':
Let x = 1 + OBSERVER_time_0.
-Let a = global(G_a_60).
+Let a = global(G_a_62).
Let a_1 = C_RdAt_int(a).
-Let a_2 = global(G_b_61).
+Let a_2 = global(G_b_63).
Let a_3 = C_RdAt_int(a_2).
Let a_4 = C_WrAt_int(a_2).
Let a_5 = ((const(0))[(a) <- (const(0))[a]+1]).
@@ -102,9 +102,9 @@ Prove: (a_7)[a_2] = 1.
Goal Post-condition 'B_writes' in 'job':
Let x = 1 + OBSERVER_time_0.
-Let a = global(G_a_60).
+Let a = global(G_a_62).
Let a_1 = C_RdAt_int(a).
-Let a_2 = global(G_b_61).
+Let a_2 = global(G_b_63).
Let a_3 = C_RdAt_int(a_2).
Let a_4 = C_WrAt_int(a_2).
Let a_5 = ((const(0))[(a) <- (const(0))[a]+1]).
@@ -145,9 +145,9 @@ Prove: (a_7)[a_2] = 1.
Goal Post-condition 'ReadValues' in 'job':
Let x = 1 + OBSERVER_time_0.
-Let a = global(G_a_60).
+Let a = global(G_a_62).
Let a_1 = C_RdAt_int(a).
-Let a_2 = global(G_b_61).
+Let a_2 = global(G_b_63).
Let a_3 = C_RdAt_int(a_2).
Let a_4 = C_WrAt_int(a_2).
Let a_5 = ((const(0))[(a) <- (const(0))[a]+1]).
@@ -188,9 +188,9 @@ Prove: (x_6 + L_RD_value(a_2, (a_5)[a_2]) + L_RD_value(a, (a_6)[a]))
Goal Post-condition 'WriteValues' in 'job':
Let x = 1 + OBSERVER_time_0.
-Let a = global(G_a_60).
+Let a = global(G_a_62).
Let a_1 = C_RdAt_int(a).
-Let a_2 = global(G_b_61).
+Let a_2 = global(G_b_63).
Let a_3 = C_RdAt_int(a_2).
Let a_4 = C_WrAt_int(a_2).
Let a_5 = ((const(0))[(a) <- (const(0))[a]+1]).
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/frame.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/frame.res.oracle
index 51dd9fadb379b12f2842de602d65e23435386708..8b51eb581fd1b78a01830ba0c3fbde6d22aee74c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/frame.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/frame.res.oracle
@@ -8,7 +8,7 @@
------------------------------------------------------------
Goal Post-condition 'KO' in 'alias':
-Let a = global(P_r_37).
+Let a = global(P_r_39).
Let x = Mint_1[a].
Let x_1 = Mint_0[a].
Assume {
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle
index 2705859a518ff4a771c046686685a4a90fd8f392..b558a7a6296bf15d1062d6fc9fa45545aadd40ba 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/overassign.res.oracle
@@ -39,15 +39,15 @@ Prove: true.
Goal Assigns nothing in 'f3_ok':
Call Effect at line 20
-Assume { (* Heap *) Have: (region(G_A_28) <= 0) /\ linked(Malloc_0). }
-Prove: invalid(Malloc_0, shift_sint32(global(G_A_28), 20), 10).
+Assume { (* Heap *) Have: (region(G_A_30) <= 0) /\ linked(Malloc_0). }
+Prove: invalid(Malloc_0, shift_sint32(global(G_A_30), 20), 10).
------------------------------------------------------------
Goal Assigns nothing in 'f3_ok':
Call Effect at line 20
-Assume { (* Heap *) Have: (region(G_A_28) <= 0) /\ linked(Malloc_0). }
-Prove: invalid(Malloc_0, shift_sint32(global(G_A_28), 20), 10).
+Assume { (* Heap *) Have: (region(G_A_30) <= 0) /\ linked(Malloc_0). }
+Prove: invalid(Malloc_0, shift_sint32(global(G_A_30), 20), 10).
------------------------------------------------------------
------------------------------------------------------------
@@ -56,15 +56,15 @@ Prove: invalid(Malloc_0, shift_sint32(global(G_A_28), 20), 10).
Goal Assigns nothing in 'f4_ok':
Call Effect at line 23
-Assume { (* Heap *) Have: (region(G_A_28) <= 0) /\ linked(Malloc_0). }
-Prove: invalid(Malloc_0, shift_sint32(global(G_A_28), -10), 10).
+Assume { (* Heap *) Have: (region(G_A_30) <= 0) /\ linked(Malloc_0). }
+Prove: invalid(Malloc_0, shift_sint32(global(G_A_30), -10), 10).
------------------------------------------------------------
Goal Assigns nothing in 'f4_ok':
Call Effect at line 23
-Assume { (* Heap *) Have: (region(G_A_28) <= 0) /\ linked(Malloc_0). }
-Prove: invalid(Malloc_0, shift_sint32(global(G_A_28), -10), 10).
+Assume { (* Heap *) Have: (region(G_A_30) <= 0) /\ linked(Malloc_0). }
+Prove: invalid(Malloc_0, shift_sint32(global(G_A_30), -10), 10).
------------------------------------------------------------
------------------------------------------------------------
@@ -73,15 +73,15 @@ Prove: invalid(Malloc_0, shift_sint32(global(G_A_28), -10), 10).
Goal Assigns nothing in 'f5_ko':
Call Effect at line 26
-Assume { (* Heap *) Have: (region(G_A_28) <= 0) /\ linked(Malloc_0). }
-Prove: invalid(Malloc_0, shift_sint32(global(G_A_28), 15), 10).
+Assume { (* Heap *) Have: (region(G_A_30) <= 0) /\ linked(Malloc_0). }
+Prove: invalid(Malloc_0, shift_sint32(global(G_A_30), 15), 10).
------------------------------------------------------------
Goal Assigns nothing in 'f5_ko':
Call Effect at line 26
-Assume { (* Heap *) Have: (region(G_A_28) <= 0) /\ linked(Malloc_0). }
-Prove: invalid(Malloc_0, shift_sint32(global(G_A_28), 15), 10).
+Assume { (* Heap *) Have: (region(G_A_30) <= 0) /\ linked(Malloc_0). }
+Prove: invalid(Malloc_0, shift_sint32(global(G_A_30), 15), 10).
------------------------------------------------------------
------------------------------------------------------------
@@ -90,14 +90,14 @@ Prove: invalid(Malloc_0, shift_sint32(global(G_A_28), 15), 10).
Goal Assigns nothing in 'f6_ko':
Call Effect at line 29
-Assume { (* Heap *) Have: (region(G_A_28) <= 0) /\ linked(Malloc_0). }
-Prove: invalid(Malloc_0, shift_sint32(global(G_A_28), -5), 10).
+Assume { (* Heap *) Have: (region(G_A_30) <= 0) /\ linked(Malloc_0). }
+Prove: invalid(Malloc_0, shift_sint32(global(G_A_30), -5), 10).
------------------------------------------------------------
Goal Assigns nothing in 'f6_ko':
Call Effect at line 29
-Assume { (* Heap *) Have: (region(G_A_28) <= 0) /\ linked(Malloc_0). }
-Prove: invalid(Malloc_0, shift_sint32(global(G_A_28), -5), 10).
+Assume { (* Heap *) Have: (region(G_A_30) <= 0) /\ linked(Malloc_0). }
+Prove: invalid(Malloc_0, shift_sint32(global(G_A_30), -5), 10).
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_store/oracle/struct.res.oracle b/src/plugins/wp/tests/wp_store/oracle/struct.res.oracle
index d69745e50d839f08b8a21aa2c33fcfabaf055c04..643bf5f86172de5f77badd11e749a010ba000939 100644
--- a/src/plugins/wp/tests/wp_store/oracle/struct.res.oracle
+++ b/src/plugins/wp/tests/wp_store/oracle/struct.res.oracle
@@ -43,7 +43,7 @@ Prove: true.
------------------------------------------------------------
Goal Post-condition 'P,qed_ok' in 'main':
-Let a = global(G_v_26).
+Let a = global(G_v_28).
Let a_1 = Load_S2_St(a, Mint_0).
Assume {
Type: IsS2_St(w) /\ IsS2_St(a_1).
@@ -56,14 +56,14 @@ Assume {
(* Initializer *)
Init: Mint_0[shiftfield_F2_St_b(a)] = 2.
(* Heap *)
- Have: region(G_v_26) <= 0.
+ Have: region(G_v_28) <= 0.
}
Prove: EqS2_St(a_1, w).
------------------------------------------------------------
Goal Post-condition 'Q,qed_ok' in 'main':
-Let a = global(G_v_26).
+Let a = global(G_v_28).
Let a_1 = Load_S2_St(a, Mint_0).
Assume {
Type: IsS2_St(w) /\ IsS2_St(a_1).
@@ -76,7 +76,7 @@ Assume {
(* Initializer *)
Init: Mint_0[shiftfield_F2_St_b(a)] = 2.
(* Heap *)
- Have: region(G_v_26) <= 0.
+ Have: region(G_v_28) <= 0.
}
Prove: EqS2_St(a_1, w).
diff --git a/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle
index ce3ab2bb5ad7807a072b8fd79d8782f443d6e444..d9091a0916603f3ff78d67fa15570d37b84120ac 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle
@@ -253,7 +253,7 @@ Assume {
When: (0 <= i) /\ (i <= 499).
(* Initializer *)
Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 499) ->
- (p[i_1] = global(G_p0_26)))).
+ (p[i_1] = global(G_p0_28)))).
(* Heap *)
Have: linked(Malloc_0).
}
diff --git a/src/plugins/wp/tests/wp_typed/oracle/array_initialized.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/array_initialized.1.res.oracle
index 5a70949456390d3b76d519cff7584df40af71625..390cc16f0e0e92e62bc0d1de50d31de962117534 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/array_initialized.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/array_initialized.1.res.oracle
@@ -26,8 +26,8 @@ Prove: Mint_0[shift_sint32(a, i)] = 0.
------------------------------------------------------------
Goal Assertion (file tests/wp_typed/array_initialized.c, line 185):
-Let a = global(K_h1_22).
-Let a_1 = global(K_h2_23).
+Let a = global(K_h1_24).
+Let a_1 = global(K_h2_25).
Assume {
(* Goal *)
When: (0 <= i) /\ (i <= 499).
@@ -254,13 +254,13 @@ Prove: true.
------------------------------------------------------------
Goal Assertion (file tests/wp_typed/array_initialized.c, line 283):
-Let a = global(K_p_30).
+Let a = global(K_p_32).
Assume {
(* Goal *)
When: (0 <= i) /\ (i <= 499).
(* Initializer *)
Init: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 499) ->
- (Mptr_0[shift_PTR(a, i_1)] = global(G_p0_29)))).
+ (Mptr_0[shift_PTR(a, i_1)] = global(G_p0_31)))).
(* Heap *)
Have: framed(Mptr_0) /\ linked(Malloc_0).
}
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
index 86999a74131fbcf821d72d8dc22c18a0b8225a7c..46aa576f42c2d5833b4296cf2270a33af2fe4af4 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
@@ -232,7 +232,7 @@ Prove: true.
------------------------------------------------------------
Goal Post-condition (file tests/wp_typed/user_init.i, line 127) in 'init_t2_bis_v1':
-Let a = global(G_t2_48).
+Let a = global(G_t2_50).
Assume {
Type: is_uint32(i_2) /\ is_sint32(v).
(* Goal *)
@@ -262,7 +262,7 @@ Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 136):
-Let a = global(G_t2_48).
+Let a = global(G_t2_50).
Let a_1 = shift_A20_sint32(a, i).
Let a_2 = shift_sint32(a_1, 0).
Let a_3 = havoc(Mint_undef_0, Mint_0, a_2, 20).
@@ -298,7 +298,7 @@ Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant 'Range' (file tests/wp_typed/user_init.i, line 135):
-Let a = global(G_t2_48).
+Let a = global(G_t2_50).
Let a_1 = shift_A20_sint32(a, i).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
@@ -342,7 +342,7 @@ Prove: true.
Goal Loop assigns 'lack,Zone' (2/3):
Effect at line 139
-Let a = global(G_t2_48).
+Let a = global(G_t2_50).
Let a_1 = shift_A20_sint32(a, i).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
@@ -379,7 +379,7 @@ Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
Goal Loop assigns 'lack,Zone' (3/3):
Call Effect at line 140
-Let a = global(G_t2_48).
+Let a = global(G_t2_50).
Let a_1 = shift_A20_sint32(a, i).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
@@ -428,7 +428,7 @@ Assume {
Have: forall a : addr.
((forall i_5,i_4 : Z. ((0 <= i_4) -> ((0 <= i_5) -> ((i_5 <= 9) ->
((i_4 <= 19) ->
- (shift_sint32(shift_A20_sint32(global(G_t2_48), i_5), i_4) != a)))))) ->
+ (shift_sint32(shift_A20_sint32(global(G_t2_50), i_5), i_4) != a)))))) ->
(Mint_0[a] = Mint_1[a])).
}
Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
@@ -463,7 +463,7 @@ Assume {
Have: forall a : addr.
((forall i_5,i_4 : Z. ((0 <= i_4) -> ((0 <= i_5) -> ((i_5 <= 9) ->
((i_4 <= 19) ->
- (shift_sint32(shift_A20_sint32(global(G_t2_48), i_5), i_4) != a)))))) ->
+ (shift_sint32(shift_A20_sint32(global(G_t2_50), i_5), i_4) != a)))))) ->
(Mint_0[a] = Mint_1[a])).
}
Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
@@ -472,7 +472,7 @@ Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
------------------------------------------------------------
Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 139):
-Let a = global(G_t2_48).
+Let a = global(G_t2_50).
Let a_1 = shift_A20_sint32(a, i).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
@@ -520,7 +520,7 @@ Prove: true.
------------------------------------------------------------
Goal Post-condition (file tests/wp_typed/user_init.i, line 145) in 'init_t2_bis_v2':
-Let a = global(G_t2_48).
+Let a = global(G_t2_50).
Assume {
Type: is_uint32(i_2) /\ is_sint32(v).
(* Goal *)
@@ -549,7 +549,7 @@ Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 154):
-Let a = global(G_t2_48).
+Let a = global(G_t2_50).
Let a_1 = shift_A20_sint32(a, i).
Let a_2 = shift_sint32(a_1, 0).
Let a_3 = havoc(Mint_undef_0, Mint_0, a_2, 20).
@@ -584,7 +584,7 @@ Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant 'Range' (file tests/wp_typed/user_init.i, line 153):
-Let a = global(G_t2_48).
+Let a = global(G_t2_50).
Let a_1 = shift_A20_sint32(a, i).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
@@ -627,7 +627,7 @@ Prove: true.
Goal Loop assigns 'tactic,Zone' (2/3):
Effect at line 157
-Let a = global(G_t2_48).
+Let a = global(G_t2_50).
Let a_1 = shift_A20_sint32(a, i_2).
Assume {
Have: 0 <= i.
@@ -660,7 +660,7 @@ Prove: exists i_6,i_5 : Z. (i_6 <= i) /\ (i_5 <= i_1) /\ (i_1 <= i_5) /\
Goal Loop assigns 'tactic,Zone' (3/3):
Call Effect at line 158
-Let a = global(G_t2_48).
+Let a = global(G_t2_50).
Let a_1 = shift_A20_sint32(a, i).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
@@ -705,7 +705,7 @@ Assume {
(* Loop assigns 'tactic,Zone' *)
Have: forall a : addr.
((forall i_5,i_4 : Z. ((0 <= i_5) -> ((i_5 <= 9) ->
- (shift_sint32(shift_A20_sint32(global(G_t2_48), i_5), i_4) != a)))) ->
+ (shift_sint32(shift_A20_sint32(global(G_t2_50), i_5), i_4) != a)))) ->
(Mint_0[a] = Mint_1[a])).
}
Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (i_1 <= i_4) /\
@@ -737,7 +737,7 @@ Assume {
(* Loop assigns 'tactic,Zone' *)
Have: forall a : addr.
((forall i_5,i_4 : Z. ((0 <= i_5) -> ((i_5 <= 9) ->
- (shift_sint32(shift_A20_sint32(global(G_t2_48), i_5), i_4) != a)))) ->
+ (shift_sint32(shift_A20_sint32(global(G_t2_50), i_5), i_4) != a)))) ->
(Mint_0[a] = Mint_1[a])).
}
Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (i_1 <= i_4) /\
@@ -746,7 +746,7 @@ Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (i_1 <= i_4) /\
------------------------------------------------------------
Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 157):
-Let a = global(G_t2_48).
+Let a = global(G_t2_50).
Let a_1 = shift_A20_sint32(a, i).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
index 847496eab27e2dc4b13dbd1c913be550dd2aeda9..8cb6dcfb82a04271e1eb1496d621b9a835dd9371 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
@@ -232,7 +232,7 @@ Prove: true.
------------------------------------------------------------
Goal Post-condition (file tests/wp_typed/user_init.i, line 127) in 'init_t2_bis_v1':
-Let a = global(G_t2_48).
+Let a = global(G_t2_50).
Assume {
Type: is_uint32(i_2) /\ is_sint32(v).
(* Goal *)
@@ -262,7 +262,7 @@ Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 136):
-Let a = global(G_t2_48).
+Let a = global(G_t2_50).
Let a_1 = shift_A20_sint32(a, i).
Let a_2 = shift_sint32(a_1, 0).
Let a_3 = havoc(Mint_undef_0, Mint_0, a_2, 20).
@@ -298,7 +298,7 @@ Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant 'Range' (file tests/wp_typed/user_init.i, line 135):
-Let a = global(G_t2_48).
+Let a = global(G_t2_50).
Let a_1 = shift_A20_sint32(a, i).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
@@ -342,7 +342,7 @@ Prove: true.
Goal Loop assigns 'lack,Zone' (2/3):
Effect at line 139
-Let a = global(G_t2_48).
+Let a = global(G_t2_50).
Let a_1 = shift_A20_sint32(a, i).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
@@ -379,7 +379,7 @@ Prove: (forall i_4,i_3 : Z. ((0 <= i_3) -> ((0 <= i_4) -> ((i_4 <= 9) ->
Goal Loop assigns 'lack,Zone' (3/3):
Call Effect at line 140
-Let a = global(G_t2_48).
+Let a = global(G_t2_50).
Let a_1 = shift_A20_sint32(a, i).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
@@ -428,7 +428,7 @@ Assume {
Have: forall a : addr.
((forall i_5,i_4 : Z. ((0 <= i_4) -> ((0 <= i_5) -> ((i_5 <= 9) ->
((i_4 <= 19) ->
- (shift_sint32(shift_A20_sint32(global(G_t2_48), i_5), i_4) != a)))))) ->
+ (shift_sint32(shift_A20_sint32(global(G_t2_50), i_5), i_4) != a)))))) ->
(Mint_0[a] = Mint_1[a])).
}
Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
@@ -463,7 +463,7 @@ Assume {
Have: forall a : addr.
((forall i_5,i_4 : Z. ((0 <= i_4) -> ((0 <= i_5) -> ((i_5 <= 9) ->
((i_4 <= 19) ->
- (shift_sint32(shift_A20_sint32(global(G_t2_48), i_5), i_4) != a)))))) ->
+ (shift_sint32(shift_A20_sint32(global(G_t2_50), i_5), i_4) != a)))))) ->
(Mint_0[a] = Mint_1[a])).
}
Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
@@ -472,7 +472,7 @@ Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_4) /\
------------------------------------------------------------
Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 139):
-Let a = global(G_t2_48).
+Let a = global(G_t2_50).
Let a_1 = shift_A20_sint32(a, i).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
@@ -520,7 +520,7 @@ Prove: true.
------------------------------------------------------------
Goal Post-condition (file tests/wp_typed/user_init.i, line 145) in 'init_t2_bis_v2':
-Let a = global(G_t2_48).
+Let a = global(G_t2_50).
Assume {
Type: is_uint32(i_2) /\ is_sint32(v).
(* Goal *)
@@ -549,7 +549,7 @@ Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant 'Partial' (file tests/wp_typed/user_init.i, line 154):
-Let a = global(G_t2_48).
+Let a = global(G_t2_50).
Let a_1 = shift_A20_sint32(a, i).
Let a_2 = shift_sint32(a_1, 0).
Let a_3 = havoc(Mint_undef_0, Mint_0, a_2, 20).
@@ -584,7 +584,7 @@ Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant 'Range' (file tests/wp_typed/user_init.i, line 153):
-Let a = global(G_t2_48).
+Let a = global(G_t2_50).
Let a_1 = shift_A20_sint32(a, i).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
@@ -627,7 +627,7 @@ Prove: true.
Goal Loop assigns 'tactic,Zone' (2/3):
Effect at line 157
-Let a = global(G_t2_48).
+Let a = global(G_t2_50).
Let a_1 = shift_A20_sint32(a, i_2).
Assume {
Have: 0 <= i.
@@ -660,7 +660,7 @@ Prove: exists i_6,i_5 : Z. (i_6 <= i) /\ (i_5 <= i_1) /\ (i_1 <= i_5) /\
Goal Loop assigns 'tactic,Zone' (3/3):
Call Effect at line 158
-Let a = global(G_t2_48).
+Let a = global(G_t2_50).
Let a_1 = shift_A20_sint32(a, i).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
@@ -705,7 +705,7 @@ Assume {
(* Loop assigns 'tactic,Zone' *)
Have: forall a : addr.
((forall i_5,i_4 : Z. ((0 <= i_5) -> ((i_5 <= 9) ->
- (shift_sint32(shift_A20_sint32(global(G_t2_48), i_5), i_4) != a)))) ->
+ (shift_sint32(shift_A20_sint32(global(G_t2_50), i_5), i_4) != a)))) ->
(Mint_0[a] = Mint_1[a])).
}
Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (i_1 <= i_4) /\
@@ -737,7 +737,7 @@ Assume {
(* Loop assigns 'tactic,Zone' *)
Have: forall a : addr.
((forall i_5,i_4 : Z. ((0 <= i_5) -> ((i_5 <= 9) ->
- (shift_sint32(shift_A20_sint32(global(G_t2_48), i_5), i_4) != a)))) ->
+ (shift_sint32(shift_A20_sint32(global(G_t2_50), i_5), i_4) != a)))) ->
(Mint_0[a] = Mint_1[a])).
}
Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (i_1 <= i_4) /\
@@ -746,7 +746,7 @@ Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (i_1 <= i_4) /\
------------------------------------------------------------
Goal Decreasing of Loop variant at loop (file tests/wp_typed/user_init.i, line 157):
-Let a = global(G_t2_48).
+Let a = global(G_t2_50).
Let a_1 = shift_A20_sint32(a, i).
Assume {
Type: is_uint32(i) /\ is_sint32(v).
diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle
index 191e73fc5ccac0ecc6e0153d2061e39116a595e6..4d2f07be6ab7dd7b776d2f3b1c1b47455aa5ca58 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle
@@ -54,7 +54,7 @@ Prove: true.
------------------------------------------------------------
Goal Post-condition 'KO' in 'observer':
-Let a = global(G_a_41).
+Let a = global(G_a_43).
Let x = Mint_0[shiftfield_F1_S_f(a)].
Let x_1 = Mint_0[shiftfield_F1_S_g(a)].
Let x_2 = 1 + x.
diff --git a/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.0.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.0.res.oracle
index e183de2d49267294a0711f2f0803a8148194950d..0dc5561959eaa13718b53698eb15a584c53af8f2 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.0.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.0.res.oracle
@@ -222,8 +222,8 @@ Prove: true.
------------------------------------------------------------
Goal Post-condition 'memcpy,ok' in 'memcpy_context_vars':
-Let a = Mptr_0[global(P_src_43)].
-Let a_1 = Mptr_0[global(P_dst_44)].
+Let a = Mptr_0[global(P_src_45)].
+Let a_1 = Mptr_0[global(P_dst_46)].
Let a_2 = shift_uint8(a_1, 0).
Let a_3 = havoc(Mint_undef_0, Mint_0, a_2, len_0).
Let a_4 = shift_uint8(a, 0).
@@ -253,8 +253,8 @@ Prove: a_3[shift_uint8(a_1, i)] = Mint_0[shift_uint8(a, i)].
------------------------------------------------------------
Goal Post-condition 'unmodified,ok' in 'memcpy_context_vars':
-Let a = Mptr_0[global(P_src_43)].
-Let a_1 = Mptr_0[global(P_dst_44)].
+Let a = Mptr_0[global(P_src_45)].
+Let a_1 = Mptr_0[global(P_dst_46)].
Let a_2 = shift_uint8(a_1, 0).
Let a_3 = havoc(Mint_undef_0, Mint_0, a_2, len_0).
Let a_4 = shift_uint8(a, 0).
@@ -285,8 +285,8 @@ Prove: a_3[a_5] = Mint_0[a_5].
------------------------------------------------------------
Goal Preservation of Invariant 'ok,cpy' (file tests/wp_usage/issue-189-bis.i, line 55):
-Let a = Mptr_0[global(P_src_43)].
-Let a_1 = Mptr_0[global(P_dst_44)].
+Let a = Mptr_0[global(P_src_45)].
+Let a_1 = Mptr_0[global(P_dst_46)].
Let a_2 = shift_uint8(a_1, 0).
Let a_3 = havoc(Mint_undef_0, Mint_0, a_2, len_0).
Let a_4 = shift_uint8(a, 0).
@@ -332,8 +332,8 @@ Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant 'ok,len' (file tests/wp_usage/issue-189-bis.i, line 51):
-Let a = Mptr_0[global(P_src_43)].
-Let a_1 = Mptr_0[global(P_dst_44)].
+Let a = Mptr_0[global(P_src_45)].
+Let a_1 = Mptr_0[global(P_dst_46)].
Let a_2 = shift_uint8(a_1, 0).
Let a_3 = havoc(Mint_undef_0, Mint_0, a_2, len_1).
Let a_4 = shift_uint8(a, 0).
@@ -394,15 +394,15 @@ Prove: true.
Goal Loop assigns (file tests/wp_usage/issue-189-bis.i, line 54) (4/4):
Effect at line 60
-Let a = Mptr_0[global(P_src_43)].
-Let a_1 = Mptr_0[global(P_dst_44)].
+Let a = Mptr_0[global(P_src_45)].
+Let a_1 = Mptr_0[global(P_dst_46)].
Let a_2 = shift_uint8(a_1, 0).
Let a_3 = havoc(Mint_undef_0, Mint_0, a_2, len_0).
Let a_4 = shift_uint8(a, 0).
Assume {
Type: is_sint32(len_0) /\ is_sint32(len_1).
(* Goal *)
- When: !invalid(Malloc_0[P_src_43 <- 1][P_dst_44 <- 1], tmp_0, 1).
+ When: !invalid(Malloc_0[P_src_45 <- 1][P_dst_46 <- 1], tmp_0, 1).
(* Heap *)
Have: framed(Mptr_0) /\ linked(Malloc_0).
(* Pre-condition *)
diff --git a/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle
index dc14184986d41184ac5396abbefc28a30c6f9ca9..911ac911111e8ac2b3fee82d06a8e172205cd441 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/issue-189-bis.1.res.oracle
@@ -5,8 +5,8 @@
[wp] Warning: Missing RTE guards
Goal Post-condition 'memcpy,ok' in 'memcpy_context_vars':
-Let a = global(G_src_43).
-Let a_1 = global(G_dst_44).
+Let a = global(G_src_45).
+Let a_1 = global(G_dst_46).
Let a_2 = havoc(Mint_undef_0, Mint_0, shift_uint8(a_1, 0), len_0).
Assume {
Type: is_sint32(len_0) /\ is_sint32(len_1).
@@ -38,8 +38,8 @@ Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant 'ok,cpy' (file tests/wp_usage/issue-189-bis.i, line 55):
-Let a = global(G_src_43).
-Let a_1 = global(G_dst_44).
+Let a = global(G_src_45).
+Let a_1 = global(G_dst_46).
Let a_2 = havoc(Mint_undef_0, Mint_0, shift_uint8(a_1, 0), len_0).
Let a_3 = a_2[dst2_0 <- a_2[src2_0]].
Assume {
@@ -82,8 +82,8 @@ Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant 'ok,len' (file tests/wp_usage/issue-189-bis.i, line 51):
-Let a = global(G_src_43).
-Let a_1 = global(G_dst_44).
+Let a = global(G_src_45).
+Let a_1 = global(G_dst_46).
Assume {
Type: is_sint32(len_1) /\ is_sint32(len_0) /\ is_sint32(len_0 - 1).
(* Heap *)
@@ -141,8 +141,8 @@ Prove: true.
Goal Loop assigns (file tests/wp_usage/issue-189-bis.i, line 54) (4/4):
Effect at line 60
-Let a = global(G_src_43).
-Let a_1 = global(G_dst_44).
+Let a = global(G_src_45).
+Let a_1 = global(G_dst_46).
Let a_2 = shift_uint8(a_1, 0).
Assume {
Type: is_sint32(len_0) /\ is_sint32(len_1).
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 0e7823ec685103d07645efcea8e3cceae7ffcdb0..1aff068563351acc6645093e0e04f1ae70b3f644 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -4783,7 +4783,7 @@ int unsetenv(char const *name)
requires
alignment_is_a_suitable_power_of_two:
alignment ≥ sizeof(void *) ∧
- ((unsigned int)alignment & ((unsigned int)alignment - 1)) ≡ 0;
+ ((size_t)alignment & ((size_t)alignment - 1)) ≡ 0;
assigns __fc_heap_status, \result;
assigns __fc_heap_status
\from (indirect: alignment), size, __fc_heap_status;
@@ -4820,7 +4820,7 @@ int posix_memalign(void **memptr, size_t alignment, size_t size)
assert
alignment_is_a_suitable_power_of_two:
alignment ≥ sizeof(void *) ∧
- ((unsigned int)alignment & ((unsigned int)alignment - 1)) ≡ 0;
+ ((size_t)alignment & ((size_t)alignment - 1)) ≡ 0;
*/
;
*memptr = malloc(size);
@@ -6893,7 +6893,7 @@ char *__fc_p_basename = __fc_basename;
null_or_valid_string_path: path ≡ \null ∨ valid_read_string(path);
ensures
result_points_to_internal_storage_or_path:
- \subset(\result, \union(__fc_p_basename, \old(path)));
+ \subset(\result, {__fc_p_basename, \old(path)});
assigns *(path + (0 ..)), __fc_basename[0 ..], \result;
assigns *(path + (0 ..)) \from *(path + (0 ..)), __fc_basename[0 ..];
assigns __fc_basename[0 ..] \from *(path + (0 ..)), __fc_basename[0 ..];
@@ -6908,7 +6908,7 @@ char *__fc_p_dirname = __fc_dirname;
null_or_valid_string_path: path ≡ \null ∨ valid_read_string(path);
ensures
result_points_to_internal_storage_or_path:
- \subset(\result, \union(__fc_p_dirname, \old(path)));
+ \subset(\result, {__fc_p_dirname, \old(path)});
assigns *(path + (0 ..)), __fc_dirname[0 ..], \result;
assigns *(path + (0 ..)) \from *(path + (0 ..)), __fc_dirname[0 ..];
assigns __fc_dirname[0 ..] \from *(path + (0 ..)), __fc_dirname[0 ..];
diff --git a/tests/misc/booleans.i b/tests/misc/booleans.i
new file mode 100644
index 0000000000000000000000000000000000000000..08cbc6cbd89c770448b363d827b620424faf1faa
--- /dev/null
+++ b/tests/misc/booleans.i
@@ -0,0 +1,8 @@
+/*run.config
+ OPT: -eva -print
+*/
+int main (void) {
+ int x = 42;
+ /*@ check (boolean)x == 17; */
+ /*@ check (integer)(boolean)x == 17; */
+}
diff --git a/tests/misc/oracle/booleans.res.oracle b/tests/misc/oracle/booleans.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..8f7927c6bceb80d83a27026a4ecd2ad4e9c7862b
--- /dev/null
+++ b/tests/misc/oracle/booleans.res.oracle
@@ -0,0 +1,38 @@
+[kernel] Parsing tests/misc/booleans.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva:alarm] tests/misc/booleans.i:7: Warning: check got status invalid.
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ x ∈ {42}
+ __retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 5 statements reached (out of 5): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 1 valid 0 unknown 1 invalid 2 total
+ Preconditions 0 valid 0 unknown 0 invalid 0 total
+ 50% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
+/* Generated by Frama-C */
+int main(void)
+{
+ int __retres;
+ int x = 42;
+ /*@ check (x ≢ 0) ≡ (17 ≢ 0); */ ;
+ /*@ check ((ℤ)x ≢ 0) ≡ 17; */ ;
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/tests/spec/logic_type.c b/tests/spec/logic_type.c
index 0b8380d9dc8b4db0c54999da8158c97fa4860dca..008bec88b3cfccc932e2acee9028e9b07b33aa4c 100644
--- a/tests/spec/logic_type.c
+++ b/tests/spec/logic_type.c
@@ -26,3 +26,11 @@ Point tab[3];
void h(void) {
f(tab) ;
}
+
+//@ logic t t_from_t(t x) = (t) x;
+
+//@ logic _Bool _Bool_from_boolean(boolean b) = (_Bool) b;
+
+//@ logic boolean boolean_from_integer(integer b) = (boolean) b;
+//@ logic boolean boolean_from_int(int b) = (boolean) b;
+//@ logic boolean boolean_from_Bool(_Bool b) = (boolean) b;
diff --git a/tests/spec/oracle/float-acsl.res.oracle b/tests/spec/oracle/float-acsl.res.oracle
index 5ef02bf9f069b305eaa338251ce54fa1f4e16d12..8073bef4e574f3d166e4f8735853336b0b3c56d0 100644
--- a/tests/spec/oracle/float-acsl.res.oracle
+++ b/tests/spec/oracle/float-acsl.res.oracle
@@ -28,12 +28,8 @@ double minus_one(void);
*/
float minus_onef(void);
-/*@ requires
- /* (coercion to:℠*/x/* ) */ ≤ /* (coercion to:℠*/y/* ) */;
- ensures
- /* (coercion to:℠*/\old(x)/* ) */ ≤
- /* (coercion to:℠*/\result/* ) */ ≤
- /* (coercion to:â„ */\old(y)/* ) */;
+/*@ requires (â„)x ≤ (â„)y;
+ ensures (â„)\old(x) ≤ (â„)\result ≤ (â„)\old(y);
assigns \result;
assigns \result \from x, y;
*/
diff --git a/tests/spec/oracle/logic_type.res.oracle b/tests/spec/oracle/logic_type.res.oracle
index 4521f06fa5f83b07057e401646a935c01cf0979d..c7f4d27c228754c51e314be1178c710e024d7775 100644
--- a/tests/spec/oracle/logic_type.res.oracle
+++ b/tests/spec/oracle/logic_type.res.oracle
@@ -51,4 +51,15 @@ void h(void)
return;
}
+/*@ logic t t_from_t(t x) = x;
+ */
+/*@ logic _Bool _Bool_from_boolean(𔹠b) = (_Bool)b;
+ */
+/*@ logic 𔹠boolean_from_integer(ℤ b) = b ≢ 0;
+ */
+/*@ logic 𔹠boolean_from_int(int b) = b ≢ 0;
+ */
+/*@ logic 𔹠boolean_from_Bool(_Bool b) = b ≢ 0;
+
+*/
diff --git a/tests/syntax/oracle/static_formals_1.res.oracle b/tests/syntax/oracle/static_formals_1.res.oracle
index a699b713faad14c29361449e3f4a8152e80d9635..33d75e1e69f2608ecd23ae500afad522912fb7ac 100644
--- a/tests/syntax/oracle/static_formals_1.res.oracle
+++ b/tests/syntax/oracle/static_formals_1.res.oracle
@@ -2,23 +2,23 @@
[kernel] Parsing tests/syntax/static_formals_2.c (with preprocessing)
/* Generated by Frama-C */
/*@ requires /* vid:23, lvid:23 */x < 10; */
-static int /* vid:52 */f(int /* vid:23, lvid:23 */x);
+static int /* vid:54 */f(int /* vid:23, lvid:23 */x);
-int /* vid:26 */g(void)
+int /* vid:28 */g(void)
{
- int /* vid:27 */tmp;
- /* vid:27 */tmp = /* vid:52 */f(4);
- return /* vid:27 */tmp;
+ int /* vid:29 */tmp;
+ /* vid:29 */tmp = /* vid:54 */f(4);
+ return /* vid:29 */tmp;
}
-/*@ requires /* vid:47, lvid:47 */x < 10; */
-static int /* vid:53 */f_0(int /* vid:47, lvid:47 */x);
+/*@ requires /* vid:49, lvid:49 */x < 10; */
+static int /* vid:55 */f_0(int /* vid:49, lvid:49 */x);
-int /* vid:50 */h(void)
+int /* vid:52 */h(void)
{
- int /* vid:51 */tmp;
- /* vid:51 */tmp = /* vid:53 */f_0(6);
- return /* vid:51 */tmp;
+ int /* vid:53 */tmp;
+ /* vid:53 */tmp = /* vid:55 */f_0(6);
+ return /* vid:53 */tmp;
}