diff --git a/src/kernel_services/ast_queries/acsl_extension.mli b/src/kernel_services/ast_queries/acsl_extension.mli
index a4b99bcf14208e8356fbed6097670c7f890a3edb..df0e7f6d07d88fe124247fbaeb2be5f62bb8994a 100644
--- a/src/kernel_services/ast_queries/acsl_extension.mli
+++ b/src/kernel_services/ast_queries/acsl_extension.mli
@@ -80,7 +80,7 @@ type extension_printer =
Here is a basic example:
[
let count = ref 0
- let foo_typer ~typing_context ~loc = function
+ let foo_typer typing_context loc = function
| p :: [] ->
Ext_preds
[ (typing_context.type_predicate
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 5bdb0939b7a617338d8b221ca8cffe24fad7c7a3..df4e0e12389593b8b0423c1bf6d46e91dd878bc5 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1223,7 +1223,7 @@ val partitionAttributes: default:attributeClass ->
attribute list (* AttrType *)
(** Add an attribute. Maintains the attributes in sorted order of the second
- argument *)
+ argument. The attribute is not added if it is already there. *)
val addAttribute: attribute -> attributes -> attributes
(** Add a list of attributes. Maintains the attributes in sorted order. The
diff --git a/src/plugins/wp/Factory.ml b/src/plugins/wp/Factory.ml
index cdb4593efb4ac2c9aa6813f5dab05f961a3730df..668610d8cfccda532eb16e76f332df7ef6875d5a 100644
--- a/src/plugins/wp/Factory.ml
+++ b/src/plugins/wp/Factory.ml
@@ -104,6 +104,9 @@ let describe s =
(* --- Variable Proxy --- *)
(* -------------------------------------------------------------------------- *)
+let validity x =
+ if RefUsage.is_nullable x then MemoryContext.Nullable else Valid
+
module type Proxy = sig
val datatype : string
val param : Cil_types.varinfo -> MemoryContext.param
@@ -124,7 +127,7 @@ struct
let module S = Datatype.String.Set in
let open MemoryContext in
if S.mem x.vname (get_addr ()) then ByAddr else
- if S.mem x.vname (get_ctxt ()) then InContext else
+ if S.mem x.vname (get_ctxt ()) then InContext (validity x) else
if S.mem x.vname (get_refs ()) then ByRef else
if S.mem x.vname (get_vars ()) then ByValue else
V.param x
@@ -182,16 +185,19 @@ let refusage_param ~byref ~context x =
| RefUsage.NoAccess -> MemoryContext.NotUsed
| RefUsage.ByAddr -> MemoryContext.ByAddr
| RefUsage.ByValue ->
- if context && is_formal_ptr x then MemoryContext.InContext
+ if context && is_formal_ptr x then MemoryContext.InContext (validity x)
else if is_ptr x && not (is_fun_ptr x) then MemoryContext.ByShift
else MemoryContext.ByValue
| RefUsage.ByRef ->
if byref
- then MemoryContext.ByRef
+ then
+ if RefUsage.is_nullable x
+ then MemoryContext.InContext Nullable
+ else MemoryContext.ByRef
else MemoryContext.ByValue
| RefUsage.ByArray ->
if context && is_formal_ptr x
- then MemoryContext.InArray
+ then MemoryContext.InArray (validity x)
else MemoryContext.ByShift
let refusage_iter ?kf ~init f = RefUsage.iter ?kf ~init (fun x _usage -> f x)
diff --git a/src/plugins/wp/Generator.ml b/src/plugins/wp/Generator.ml
index 4b5d51804c65821460d0d5ee8397f6c39468e130..425a2b4ca9bab6bf6e494abd77b7d5321d3c1a69 100644
--- a/src/plugins/wp/Generator.ml
+++ b/src/plugins/wp/Generator.ml
@@ -50,7 +50,19 @@ let user_setup () : Factory.setup =
cint = Cint.Natural ;
cfloat = Cfloat.Real ;
}
- | spec -> Factory.parse spec
+ | spec ->
+ let setup = Factory.parse spec in
+ let mref = match setup.mvar with
+ | Caveat -> "caveat" | Ref -> "ref" | Raw | Var -> "" in
+ if mref <> ""
+ && RefUsage.has_nullable ()
+ && not (Wp_parameters.RTE.is_set ())
+ then
+ Wp_parameters.warning ~current:false ~once:true
+ "In %s model with nullable arguments, \
+ -wp-(no)-rte shall be explicitly positioned."
+ mref ;
+ setup
end
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index e373bd541e29e52019abce940537424ab03ff533..45cc5514fc77bf7cf02ef169a228cbabfc8f9311 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -104,7 +104,7 @@ struct
match V.param x with
| ByRef ->
"ra_" ^ LogicUsage.basename x
- | NotUsed | ByValue | ByShift | ByAddr | InContext | InArray ->
+ | NotUsed | ByValue | ByShift | ByAddr | InContext _ | InArray _ ->
"ta_" ^ LogicUsage.basename x
let is_framed = is_framed_var
end
@@ -517,8 +517,8 @@ struct
type mem =
| CVAL (* By-Value variable *)
| CREF (* By-Ref variable *)
- | CTXT (* In-context pointer *)
- | CARR (* In-context array *)
+ | CTXT of MemoryContext.validity (* In-context pointer *)
+ | CARR of MemoryContext.validity (* In-context array *)
| HEAP (* In-heap variable *)
type loc =
@@ -563,8 +563,8 @@ struct
let vtype m x =
match m with
| CVAL | HEAP -> x.vtype
- | CTXT | CREF -> Cil.typeOf_pointed x.vtype
- | CARR -> Ast_info.array_type (Cil.typeOf_pointed x.vtype)
+ | CTXT _ | CREF -> Cil.typeOf_pointed x.vtype
+ | CARR _ -> Ast_info.array_type (Cil.typeOf_pointed x.vtype)
let vobject m x = Ctypes.object_of (vtype m x)
@@ -593,15 +593,15 @@ struct
let pp_mem fmt = function
| CVAL -> Format.pp_print_string fmt "var"
| CREF -> Format.pp_print_string fmt "ref"
- | CTXT -> Format.pp_print_string fmt "ptr"
- | CARR -> Format.pp_print_string fmt "arr"
+ | CTXT _ -> Format.pp_print_string fmt "ptr"
+ | CARR _ -> Format.pp_print_string fmt "arr"
| HEAP -> Format.pp_print_string fmt "mem"
(* re-uses strings that are used into the description of -wp-xxx-vars *)
let pp_var_model fmt = function
| ByValue | ByShift | NotUsed -> Format.pp_print_string fmt "non-aliased" (* cf. -wp-unalias-vars *)
| ByRef -> Format.pp_print_string fmt "by reference" (* cf. -wp-ref-vars *)
- | InContext | InArray -> Format.pp_print_string fmt "in an isolated context" (* cf. -wp-context-vars *)
+ | InContext _ | InArray _ -> Format.pp_print_string fmt "in an isolated context" (* cf. -wp-context-vars *)
| ByAddr -> Format.pp_print_string fmt "aliased" (* cf. -wp-alias-vars *)
let pretty fmt = function
@@ -632,7 +632,36 @@ struct
let cvar x = match V.param x with
| NotUsed | ByValue | ByShift -> Val(CVAL,x,[])
| ByAddr -> Val(HEAP,x,[])
- | InContext | InArray | ByRef -> Ref x
+ | InContext _ | InArray _ | ByRef -> Ref x
+
+ (* -------------------------------------------------------------------------- *)
+ (* --- Nullable locations --- *)
+ (* -------------------------------------------------------------------------- *)
+
+ module Nullable = WpContext.Generator(Varinfo)
+ (struct
+ let name = "MemVar.Nullable"
+ type key = varinfo
+ type data = lfun
+
+ let compile v =
+ let result = t_addr () in
+ let lfun = Lang.generated_f ~result "pointer_%s" v.vname in
+ let cluster =
+ Definitions.cluster ~id:"Globals" ~title:"Context pointers" ()
+ in
+ Definitions.define_symbol {
+ d_lfun = lfun ;
+ d_types = 0 ;
+ d_params = [] ;
+ d_definition = Definitions.Logic result ;
+ d_cluster = cluster
+ } ;
+ lfun
+ end)
+
+ let nullable_address v =
+ Lang.F.e_fun (Nullable.get v) []
(* -------------------------------------------------------------------------- *)
(* --- Lifting --- *)
@@ -645,7 +674,11 @@ struct
let mseq_of_seq seq = { pre = seq.pre.mem ; post = seq.post.mem }
let mloc_of_path m x ofs =
- List.fold_left moffset (M.cvar (vbase m x)) ofs
+ let l = match m with
+ | CTXT Nullable | CARR Nullable -> M.pointer_loc @@ nullable_address x
+ | _ -> M.cvar (vbase m x)
+ in
+ List.fold_left moffset l ofs
let mloc_of_loc = function
| Loc l -> l
@@ -731,9 +764,9 @@ struct
let load sigma obj = function
| Ref x ->
begin match V.param x with
- | ByRef -> Sigs.Loc(Val(CREF,x,[]))
- | InContext -> Sigs.Loc(Val(CTXT,x,[]))
- | InArray -> Sigs.Loc(Val(CARR,x,[]))
+ | ByRef -> Sigs.Loc(Val(CREF,x,[]))
+ | InContext n -> Sigs.Loc(Val(CTXT n,x,[]))
+ | InArray n -> Sigs.Loc(Val(CARR n,x,[]))
| NotUsed | ByAddr | ByValue | ByShift -> assert false
end
| Val((CREF|CVAL),x,ofs) ->
@@ -742,7 +775,7 @@ struct
Cvalues.map_value
(fun l -> Loc l)
(M.load sigma.mem obj l)
- | Val((CTXT|CARR|HEAP) as m,x,ofs) ->
+ | Val((CTXT _|CARR _|HEAP) as m,x,ofs) ->
Cvalues.map_value
(fun l -> Loc l)
(M.load sigma.mem obj (mloc_of_path m x ofs))
@@ -773,7 +806,7 @@ struct
| Val((CREF|CVAL),x,ofs) ->
let init = Cvalues.initialized_obj obj in
(memvar_stored seq obj l v) :: (memvar_set_init seq x ofs init)
- | Val((CTXT|CARR|HEAP) as m,x,ofs) ->
+ | Val((CTXT _|CARR _|HEAP) as m,x,ofs) ->
M.stored (mseq_of_seq seq) obj (mloc_of_path m x ofs) v
| Loc l ->
M.stored (mseq_of_seq seq) obj l v
@@ -790,6 +823,8 @@ struct
let is_null = function
| Loc l -> M.is_null l
+ | Val ((CTXT Nullable|CARR Nullable)as m,x,ofs) ->
+ M.is_null (mloc_of_path m x ofs)
| Ref _ | Val _ -> F.p_false
let rec offset = function
@@ -831,7 +866,7 @@ struct
exception ShiftMismatch
let is_heap_allocated = function
- | CREF | CVAL -> false | HEAP | CTXT | CARR -> true
+ | CREF | CVAL -> false | HEAP | CTXT _ | CARR _ -> true
let shift_mismatch l =
Wp_parameters.fatal "Invalid shift : %a" pretty l
@@ -939,7 +974,9 @@ struct
else
match mem with
| CVAL | HEAP -> p_bool (ALLOC.value sigma.alloc x)
- | CREF | CTXT | CARR -> p_true
+ | CREF | CTXT Valid | CARR Valid -> p_true
+ | CTXT Nullable | CARR Nullable ->
+ p_not @@ M.is_null (mloc_of_path mem x [])
(* segment *)
@@ -1181,7 +1218,7 @@ struct
let is_mvar_alloc x =
match V.param x with
- | ByRef | InContext | InArray | NotUsed -> false
+ | ByRef | InContext _ | InArray _ | NotUsed -> false
| ByValue | ByShift | ByAddr -> true
let alloc sigma xs =
@@ -1221,6 +1258,17 @@ struct
in
List.map uninitialized xs
+ let is_nullable m v =
+ let addr = nullable_address v in
+ p_or
+ (M.is_null @@ M.pointer_loc addr)
+ (p_equal (M.pointer_val @@ M.cvar (vbase m v)) addr)
+
+ let nullable_scope v =
+ match V.param v with
+ | InContext Nullable -> Some (is_nullable (CTXT Nullable) v)
+ | InArray Nullable -> Some (is_nullable (CARR Nullable) v)
+ | _ -> None
let scope seq scope xs =
let xm = List.filter is_mem xs in
@@ -1228,7 +1276,8 @@ struct
let hmem = M.scope smem scope xm in
let hvars = scope_vars seq scope xs in
let hinit = scope_init seq scope xs in
- hvars @ hinit @ hmem
+ let hcontext = List.filter_map nullable_scope xs in
+ hvars @ hinit @ hmem @ hcontext
let global sigma p = M.global sigma.mem p
@@ -1365,7 +1414,7 @@ struct
| Val((CVAL|CREF),_,_) as vloc ->
let v = Lang.freshvar ~basename:"v" (Lang.tau_of_object obj) in
memvar_assigned seq obj vloc (e_var v)
- | Val((HEAP|CTXT|CARR) as m,x,ofs) ->
+ | Val((HEAP|CTXT _|CARR _) as m,x,ofs) ->
M.assigned (mseq_of_seq seq) obj (Sloc (mloc_of_path m x ofs))
| Loc l ->
M.assigned (mseq_of_seq seq) obj (Sloc l)
@@ -1387,7 +1436,7 @@ struct
in
let obj = get_obj (Ctypes.object_of x.vtype) ofs in
memvar_assigned seq obj vloc (e_var v)
- | Val((HEAP|CTXT|CARR) as m,x,ofs) ->
+ | Val((HEAP|CTXT _|CARR _) as m,x,ofs) ->
let l = mloc_of_path m x ofs in
M.assigned (mseq_of_seq seq) obj (Sarray(l,elt,n))
| Loc l ->
@@ -1398,7 +1447,7 @@ struct
| Ref x -> noref ~op:"assigns to" x
| Loc l ->
M.assigned (mseq_of_seq seq) obj (Srange(l,elt,a,b))
- | Val((HEAP|CTXT|CARR) as m,x,ofs) ->
+ | Val((HEAP|CTXT _|CARR _) as m,x,ofs) ->
M.assigned (mseq_of_seq seq) obj (Srange(mloc_of_path m x ofs,elt,a,b))
| Val((CVAL|CREF) as m,x,ofs) ->
let k = Lang.freshvar ~basename:"k" Qed.Logic.Int in
@@ -1412,7 +1461,7 @@ struct
| Ref x -> noref ~op:"assigns to" x
| Loc l ->
M.assigned (mseq_of_seq seq) obj (Sdescr(xs,l,p))
- | Val((HEAP|CTXT|CARR) as m,x,ofs) ->
+ | Val((HEAP|CTXT _|CARR _) as m,x,ofs) ->
M.assigned (mseq_of_seq seq) obj (Sdescr(xs,mloc_of_path m x ofs,p))
| Val((CVAL|CREF) as m,x,ofs) ->
(* (monotonic_initialized_genset seq xs m x ofs p) @ *)
@@ -1481,10 +1530,16 @@ struct
| Rrange(Val((CVAL|CREF),x,ofs),obj,a,b) ->
Fseg(x,range ofs obj a b)
- (* in M: *)
- | Rloc(obj,Val((CTXT|CARR|HEAP) as m,x,ofs)) ->
+ (* Nullable: force M without symbolic access *)
+ | Rloc(obj,Val((CTXT Nullable|CARR Nullable) as m,x,ofs)) ->
+ Lseg(Rloc(obj, mloc_of_path m x ofs))
+ | Rrange(Val((CTXT Nullable|CARR Nullable) as m,x,ofs),obj,a,b) ->
+ Lseg(Rrange(mloc_of_path m x ofs, obj, a, b))
+
+ (* Otherwise: use M with symbolic access *)
+ | Rloc(obj,Val((CTXT Valid|CARR Valid|HEAP) as m,x,ofs)) ->
Mseg(Rloc(obj,mloc_of_path m x ofs),x,delta obj x ofs)
- | Rrange(Val((CTXT|CARR|HEAP) as m,x,ofs),obj,a,b) ->
+ | Rrange(Val((CTXT Valid|CARR Valid|HEAP) as m,x,ofs),obj,a,b) ->
Mseg(Rrange(mloc_of_path m x ofs,obj,a,b),x,range ofs obj a b)
(* -------------------------------------------------------------------------- *)
@@ -1559,7 +1614,7 @@ struct
else []
in
Heap.Set.of_list ((Var x) :: init)
- | Loc _ | Val((CTXT|CARR|HEAP),_,_) ->
+ | Loc _ | Val((CTXT _|CARR _|HEAP),_,_) ->
M.Heap.Set.fold
(fun m s -> Heap.Set.add (Mem m) s)
(M.domain obj (mloc_of_loc l)) Heap.Set.empty
diff --git a/src/plugins/wp/MemoryContext.ml b/src/plugins/wp/MemoryContext.ml
index e337a19633147beae582c55553e6e252bbd5da89..1b1066105cb0354d9d327f72617a2a2d9b911fbf 100644
--- a/src/plugins/wp/MemoryContext.ml
+++ b/src/plugins/wp/MemoryContext.ml
@@ -24,16 +24,23 @@
(* --- Variable Partitionning --- *)
(* -------------------------------------------------------------------------- *)
-type param = NotUsed | ByAddr | ByValue | ByShift | ByRef | InContext | InArray
+type validity = Valid | Nullable
+type param =
+ | NotUsed | ByAddr | ByValue | ByShift | ByRef
+ | InContext of validity | InArray of validity
+
+let pp_nullable fmt = function
+ | Valid -> ()
+ | Nullable -> Format.pp_print_string fmt " (nullable)"
let pp_param fmt = function
| NotUsed -> Format.pp_print_string fmt "not used"
| ByAddr -> Format.pp_print_string fmt "in heap"
| ByValue -> Format.pp_print_string fmt "by value"
| ByShift -> Format.pp_print_string fmt "by value with shift"
- | ByRef -> Format.pp_print_string fmt "by ref."
- | InContext -> Format.pp_print_string fmt "in context"
- | InArray -> Format.pp_print_string fmt "in array"
+ | ByRef -> Format.pp_print_string fmt "by ref"
+ | InContext n -> Format.fprintf fmt "in context%a" pp_nullable n
+ | InArray n -> Format.fprintf fmt "in array%a" pp_nullable n
(* -------------------------------------------------------------------------- *)
(* --- Separation Hypotheses --- *)
@@ -47,10 +54,11 @@ type zone =
| Arr of varinfo (* p+(..) - the cell and its neighbors pointed by p *)
type partition = {
- globals : zone list ; (* [ &G , G[...], ... ] *)
- to_heap : zone list ; (* [ p, ... ] *)
- context : zone list ; (* [ p+(..), ... ] *)
- by_addr : zone list ; (* [ &(x + ..), ... ] *)
+ globals : zone list ; (* [ &G , G[...], ... ] *)
+ to_heap : zone list ; (* [ p, ... ] *)
+ context : zone list ; (* [ p+(..), ... ] *)
+ nullable : zone list ; (* [ p+(..), ... ] but can be NULL *)
+ by_addr : zone list ; (* [ &(x + ..), ... ] *)
}
(* -------------------------------------------------------------------------- *)
@@ -60,6 +68,7 @@ type partition = {
let empty = {
globals = [] ;
context = [] ;
+ nullable = [] ;
to_heap = [] ;
by_addr = [] ;
}
@@ -68,12 +77,21 @@ let set x p w =
match p with
| NotUsed -> w
| ByAddr -> { w with by_addr = Var x :: w.by_addr }
- | ByRef | InContext ->
+ | ByRef ->
if Cil.isFunctionType x.vtype then w else
{ w with context = Ptr x :: w.context }
- | InArray ->
+ | InContext v ->
+ if Cil.isFunctionType x.vtype then w else
+ begin match v with
+ | Nullable -> { w with nullable = Ptr x :: w.nullable }
+ | Valid -> { w with context = Ptr x :: w.context }
+ end
+ | InArray v ->
if Cil.isFunctionType x.vtype then w else
- { w with context = Arr x :: w.context }
+ begin match v with
+ | Nullable -> { w with nullable = Arr x :: w.nullable }
+ | Valid -> { w with context = Arr x :: w.context }
+ end
| ByValue | ByShift ->
if x.vghost then w else
if Cil.isFunctionType x.vtype then w else
@@ -187,9 +205,25 @@ let valid_region loc r =
let t = region_to_term loc r in
pvalid ~loc (here_label, t)
-let simplify ps =
- List.sort_uniq Logic_utils.compare_predicate
- (List.filter (fun p -> not(Logic_utils.is_trivially_true p)) ps)
+let valid_or_null_region loc r =
+ let t = region_to_term loc r in
+ let null = term ~loc Tnull t.term_type in
+ por (valid_region loc r, prel ~loc (Req, t, null))
+
+let rec rank p = match p.pred_content with
+ | Pvalid _ -> 1
+ | Pseparated _ -> 2
+ | Pimplies(_,p) -> rank p
+ | Por(p,q) | Pand(p,q) -> max (rank p) (rank q)
+ | _ -> 0
+
+let compare p q =
+ let r = rank p - rank q in
+ if r <> 0 then r else Logic_utils.compare_predicate p q
+
+let normalize ps =
+ List.sort_uniq compare @@
+ List.filter (fun p -> not(Logic_utils.is_trivially_true p)) ps
let ptrset { term_type = t } =
let open Logic_typing in
@@ -221,6 +255,9 @@ let global_zones partition =
let context_zones partition =
List.map (fun z -> [z]) partition.context
+let nullable_zones partition =
+ List.map (fun z -> [z]) partition.nullable
+
let heaps partition = welltyped partition.to_heap
let addr_of_vars partition = welltyped partition.by_addr
@@ -229,20 +266,42 @@ let addr_of_vars partition = welltyped partition.by_addr
(* -------------------------------------------------------------------------- *)
(* Memory regions shall be separated with each others *)
-let main_separation loc globals context heaps =
- match heaps, context with
- | [], [] ->
- (* In this case, separation is completely trivial *)
- [ ptrue ]
- | [], context ->
- let zones = globals @ context in
- [ separated_list ~loc (List.map (region_to_term loc) zones) ]
- | heaps, context ->
- let for_typed_heap h =
- let zones = h :: globals @ context in
- separated_list ~loc (List.map (region_to_term loc) zones)
+let main_separation loc globals context nullable heaps =
+ if context = [] && nullable = [] && heaps = [] then []
+ else
+ let l_zones = match heaps with
+ | [] -> [globals @ context]
+ | heaps -> List.map (fun h -> h :: (globals @ context)) heaps
+ in
+ let regions_to_terms = List.map (region_to_term loc) in
+ let guard_nullable tn sep =
+ pimplies ~loc (prel ~loc (Rneq, tn, term ~loc Tnull tn.term_type), sep)
+ in
+ let acc_with_nullable tn zones =
+ List.cons @@
+ guard_nullable tn (separated_list ~loc (tn :: regions_to_terms zones))
+ in
+ let no_nullable zones = separated_list ~loc @@ regions_to_terms zones in
+ let nullable_inter nullable =
+ let separated_nullable (p, q) =
+ guard_nullable p @@ guard_nullable q @@ pseparated ~loc [ p ; q ]
in
- List.map for_typed_heap heaps
+ let rec collect_pairs = function
+ (* trivial cases *)
+ | [] -> [] | [_] -> []
+ | p :: l ->
+ let acc_sep q = List.cons @@ separated_nullable (p, q) in
+ List.fold_right acc_sep l @@ collect_pairs l
+ in
+ collect_pairs nullable
+ in
+ match nullable with
+ | [] -> List.map no_nullable l_zones
+ | nullable ->
+ let t_nullable = regions_to_terms nullable in
+ let sep_nullable = nullable_inter t_nullable in
+ let fold n = List.fold_right (acc_with_nullable n) l_zones in
+ List.fold_right fold t_nullable sep_nullable
(* Filter assigns *)
let assigned_locations kf filter =
@@ -301,12 +360,15 @@ let assigned_separation kf loc globals =
(* Computes conditions from partition *)
let clauses_of_partition kf loc p =
let globals = global_zones p in
- let main_sep = main_separation loc globals (context_zones p) (heaps p) in
+ let main_sep =
+ main_separation loc globals (context_zones p) (nullable_zones p) (heaps p)
+ in
let assigns_sep_req, assigns_sep_ens = assigned_separation kf loc globals in
- let context_validity = List.map (valid_region loc) (context_zones p) in
- let reqs = main_sep @ assigns_sep_req @ context_validity in
- let reqs = simplify reqs in
- let ens = simplify assigns_sep_ens in
+ let context_valid = List.map (valid_region loc) (context_zones p) in
+ let nullable_valid = List.map (valid_or_null_region loc) (nullable_zones p) in
+ let reqs = main_sep @ assigns_sep_req @ context_valid @ nullable_valid in
+ let reqs = normalize reqs in
+ let ens = normalize assigns_sep_ens in
reqs, ens
(* Computes conditions from return *)
@@ -335,7 +397,7 @@ let out_pointers_separation kf loc p =
let globals = global_zones p in
List.map (fun t -> term_separated_from_regions loc t globals) asgnd_ptrs
in
- simplify (formals_separation @ globals_separation)
+ normalize (formals_separation @ globals_separation)
(* Computes all conditions from behavior *)
let compute_behavior kf name hypotheses_computer =
diff --git a/src/plugins/wp/MemoryContext.mli b/src/plugins/wp/MemoryContext.mli
index c0698fa9ea1d38761283b3d675fb82ca29cc1375..9cf4ea56bfc5f17b74a9b9b6d94ba2bbb878ac8e 100644
--- a/src/plugins/wp/MemoryContext.mli
+++ b/src/plugins/wp/MemoryContext.mli
@@ -22,7 +22,9 @@
open Cil_types
-type param = NotUsed | ByAddr | ByValue | ByShift | ByRef | InContext | InArray
+type validity = Valid | Nullable
+type param = NotUsed | ByAddr | ByValue | ByShift | ByRef
+ | InContext of validity | InArray of validity
val pp_param: Format.formatter -> param -> unit
diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index 4413187be9efce693afa69a5795f59bdbcb68288..7e485e323bef5d461e2985706f00e47022059611 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/src/plugins/wp/RefUsage.ml
@@ -827,6 +827,61 @@ module S = State_builder.Option_ref(D)
let usage () = S.memo compute_usage
let is_computed () = S.is_computed ()
+(* ---------------------------------------------------------------------- *)
+(* --- Nullable variables --- *)
+(* ---------------------------------------------------------------------- *)
+
+module Nullable =
+struct
+ let attribute_name = "wp_nullable"
+
+ let is_nullable vi =
+ vi.vformal && Cil.hasAttribute attribute_name vi.vattr
+
+ let make_nullable vi =
+ vi.vattr <- Cil.addAttribute (AttrAnnot attribute_name) vi.vattr
+
+ module Nullable_extension =
+ struct
+ let type_term typing_context loc e =
+ match e.Logic_ptree.lexpr_node with
+ | Logic_ptree.PLvar s ->
+ let lv = typing_context.Logic_typing.find_var s in
+ begin match lv.lv_origin with
+ | Some vi when Cil.isPointerType vi.vtype && vi.vformal ->
+ make_nullable vi ;
+ Logic_const.tvar ~loc lv
+ | _ ->
+ typing_context.error loc "No pointer: %s" s
+ end
+ | _ ->
+ typing_context.error loc "Illegal expression %a"
+ Logic_print.print_lexpr e
+
+ let typer typing_context loc l =
+ Ext_terms (List.map (type_term typing_context loc) l)
+ end
+
+ let () =
+ Acsl_extension.register_behavior
+ "wp_nullable_args" Nullable_extension.typer false
+
+ module HasNullable =
+ State_builder.Option_ref(Datatype.Bool)
+ (struct
+ let name = "Wp.RefUsage.HasNullable"
+ let dependencies = [Ast.self]
+ end)
+
+ let compute_nullable () =
+ let module F = Globals.Functions in
+ F.fold (fun f b ->
+ b || List.fold_left (fun b v -> b || is_nullable v) b (F.get_params f)
+ ) false
+
+ let has_nullable () = HasNullable.memo compute_nullable
+end
+
(* ---------------------------------------------------------------------- *)
(* --- API --- *)
(* ---------------------------------------------------------------------- *)
@@ -854,6 +909,9 @@ let get ?kf ?(init=false) vi =
let compute () = ignore (usage ())
+let is_nullable = Nullable.is_nullable
+let has_nullable = Nullable.has_nullable
+
let print x m fmt = Access.pretty x fmt m
let dump () =
diff --git a/src/plugins/wp/RefUsage.mli b/src/plugins/wp/RefUsage.mli
index 988103efebfd6817de6320945e69f06d9194cc12..2290ad05f69084646ce2514260e4cb88db7ec965 100644
--- a/src/plugins/wp/RefUsage.mli
+++ b/src/plugins/wp/RefUsage.mli
@@ -38,6 +38,14 @@ val get : ?kf:kernel_function -> ?init:bool -> varinfo -> access
val iter: ?kf:kernel_function -> ?init:bool -> (varinfo -> access -> unit) -> unit
+val is_nullable : varinfo -> bool
+(** [is_nullable vi] returns true
+ iff [vi] is a formal and has an attribute 'nullable' *)
+
+val has_nullable : unit -> bool
+(** [has_nullable ()] return true
+ iff there exists a variable that satisfies [is_nullable] *)
+
val print : varinfo -> access -> Format.formatter -> unit
val dump : unit -> unit
val compute : unit -> unit
diff --git a/src/plugins/wp/doc/manual/nullable.c b/src/plugins/wp/doc/manual/nullable.c
new file mode 100644
index 0000000000000000000000000000000000000000..9b403ffe91cb9148bcff3b461de90cec89c09cb1
--- /dev/null
+++ b/src/plugins/wp/doc/manual/nullable.c
@@ -0,0 +1,9 @@
+void foo(int* p /*@ wp_nullable */, int* q /*@ wp_nullable */){
+
+}
+
+// or equivalently:
+//@ wp_nullable_args p, q ;
+void foo(int* p, int* q){
+
+}
diff --git a/src/plugins/wp/doc/manual/wp_caveat.tex b/src/plugins/wp/doc/manual/wp_caveat.tex
index 6e7afa77c066bb52273da98252d093d08b6980f3..4a49fd03c2be8622dc6700db76484395853348bf 100644
--- a/src/plugins/wp/doc/manual/wp_caveat.tex
+++ b/src/plugins/wp/doc/manual/wp_caveat.tex
@@ -21,7 +21,14 @@ global ones).
Additionally, the \texttt{Caveat} memory model of \textsf{Frama-C}
performs a local allocation of formal parameters with pointer
-types that cannot be treated as \textit{reference parameters}.
+types that cannot be treated as \textit{reference parameters}.
+Note that it means that the pointer is considered valid. If one needs
+to accept \texttt{NULL} for this pointer, a \texttt{wp\_nullable} ghost
+annotation or the clause \texttt{wp\_nullage\_args} can be used to bring
+this information to WP:
+
+\listingname{nullable.c}
+\cinput{nullable.c}
This makes explicit the separation hypothesis of memory regions
pointed by formals in the \textsf{Caveat} tool. The major benefit of
@@ -29,7 +36,7 @@ the \textsf{WP} version is that aliases are taken into account by the
\texttt{Typed} memory model, hence, there are no more suspicious
\textit{aliasing} warnings.
-\paragraph{Warning:} using the \texttt{Caveat} memory model,
+\paragraph{Warning:} using the \texttt{Caveat} memory model,
the user \emph{must} check by manual code review that no aliases are
introduced \emph{via} pointers passed to formal parameters at call sites.
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_1828.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1828.1.res.oracle
index 1f183b1d30a1530c5c404f9a38f7ed12fec5d9ff..9c383998a35a6db6956fd0e37c775bc07059fa59 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_1828.1.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_1828.1.res.oracle
@@ -48,8 +48,8 @@ Prove: global(L_two_24) != one_0.
Memory model hypotheses for function 'global_frame':
/*@
behavior wp_typed_ref:
- requires \separated(zero, one);
requires \valid(one);
requires \valid(zero);
+ requires \separated(zero, one);
*/
void global_frame(int *one, int arg);
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle
index 43305903b452ccabf5e96e46b022d2bfe3c1ffce..e9a2a01d9a210f37acaaa53be63d723f7baf2541 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle
@@ -21,8 +21,8 @@
Memory model hypotheses for function 'global_frame':
/*@
behavior wp_typed_ref:
- requires \separated(zero, one);
requires \valid(one);
requires \valid(zero);
+ requires \separated(zero, one);
*/
void global_frame(int *one, int arg);
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle
index 56bb306558b56d74141556fc1b026d735ef9cfe9..5508bc1831913be6943b2cc4f680f7b4d23fcbd7 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle
@@ -56,8 +56,8 @@
Memory model hypotheses for function 'equal_elements':
/*@
behavior wp_typed_ref:
- requires \separated(v1, v2, a + (..));
requires \valid(v1);
requires \valid(v2);
+ requires \separated(v1, v2, a + (..));
*/
void equal_elements(int *a, int *v1, int *v2);
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle
index 53078f53cb88bbc0681c1ce463aef6b08bf1de0e..87430ad4b3c1a897ffe57842d2ad079a105b7649 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle
@@ -57,8 +57,8 @@
Memory model hypotheses for function 'equal_elements':
/*@
behavior wp_typed_ref:
- requires \separated(v1, v2, a + (..));
requires \valid(v1);
requires \valid(v2);
+ requires \separated(v1, v2, a + (..));
*/
void equal_elements(int *a, int *v1, int *v2);
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
index 3903ba3a3a32a691f6e6e2bce73a83b71362f378..174cfa7521504fd213dc75ca4404ea89dddb4faa 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
@@ -48,9 +48,9 @@
Memory model hypotheses for function 'equal_elements':
/*@
behavior wp_typed_ref:
- requires \separated(v1, v2, a + (..));
requires \valid(v1);
requires \valid(v2);
+ requires \separated(v1, v2, a + (..));
*/
void equal_elements(int *a, int *v1, int *v2);
[wp] Running WP plugin...
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
index 1dfeafb91d559189ced438c76169d59f9f36c303..cfbc31146758fcdad382bd59ca15be2c53d18327 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
@@ -49,9 +49,9 @@
Memory model hypotheses for function 'equal_elements':
/*@
behavior wp_typed_ref:
- requires \separated(v1, v2, a + (..));
requires \valid(v1);
requires \valid(v2);
+ requires \separated(v1, v2, a + (..));
*/
void equal_elements(int *a, int *v1, int *v2);
[wp] Running WP plugin...
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var.res.oracle
index 03056370c4a6760b6e4e1e2f3662a4c7bf5753a0..30d6f05c1f7c75c51330593d503e43a92237da15 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/dispatch_var.res.oracle
@@ -515,10 +515,10 @@ Prove: true.
Memory model hypotheses for function 'ref_ctr_nr':
/*@
behavior wp_typed_ref:
- requires \separated(ref, ref1, ref2);
requires \valid(ref);
requires \valid(ref1);
requires \valid(ref2);
+ requires \separated(ref, ref1, ref2);
*/
int ref_ctr_nr(int *ref, int *ref1, int *ref2);
[wp] tests/wp_hoare/dispatch_var.i:158: Warning:
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/memory_hypotheses_checking.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/memory_hypotheses_checking.res.oracle
index 380a7e0cc8ace27dc70721782cf090990ab2631b..142b8eba2461dd41529943de1b117ebcb619649d 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/memory_hypotheses_checking.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/memory_hypotheses_checking.res.oracle
@@ -142,13 +142,13 @@ Prove: true.
Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 58) in 'assigns_ptr'' in 'call_assigns_ptr_bad' at call 'assigns_ptr' (file tests/wp_hoare/memory_hypotheses_checking.i, line 70)
:
-Prove: false.
+Prove: true.
------------------------------------------------------------
Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 58) in 'assigns_ptr'' in 'call_assigns_ptr_bad' at call 'assigns_ptr' (file tests/wp_hoare/memory_hypotheses_checking.i, line 70)
:
-Prove: true.
+Prove: false.
------------------------------------------------------------
------------------------------------------------------------
@@ -194,14 +194,14 @@ Prove: true.
Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 39) in 'gptr_sep'' in 'call_gptr_sep_bad' at call 'gptr_sep' (file tests/wp_hoare/memory_hypotheses_checking.i, line 53)
:
-Prove: false.
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: valid_rw(Malloc_0, global(G_g_20), 1).
------------------------------------------------------------
Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 39) in 'gptr_sep'' in 'call_gptr_sep_bad' at call 'gptr_sep' (file tests/wp_hoare/memory_hypotheses_checking.i, line 53)
:
-Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: valid_rw(Malloc_0, global(G_g_20), 1).
+Prove: false.
------------------------------------------------------------
------------------------------------------------------------
@@ -220,14 +220,14 @@ Prove: true.
Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 39) in 'gptr_sep'' in 'call_gptr_sep_ok' at call 'gptr_sep' (file tests/wp_hoare/memory_hypotheses_checking.i, line 47)
:
-Prove: true.
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: valid_rw(Malloc_0[L_l_46 <- 1], global(L_l_46), 1).
------------------------------------------------------------
Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 39) in 'gptr_sep'' in 'call_gptr_sep_ok' at call 'gptr_sep' (file tests/wp_hoare/memory_hypotheses_checking.i, line 47)
:
-Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: valid_rw(Malloc_0[L_l_46 <- 1], global(L_l_46), 1).
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
@@ -246,13 +246,13 @@ Prove: true.
Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 12) in 'sep'' in 'call_sep_bad_sep' at call 'sep' (file tests/wp_hoare/memory_hypotheses_checking.i, line 24)
:
-Prove: false.
+Prove: true.
------------------------------------------------------------
Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 12) in 'sep'' in 'call_sep_bad_sep' at call 'sep' (file tests/wp_hoare/memory_hypotheses_checking.i, line 24)
:
-Prove: true.
+Prove: false.
------------------------------------------------------------
------------------------------------------------------------
@@ -283,14 +283,14 @@ Prove: true.
Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 12) in 'sep'' in 'call_sep_bad_valid' at call 'sep' (file tests/wp_hoare/memory_hypotheses_checking.i, line 34)
:
-Prove: true.
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: valid_rw(Malloc_0[L_l_37 <- 0], global(L_l_37), 1).
------------------------------------------------------------
Goal Instance of 'Pre-condition for 'wp_typed_ref' (file tests/wp_hoare/memory_hypotheses_checking.i, line 12) in 'sep'' in 'call_sep_bad_valid' at call 'sep' (file tests/wp_hoare/memory_hypotheses_checking.i, line 34)
:
-Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: valid_rw(Malloc_0[L_l_37 <- 0], global(L_l_37), 1).
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
@@ -341,8 +341,8 @@ int g;
/*@ assigns \nothing;
behavior wp_typed_ref:
- requires \separated(p_0, &g);
requires \valid(p_0);
+ requires \separated(p_0, &g);
*/
int sep(int *p_0)
{
@@ -382,8 +382,8 @@ int *p;
/*@ assigns \nothing;
behavior wp_typed_ref:
- requires \separated(p, &g);
requires \valid(p);
+ requires \separated(p, &g);
*/
int gptr_sep(void)
{
@@ -414,8 +414,8 @@ void call_gptr_sep_bad(void)
/*@ assigns *p_0;
behavior wp_typed_ref:
- requires \separated(p_0, &g);
requires \valid(p_0);
+ requires \separated(p_0, &g);
*/
void assigns_ptr(int *p_0)
{
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle
index bf4453996e1f0c3f7c0390b232a6c5e86e4608d0..3d3946ce97f51a2657303d810fb22191ebf65aec 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference.res.oracle
@@ -150,9 +150,9 @@ Prove: true.
Memory model hypotheses for function 'f2':
/*@
behavior wp_typed_ref:
- requires \separated(p2, q);
requires \valid(p2);
requires \valid(q);
+ requires \separated(p2, q);
*/
int f2(int *p2, int *q);
[wp] tests/wp_hoare/reference.i:37: Warning:
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle
index b99e101310280266d0fc3cf756af8bf32fabd5d8..535d8556ba56a0e495dfbb31d6796d3bee7b3636 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/refguards.res.oracle
@@ -72,26 +72,26 @@ Prove: d != c.
Memory model hypotheses for function 'f':
/*@
behavior wp_typed_ref:
- requires \separated(c, d, {a + (..), b + (..)});
requires \valid(c);
requires \valid(d);
+ requires \separated(c, d, {a + (..), b + (..)});
*/
void f(int *a, int *b, int *c, int *d, int k);
[wp] tests/wp_hoare/refguards.i:25: Warning:
Memory model hypotheses for function 'h':
/*@
behavior wp_typed_ref:
- requires \separated(c, d);
requires \valid(c);
requires \valid(d);
+ requires \separated(c, d);
*/
void h(int *c, int *d, int k);
[wp] tests/wp_hoare/refguards.i:39: Warning:
Memory model hypotheses for function 's':
/*@
behavior wp_typed_ref:
- requires \separated(c, d);
requires \valid(c);
requires \valid(d);
+ requires \separated(c, d);
*/
void s(int **c, int **d, int k);
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
index ab588be9a5c14dfaecd979bc01834341e6c05cef..66bc5879f093902b5614de36af3cbf81025e4f34 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle
@@ -118,10 +118,10 @@
Memory model hypotheses for function 'ref_ctr_nr':
/*@
behavior wp_typed_ref:
- requires \separated(ref, ref1, ref2);
requires \valid(ref);
requires \valid(ref1);
requires \valid(ref2);
+ requires \separated(ref, ref1, ref2);
*/
int ref_ctr_nr(int *ref, int *ref1, int *ref2);
[wp] tests/wp_hoare/dispatch_var.i:158: Warning:
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/memory_hypotheses_checking.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/memory_hypotheses_checking.res.oracle
index 6a5957ad9bc912905cd60d35a230bb32192e39ea..da1d58667029622f44e24d74f24031b12720acb4 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/memory_hypotheses_checking.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/memory_hypotheses_checking.res.oracle
@@ -10,23 +10,23 @@
[wp] [Qed] Goal typed_ref_call_sep_ok_call_sep_wp_typed_ref_requires_2 : Valid
[wp] [Qed] Goal typed_ref_call_sep_bad_sep_assigns_exit : Valid
[wp] [Qed] Goal typed_ref_call_sep_bad_sep_assigns_normal : Valid
-[wp] [Alt-Ergo] Goal typed_ref_call_sep_bad_sep_call_sep_wp_typed_ref_requires : Unsuccess
-[wp] [Qed] Goal typed_ref_call_sep_bad_sep_call_sep_wp_typed_ref_requires_2 : Valid
+[wp] [Qed] Goal typed_ref_call_sep_bad_sep_call_sep_wp_typed_ref_requires : Valid
+[wp] [Alt-Ergo] Goal typed_ref_call_sep_bad_sep_call_sep_wp_typed_ref_requires_2 : Unsuccess
[wp] [Qed] Goal typed_ref_call_sep_bad_valid_assigns_exit_part1 : Valid
[wp] [Qed] Goal typed_ref_call_sep_bad_valid_assigns_exit_part2 : Valid
[wp] [Qed] Goal typed_ref_call_sep_bad_valid_assigns_normal_part1 : Valid
[wp] [Qed] Goal typed_ref_call_sep_bad_valid_assigns_normal_part2 : Valid
-[wp] [Qed] Goal typed_ref_call_sep_bad_valid_call_sep_wp_typed_ref_requires : Valid
-[wp] [Alt-Ergo] Goal typed_ref_call_sep_bad_valid_call_sep_wp_typed_ref_requires_2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_ref_call_sep_bad_valid_call_sep_wp_typed_ref_requires : Unsuccess
+[wp] [Qed] Goal typed_ref_call_sep_bad_valid_call_sep_wp_typed_ref_requires_2 : Valid
[wp] [Qed] Goal typed_ref_gptr_sep_assigns : Valid
[wp] [Qed] Goal typed_ref_call_gptr_sep_ok_assigns_exit : Valid
[wp] [Qed] Goal typed_ref_call_gptr_sep_ok_assigns_normal : Valid
-[wp] [Qed] Goal typed_ref_call_gptr_sep_ok_call_gptr_sep_wp_typed_ref_requires : Valid
-[wp] [Alt-Ergo] Goal typed_ref_call_gptr_sep_ok_call_gptr_sep_wp_typed_ref_requires_2 : Valid
+[wp] [Alt-Ergo] Goal typed_ref_call_gptr_sep_ok_call_gptr_sep_wp_typed_ref_requires : Valid
+[wp] [Qed] Goal typed_ref_call_gptr_sep_ok_call_gptr_sep_wp_typed_ref_requires_2 : Valid
[wp] [Qed] Goal typed_ref_call_gptr_sep_bad_assigns_exit : Valid
[wp] [Qed] Goal typed_ref_call_gptr_sep_bad_assigns_normal : Valid
-[wp] [Alt-Ergo] Goal typed_ref_call_gptr_sep_bad_call_gptr_sep_wp_typed_ref_requires : Unsuccess
-[wp] [Alt-Ergo] Goal typed_ref_call_gptr_sep_bad_call_gptr_sep_wp_typed_ref_requires_2 : Valid
+[wp] [Alt-Ergo] Goal typed_ref_call_gptr_sep_bad_call_gptr_sep_wp_typed_ref_requires : Valid
+[wp] [Alt-Ergo] Goal typed_ref_call_gptr_sep_bad_call_gptr_sep_wp_typed_ref_requires_2 : Unsuccess
[wp] [Qed] Goal typed_ref_assigns_ptr_assigns : Valid
[wp] [Qed] Goal typed_ref_call_assigns_ptr_ok_assigns_exit : Valid
[wp] [Qed] Goal typed_ref_call_assigns_ptr_ok_assigns_normal : Valid
@@ -34,8 +34,8 @@
[wp] [Qed] Goal typed_ref_call_assigns_ptr_ok_call_assigns_ptr_wp_typed_ref_requires_2 : Valid
[wp] [Qed] Goal typed_ref_call_assigns_ptr_bad_assigns_exit : Valid
[wp] [Qed] Goal typed_ref_call_assigns_ptr_bad_assigns_normal : Valid
-[wp] [Alt-Ergo] Goal typed_ref_call_assigns_ptr_bad_call_assigns_ptr_wp_typed_ref_requires : Unsuccess
-[wp] [Qed] Goal typed_ref_call_assigns_ptr_bad_call_assigns_ptr_wp_typed_ref_requires_2 : Valid
+[wp] [Qed] Goal typed_ref_call_assigns_ptr_bad_call_assigns_ptr_wp_typed_ref_requires : Valid
+[wp] [Alt-Ergo] Goal typed_ref_call_assigns_ptr_bad_call_assigns_ptr_wp_typed_ref_requires_2 : Unsuccess
[wp] [Qed] Goal typed_ref_add_return_ok_ensures : Valid
[wp] [Qed] Goal typed_ref_add_return_ok_assigns : Valid
[wp] [Qed] Goal typed_ref_add_return_ok_wp_typed_ref_ensures : Valid
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle
index 6fa2c547d939685057c4e3ce840a76ab810eb7e8..c94049ea06d84693c16c54c4dc50a3e5083ea89c 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle
@@ -45,9 +45,9 @@
Memory model hypotheses for function 'f2':
/*@
behavior wp_typed_ref:
- requires \separated(p2, q);
requires \valid(p2);
requires \valid(q);
+ requires \separated(p2, q);
*/
int f2(int *p2, int *q);
[wp] tests/wp_hoare/reference.i:37: Warning:
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle
index 3fba6a750b4f8d97faebe8f14aca0aa61237fea0..549d47287ee22c85592ea76b95d7b7032aca6afa 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle
@@ -26,26 +26,26 @@
Memory model hypotheses for function 'f':
/*@
behavior wp_typed_ref:
- requires \separated(c, d, {a + (..), b + (..)});
requires \valid(c);
requires \valid(d);
+ requires \separated(c, d, {a + (..), b + (..)});
*/
void f(int *a, int *b, int *c, int *d, int k);
[wp] tests/wp_hoare/refguards.i:25: Warning:
Memory model hypotheses for function 'h':
/*@
behavior wp_typed_ref:
- requires \separated(c, d);
requires \valid(c);
requires \valid(d);
+ requires \separated(c, d);
*/
void h(int *c, int *d, int k);
[wp] tests/wp_hoare/refguards.i:39: Warning:
Memory model hypotheses for function 's':
/*@
behavior wp_typed_ref:
- requires \separated(c, d);
requires \valid(c);
requires \valid(d);
+ requires \separated(c, d);
*/
void s(int **c, int **d, int k);
diff --git a/src/plugins/wp/tests/wp_plugin/nullable.i b/src/plugins/wp/tests/wp_plugin/nullable.i
new file mode 100644
index 0000000000000000000000000000000000000000..ff08ead486c94dfc77c8b34d2a9a7553b6cec248
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/nullable.i
@@ -0,0 +1,34 @@
+/* run.config
+ OPT: -wp-model Caveat
+*/
+/* run.config_qualif
+ OPT: -wp-model Caveat
+*/
+
+int x ;
+int *g ;
+
+/*@ assigns *g, *p, x ; */
+void nullable_coherence(int* p /*@ wp_nullable */){
+ if(p == (void*)0){
+ //@ check must_fail: \false ;
+ return;
+ }
+ //@ check \valid(p);
+ *p = 42;
+ *g = 24;
+ x = 1;
+}
+
+//@ assigns *p, *q, *r, *s, *t ;
+void nullable_in_context
+(int* p /*@ wp_nullable */,
+ int* q /*@ wp_nullable */,
+ int* r /*@ wp_nullable */,
+ int* s, int* t)
+{
+ *p = 42;
+ *q = 42;
+ *r = 42;
+ *s = *t = 0;
+}
diff --git a/src/plugins/wp/tests/wp_plugin/nullable_ext.i b/src/plugins/wp/tests/wp_plugin/nullable_ext.i
new file mode 100644
index 0000000000000000000000000000000000000000..7225aa000f21516ce9c2596b9ff62f4e7245e7ca
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/nullable_ext.i
@@ -0,0 +1,33 @@
+/* run.config
+ OPT: -wp-model Caveat
+*/
+/* run.config_qualif
+ OPT: -wp-model Caveat
+*/
+
+int x ;
+int *g ;
+
+/*@ assigns *g, *p, x ;
+ wp_nullable_args p ;
+*/
+void nullable_coherence(int* p){
+ if(p == (void*)0){
+ //@ check must_fail: \false ;
+ return;
+ }
+ //@ check \valid(p);
+ *p = 42;
+ *g = 24;
+ x = 1;
+}
+
+/*@ assigns *p, *q, *r, *s, *t ;
+ wp_nullable_args p, q, r ;
+*/
+void nullable_in_context(int* p, int* q, int* r, int* s, int* t){
+ *p = 42;
+ *q = 42;
+ *r = 42;
+ *s = *t = 0;
+}
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/nullable.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/nullable.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1fe84b7fa72fb41c754482abcee25af6e247c822
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/nullable.res.oracle
@@ -0,0 +1,68 @@
+# frama-c -wp -wp-model 'Typed (Caveat)' [...]
+[kernel] Parsing tests/wp_plugin/nullable.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: In caveat model with nullable arguments, -wp-(no)-rte shall be explicitly positioned.
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function nullable_coherence
+------------------------------------------------------------
+
+Goal Check 'must_fail' (file tests/wp_plugin/nullable.i, line 14):
+Assume { (* Then *) Have: null = pointer_p. }
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_plugin/nullable.i, line 17):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/nullable.i, line 11) in 'nullable_coherence':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function nullable_in_context
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/nullable.i, line 23) in 'nullable_in_context' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/nullable.i, line 23) in 'nullable_in_context' (2/2):
+Effect at line 33
+Prove: true.
+
+------------------------------------------------------------
+[wp] tests/wp_plugin/nullable.i:12: Warning:
+ Memory model hypotheses for function 'nullable_coherence':
+ /*@
+ behavior wp_typed_caveat:
+ requires \valid(g);
+ requires \valid(p) ∨ p ≡ \null;
+ requires \separated(g, &x);
+ requires \separated(p, &x);
+ requires p ≢ \null ⇒ \separated(g, p, &x);
+ */
+ void nullable_coherence(int *p /*@ wp_nullable */);
+[wp] tests/wp_plugin/nullable.i:24: Warning:
+ Memory model hypotheses for function 'nullable_in_context':
+ /*@
+ behavior wp_typed_caveat:
+ requires \valid(s);
+ requires \valid(t);
+ requires \valid(p) ∨ p ≡ \null;
+ requires \valid(q) ∨ q ≡ \null;
+ requires \valid(r) ∨ r ≡ \null;
+ requires p ≢ \null ⇒ \separated(p, s, t);
+ requires q ≢ \null ⇒ \separated(q, s, t);
+ requires q ≢ \null ⇒ p ≢ \null ⇒ \separated(q, p);
+ requires r ≢ \null ⇒ \separated(r, s, t);
+ requires r ≢ \null ⇒ p ≢ \null ⇒ \separated(r, p);
+ requires r ≢ \null ⇒ q ≢ \null ⇒ \separated(r, q);
+ */
+ void nullable_in_context(int *p /*@ wp_nullable */,
+ int *q /*@ wp_nullable */,
+ int *r /*@ wp_nullable */, int *s, int *t);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..b4246e6986ee28aa5501e570f37ff31edc9d1282
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/nullable_ext.res.oracle
@@ -0,0 +1,68 @@
+# frama-c -wp -wp-model 'Typed (Caveat)' [...]
+[kernel] Parsing tests/wp_plugin/nullable_ext.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: In caveat model with nullable arguments, -wp-(no)-rte shall be explicitly positioned.
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function nullable_coherence
+------------------------------------------------------------
+
+Goal Check 'must_fail' (file tests/wp_plugin/nullable_ext.i, line 16):
+Assume { (* Then *) Have: null = pointer_p. }
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_plugin/nullable_ext.i, line 19):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/nullable_ext.i, line 11) in 'nullable_coherence':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function nullable_in_context
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/nullable_ext.i, line 25) in 'nullable_in_context' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/nullable_ext.i, line 25) in 'nullable_in_context' (2/2):
+Effect at line 32
+Prove: true.
+
+------------------------------------------------------------
+[wp] tests/wp_plugin/nullable_ext.i:14: Warning:
+ Memory model hypotheses for function 'nullable_coherence':
+ /*@
+ behavior wp_typed_caveat:
+ requires \valid(g);
+ requires \valid(p) ∨ p ≡ \null;
+ requires \separated(g, &x);
+ requires \separated(p, &x);
+ requires p ≢ \null ⇒ \separated(g, p, &x);
+ */
+ void nullable_coherence(int *p /*@ wp_nullable */);
+[wp] tests/wp_plugin/nullable_ext.i:28: Warning:
+ Memory model hypotheses for function 'nullable_in_context':
+ /*@
+ behavior wp_typed_caveat:
+ requires \valid(s);
+ requires \valid(t);
+ requires \valid(p) ∨ p ≡ \null;
+ requires \valid(q) ∨ q ≡ \null;
+ requires \valid(r) ∨ r ≡ \null;
+ requires p ≢ \null ⇒ \separated(p, s, t);
+ requires q ≢ \null ⇒ \separated(q, s, t);
+ requires q ≢ \null ⇒ p ≢ \null ⇒ \separated(q, p);
+ requires r ≢ \null ⇒ \separated(r, s, t);
+ requires r ≢ \null ⇒ p ≢ \null ⇒ \separated(r, p);
+ requires r ≢ \null ⇒ q ≢ \null ⇒ \separated(r, q);
+ */
+ void nullable_in_context(int *p /*@ wp_nullable */,
+ int *q /*@ wp_nullable */,
+ int *r /*@ wp_nullable */, int *s, int *t);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle
index e5d8aa84c061c2c39a06fe1f5257ffadeaea8003..24c245a193b32ecbb0357aa353d2e21d9bce3995 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/sep.res.oracle
@@ -69,58 +69,58 @@ Prove: true.
[wp] tests/wp_plugin/sep.i:18: Warning:
Memory model hypotheses for function 'f2_p_a':
/*@ behavior wp_typed_caveat:
- requires \separated(p, &a);
- requires \valid(p); */
+ requires \valid(p);
+ requires \separated(p, &a); */
void f2_p_a(int *p);
[wp] tests/wp_plugin/sep.i:22: Warning:
Memory model hypotheses for function 'f3_p_ab':
/*@
behavior wp_typed_caveat:
- requires \separated(p, &a, &b);
requires \valid(p);
+ requires \separated(p, &a, &b);
*/
void f3_p_ab(int *p);
[wp] tests/wp_plugin/sep.i:26: Warning:
Memory model hypotheses for function 'f4_pq_ab':
/*@
behavior wp_typed_caveat:
- requires \separated(p, q, &a, &b);
requires \valid(p);
requires \valid(q);
+ requires \separated(p, q, &a, &b);
*/
void f4_pq_ab(int *p, int *q);
[wp] tests/wp_plugin/sep.i:30: Warning:
Memory model hypotheses for function 'f5_pq':
/*@
behavior wp_typed_caveat:
- requires \separated(p, q);
requires \valid(p);
requires \valid(q);
+ requires \separated(p, q);
*/
void f5_pq(int *p, int *q);
[wp] tests/wp_plugin/sep.i:34: Warning:
Memory model hypotheses for function 'f6_Pa':
/*@
behavior wp_typed_caveat:
- requires \separated(p + (..), &a);
requires \valid(p + (..));
+ requires \separated(p + (..), &a);
*/
void f6_Pa(int *p, int k);
[wp] tests/wp_plugin/sep.i:43: Warning:
Memory model hypotheses for function 'f7_pq_ad':
/*@
behavior wp_typed_caveat:
- requires \separated(p, q, &a, &d);
requires \valid(p);
requires \valid(q);
+ requires \separated(p, q, &a, &d);
*/
void f7_pq_ad(int *p, int *q);
[wp] tests/wp_plugin/sep.i:49: Warning:
Memory model hypotheses for function 'f8_pq_a':
/*@
behavior wp_typed_caveat:
- requires \separated(p, q, &a);
requires \valid(p);
requires \valid(q);
+ requires \separated(p, q, &a);
*/
void f8_pq_a(int *p, int *q);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a63862b2bf46f677cdb87a010e4272ceff395884
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable.res.oracle
@@ -0,0 +1,49 @@
+# frama-c -wp -wp-model 'Typed (Caveat)' [...]
+[kernel] Parsing tests/wp_plugin/nullable.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: In caveat model with nullable arguments, -wp-(no)-rte shall be explicitly positioned.
+[wp] Warning: Missing RTE guards
+[wp] 5 goals scheduled
+[wp] [Alt-Ergo] Goal typed_caveat_nullable_coherence_check_must_fail : Unsuccess
+[wp] [Qed] Goal typed_caveat_nullable_coherence_check : Valid
+[wp] [Qed] Goal typed_caveat_nullable_coherence_assigns : Valid
+[wp] [Qed] Goal typed_caveat_nullable_in_context_assigns_part1 : Valid
+[wp] [Qed] Goal typed_caveat_nullable_in_context_assigns_part2 : Valid
+[wp] Proved goals: 4 / 5
+ Qed: 4
+ Alt-Ergo: 0 (unsuccess: 1)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ nullable_coherence 2 - 3 66.7%
+ nullable_in_context 2 - 2 100%
+------------------------------------------------------------
+[wp] tests/wp_plugin/nullable.i:12: Warning:
+ Memory model hypotheses for function 'nullable_coherence':
+ /*@
+ behavior wp_typed_caveat:
+ requires \valid(g);
+ requires \valid(p) ∨ p ≡ \null;
+ requires \separated(g, &x);
+ requires \separated(p, &x);
+ requires p ≢ \null ⇒ \separated(g, p, &x);
+ */
+ void nullable_coherence(int *p /*@ wp_nullable */);
+[wp] tests/wp_plugin/nullable.i:24: Warning:
+ Memory model hypotheses for function 'nullable_in_context':
+ /*@
+ behavior wp_typed_caveat:
+ requires \valid(s);
+ requires \valid(t);
+ requires \valid(p) ∨ p ≡ \null;
+ requires \valid(q) ∨ q ≡ \null;
+ requires \valid(r) ∨ r ≡ \null;
+ requires p ≢ \null ⇒ \separated(p, s, t);
+ requires q ≢ \null ⇒ \separated(q, s, t);
+ requires q ≢ \null ⇒ p ≢ \null ⇒ \separated(q, p);
+ requires r ≢ \null ⇒ \separated(r, s, t);
+ requires r ≢ \null ⇒ p ≢ \null ⇒ \separated(r, p);
+ requires r ≢ \null ⇒ q ≢ \null ⇒ \separated(r, q);
+ */
+ void nullable_in_context(int *p /*@ wp_nullable */,
+ int *q /*@ wp_nullable */,
+ int *r /*@ wp_nullable */, int *s, int *t);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable_ext.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable_ext.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1f2fed4938befc5db60a585320ff3e63bce02d74
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nullable_ext.res.oracle
@@ -0,0 +1,49 @@
+# frama-c -wp -wp-model 'Typed (Caveat)' [...]
+[kernel] Parsing tests/wp_plugin/nullable_ext.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: In caveat model with nullable arguments, -wp-(no)-rte shall be explicitly positioned.
+[wp] Warning: Missing RTE guards
+[wp] 5 goals scheduled
+[wp] [Alt-Ergo] Goal typed_caveat_nullable_coherence_check_must_fail : Unsuccess
+[wp] [Qed] Goal typed_caveat_nullable_coherence_check : Valid
+[wp] [Qed] Goal typed_caveat_nullable_coherence_assigns : Valid
+[wp] [Qed] Goal typed_caveat_nullable_in_context_assigns_part1 : Valid
+[wp] [Qed] Goal typed_caveat_nullable_in_context_assigns_part2 : Valid
+[wp] Proved goals: 4 / 5
+ Qed: 4
+ Alt-Ergo: 0 (unsuccess: 1)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ nullable_coherence 2 - 3 66.7%
+ nullable_in_context 2 - 2 100%
+------------------------------------------------------------
+[wp] tests/wp_plugin/nullable_ext.i:14: Warning:
+ Memory model hypotheses for function 'nullable_coherence':
+ /*@
+ behavior wp_typed_caveat:
+ requires \valid(g);
+ requires \valid(p) ∨ p ≡ \null;
+ requires \separated(g, &x);
+ requires \separated(p, &x);
+ requires p ≢ \null ⇒ \separated(g, p, &x);
+ */
+ void nullable_coherence(int *p /*@ wp_nullable */);
+[wp] tests/wp_plugin/nullable_ext.i:28: Warning:
+ Memory model hypotheses for function 'nullable_in_context':
+ /*@
+ behavior wp_typed_caveat:
+ requires \valid(s);
+ requires \valid(t);
+ requires \valid(p) ∨ p ≡ \null;
+ requires \valid(q) ∨ q ≡ \null;
+ requires \valid(r) ∨ r ≡ \null;
+ requires p ≢ \null ⇒ \separated(p, s, t);
+ requires q ≢ \null ⇒ \separated(q, s, t);
+ requires q ≢ \null ⇒ p ≢ \null ⇒ \separated(q, p);
+ requires r ≢ \null ⇒ \separated(r, s, t);
+ requires r ≢ \null ⇒ p ≢ \null ⇒ \separated(r, p);
+ requires r ≢ \null ⇒ q ≢ \null ⇒ \separated(r, q);
+ */
+ void nullable_in_context(int *p /*@ wp_nullable */,
+ int *q /*@ wp_nullable */,
+ int *r /*@ wp_nullable */, int *s, int *t);
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_labels.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_labels.1.res.oracle
index 7a7b1b25d56460d9600a2462fbc1f0b38cc49dd2..24ac613e94a8d5f7e266beeee05e591a8c77d78e 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_labels.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_labels.1.res.oracle
@@ -30,8 +30,8 @@ Prove: true.
Memory model hypotheses for function 'duplet':
/*@
behavior wp_typed_ref:
- requires \separated(pi, pj, a + (..));
requires \valid(pi);
requires \valid(pj);
+ requires \separated(pi, pj, a + (..));
*/
void duplet(int *a, int *pi, int *pj);
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_swap.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_swap.1.res.oracle
index e571b4fc2cce83e61a9d3f99da28c56e0219ce79..26c949f5c0cd9122a79829c5f595a18b0ad69a14 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_swap.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_swap.1.res.oracle
@@ -44,8 +44,8 @@ Prove: true.
Memory model hypotheses for function 'swap':
/*@
behavior wp_typed_ref:
- requires \separated(a, b);
requires \valid(a);
requires \valid(b);
+ requires \separated(a, b);
*/
void swap(int *a, int *b);
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle
index ad44942e79c58b466fce26436dad805a9512eab4..5d5ce1185b2e1c7d41d297886f473249cfc9c7df 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle
@@ -29,11 +29,11 @@
Memory model hypotheses for function 'job':
/*@
behavior wp_typed_ref:
+ requires \valid(error);
requires
\separated(
error, (int *)service_id + (..), (int *)service_result + (..), &seq,
&service_cpt
);
- requires \valid(error);
*/
int job(int a, int b, int *error);
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle
index d37ff58f250004ef4d1fb0e0262f230040f9f336..18eff921deab26414b4b24426d59fa1a2bb7d5e1 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle
@@ -20,8 +20,8 @@
Memory model hypotheses for function 'swap':
/*@
behavior wp_typed_ref:
- requires \separated(a, b);
requires \valid(a);
requires \valid(b);
+ requires \separated(a, b);
*/
void swap(int *a, int *b);
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 7f6f4e1316280036e5df8c8d578bbb2b5e487f1b..0141c03ea9ff5368e80b619ad7ce64c3253d72c0 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
@@ -72,26 +72,26 @@ Prove: P_OBS(x_2, x_3, x_4).
Memory model hypotheses for function 'implicit':
/*@
behavior wp_typed_caveat:
- requires \separated(a, r);
requires \valid(a);
requires \valid(r);
+ requires \separated(a, r);
*/
void implicit(struct S *a, int *r);
[wp] tests/wp_usage/caveat.i:32: Warning:
Memory model hypotheses for function 'explicit':
/*@
behavior wp_typed_caveat:
- requires \separated(a, r);
requires \valid(a);
requires \valid(r);
+ requires \separated(a, r);
*/
void explicit(struct S *a, int *r);
[wp] tests/wp_usage/caveat.i:47: Warning:
Memory model hypotheses for function 'observer':
/*@
behavior wp_typed_caveat:
- requires \separated(a, r);
requires \valid(a);
requires \valid(r);
+ requires \separated(a, r);
*/
void observer(struct S *a, int *r);
diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
index bd126749ac28da329e21c30afd6113528bb91909..7ec4d49d41a9cc9cf35cc6aa9ab3dd2c08c11c9d 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
@@ -101,8 +101,8 @@ Prove: true.
Memory model hypotheses for function 'job':
/*@
behavior wp_typed_caveat:
- requires \separated(p, b + (..));
requires \valid(b + (..));
requires \valid(p);
+ requires \separated(p, b + (..));
*/
void job(struct S *p, int n, int *b);
diff --git a/src/plugins/wp/tests/wp_usage/oracle/global.2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/global.2.res.oracle
index 3489aa287459e7a28ac2466a765b8a28f44a3e89..7bb8969a653815ed38f4c1d7a8033b3de5e92220 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/global.2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/global.2.res.oracle
@@ -23,7 +23,7 @@ Prove: true.
Memory model hypotheses for function 'foo':
/*@
behavior wp_typed_ref:
- requires \separated(a, &GLOBAL);
requires \valid(a);
+ requires \separated(a, &GLOBAL);
*/
void foo(int *a);
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 c15cbee10c3bd49b6bdb5e70c103a1ebac5cb9ff..0fb3ea0ed2e6643f287e6cedf372596e6086c6f1 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
@@ -171,8 +171,8 @@ Prove: true.
Memory model hypotheses for function 'memcpy_context_vars':
/*@
behavior wp_typed:
- requires \separated(src, dst);
requires \valid(dst);
requires \valid(src);
+ requires \separated(src, dst);
*/
void memcpy_context_vars(unsigned char *src, unsigned char *dst, int len);
diff --git a/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle
index 5cd9f57c585ba881735715218f8d80be0aab2e2d..0114ddb64681e6f4636f2d82a07fdb25b9f291b4 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/issue-189.2.res.oracle
@@ -26,7 +26,7 @@ Prove: true.
Memory model hypotheses for function 'f':
/*@
behavior wp_typed_caveat:
- requires \separated(ptr, src);
requires \valid(ptr);
+ requires \separated(ptr, src);
*/
void f(char *ptr, char const *src, unsigned int idx);
diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle
index 86f77567c02d0caf7aab6020ddf1b5cb07631098..5ebef0000b8e36cb669571dd841f5ee001c4a791 100644
--- a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle
@@ -24,8 +24,8 @@
Memory model hypotheses for function 'job':
/*@
behavior wp_typed_caveat:
- requires \separated(p, b + (..));
requires \valid(b + (..));
requires \valid(p);
+ requires \separated(p, b + (..));
*/
void job(struct S *p, int n, int *b);
diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle
index e73a38c074fdf04dbda90f7e6ef41eaca850a587..4a5c45145f618785311b2456d1172e1cdfc203e2 100644
--- a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle
@@ -24,8 +24,8 @@
Memory model hypotheses for function 'memcpy_context_vars':
/*@
behavior wp_typed:
- requires \separated(src, dst);
requires \valid(dst);
requires \valid(src);
+ requires \separated(src, dst);
*/
void memcpy_context_vars(unsigned char *src, unsigned char *dst, int len);