diff --git a/Makefile b/Makefile
index 582741e0b7567594271b8b4618460975daea49e5..90e779f26d5e8b41b527d0d974ff726fedb5e349 100644
--- a/Makefile
+++ b/Makefile
@@ -1288,6 +1288,14 @@ gui: gui-$(OCAMLBEST)
ALL_GUI_CMO= $(ALL_CMO) $(GRAPH_GUICMO) $(GUICMO)
ALL_GUI_CMX= $(patsubst %.cma,%.cmxa,$(ALL_GUI_CMO:.cmo=.cmx))
+ifeq ($(LABLGTK_VERSION),3)
+ifeq ($(NATIVE_THREADS),yes)
+THREAD=-thread
+else
+THREAD=-vmthread
+endif
+endif
+
bin/viewer.byte$(EXE): BYTE_LIBS+= $(GRAPH_GUICMO)
bin/viewer.byte$(EXE): $(filter-out $(GRAPH_GUICMO),$(ALL_GUI_CMO)) \
$(GEN_BYTE_LIBS) \
@@ -2297,21 +2305,21 @@ PTESTS_SRC=ptests/ptests_config.ml ptests/ptests.ml
PTESTS_CONFIG:= $(shell if test -d tests; then echo tests/ptests_config; fi)
ifeq ($(NATIVE_THREADS),yes)
-THREAD=-thread
+PTEST_THREAD=-thread
ptests: bin/ptests.$(PTESTSBEST)$(EXE) $(PTESTS_CONFIG)
else
-THREAD=-vmthread
+PTEST_THREAD=-vmthread
ptests: bin/ptests.byte$(EXE) $(PTESTS_CONFIG)
endif
bin/ptests.byte$(EXE): $(PTESTS_SRC)
$(PRINT_LINKING) $@
- $(OCAMLC) -I ptests -dtypes $(THREAD) -g -o $@ \
+ $(OCAMLC) -I ptests -dtypes $(PTEST_THREAD) -g -o $@ \
unix.cma threads.cma str.cma dynlink.cma $^
bin/ptests.opt$(EXE): $(PTESTS_SRC)
$(PRINT_LINKING) $@
- $(OCAMLOPT) -I ptests -dtypes $(THREAD) -o $@ \
+ $(OCAMLOPT) -I ptests -dtypes $(PTEST_THREAD) -o $@ \
unix.cmxa threads.cmxa str.cmxa dynlink.cmxa $^
GENERATED+=ptests/ptests_config.ml tests/ptests_config
diff --git a/configure.in b/configure.in
index 09121c03098bc616365e96ecc5ce9d4d9387366c..1c508452c3e88478318f82fff46c8a61dbe09c0f 100644
--- a/configure.in
+++ b/configure.in
@@ -424,6 +424,7 @@ rm -f test_os_type.cmi test_os_type.cmo test_os_type.ml test_os_type
if test "$OCAML_OS_TYPE" = "Win32"; then
AC_MSG_RESULT(Win32)
AC_CHECK_PROG(CYGPATH,cygpath,cygpath,no)
+ PLATFORM=Win32
OCAMLWIN32=yes
EXE=.exe
# OCaml on Win32 does not support vmthreads, use native ones.
@@ -432,9 +433,16 @@ else
OCAMLWIN32=no
if test "$OCAML_OS_TYPE" = "Cygwin"; then
AC_MSG_RESULT(Cygwin)
+ PLATFORM=Cygwin
EXE=.exe
else
- AC_MSG_RESULT(Unix)
+ if test $(uname -s) = "Darwin"; then
+ AC_MSG_RESULT(MacOS)
+ PLATFORM=MacOS
+ else
+ AC_MSG_RESULT(Unix)
+ PLATFORM=Unix
+ fi
EXE=
fi
@@ -938,13 +946,14 @@ USE_LABLGTK="$USE_LABLGTK$USE_GNOMECANVAS"
LABLGTK_PATH=""
SOURCEVIEW_PATH=""
+if test "$PLATFORM" != "MacOS"; then
if test "$ENABLE_LABLGTK3" = "yes"; then
LABLGTK_PATH=`ocamlfind query lablgtk3 | tr -d '\\r\\n'`;
fi
-
if test "$LABLGTK_PATH" != ""; then
SOURCEVIEW_PATH=`ocamlfind query lablgtk3-sourceview3 | tr -d '\\r\\n'`;
fi
+fi
if test "$SOURCEVIEW_PATH" = ""; then
LABLGTK_VERSION=2
@@ -1016,6 +1025,7 @@ check_frama_c_dependencies
EXTERNAL_PLUGINS="${EXTERNAL_PLUGINS} ${EXTRA_EXTERNAL_PLUGINS}"
+AC_SUBST(PLATFORM)
AC_SUBST(VERBOSEMAKE)
AC_SUBST(DEVELOPMENT)
AC_SUBST(DOT)
diff --git a/opam/opam b/opam/opam
index 16ea05f0d3eb81cba33aaff3e84e8d87cac22374..bda948e9199b27790ffd9fac8029f18e26587ee0 100644
--- a/opam/opam
+++ b/opam/opam
@@ -90,7 +90,7 @@ depends: [
"zarith"
"conf-autoconf" { build }
( ( "lablgtk" { >= "2.18.2" } & "conf-gnomecanvas" )
- | ( "lablgtk3" { >= "3.0.beta4" } & "lablgtk3-sourceview3"))
+ | ( "lablgtk3" { >= "3.0.beta4" & os!="macos" } & "lablgtk3-sourceview3" ))
"conf-gtksourceview"
( "alt-ergo-free" | "alt-ergo" )
"conf-graphviz" { post }
diff --git a/share/Makefile.config.in b/share/Makefile.config.in
index f6b545148e78dc450b717a4f7d9b5c539f4a0cfc..f0bc8ae518d5973c1e46e30e979ecf6e1dcdfd73 100644
--- a/share/Makefile.config.in
+++ b/share/Makefile.config.in
@@ -91,6 +91,7 @@ HAS_OCAML405 ?=@HAS_OCAML405@
HAS_OCAML407 ?=@HAS_OCAML407@
HAS_OCAML408 ?=@HAS_OCAML408@
+PLATFORM ?=@PLATFORM@
NATIVE_THREADS ?=@HAS_NATIVE_THREADS@
OCAMLWIN32 ?=@OCAMLWIN32@
PTESTSBEST ?=@PTESTSBEST@
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/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/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/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/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/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/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/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_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/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/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_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/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/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/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/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
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;
}