diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index 3ec3b7227a1b0744cae8d2817be3cd31ce299614..dbf2df8ce7a15614a2235f8fd11fea846bf7d5be 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -59,7 +59,8 @@ let library = "cint"
let make_fun_int op i =
Lang.extern_f ~library ~result:Logic.Int "%s_%a" op Ctypes.pp_int i
let make_pred_int op i =
- Lang.extern_f ~library ~result:Logic.Prop "%s_%a" op Ctypes.pp_int i
+ Lang.extern_f
+ ~library ~result:Logic.Prop ~coloring:true "%s_%a" op Ctypes.pp_int i
(* let fun_int op = Ctypes.imemo (make_fun_int op) *) (* unused for now *)
(* let pred_int op = Ctypes.imemo (make_pred_int op) *) (* unused for now *)
diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index 6f74f1dcde905233dcfc5a0bc4817c3e1a54d1db..38d6f4bb1381a6bc9730aaf1b93897024226ecc6 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -1304,22 +1304,31 @@ struct
(fun fs e -> Fset.union fs (phi e))
Fset.empty es
- let rec gvars_of_term m t =
+ let rec gvars_of_term ~deep m t =
try Tmap.find t m.footprint
with Not_found ->
- match F.repr t with
- | Fun(f,[]) -> Gset.singleton f , Fset.empty
- | Fun(f,_) -> Gset.empty , fset_of_lfun m f
- | Rget(_,fd) -> Gset.empty , Fset.singleton fd
- | Rdef fts -> Gset.empty ,
- List.fold_left (fun fs (f,_) -> Fset.add f fs)
- Fset.empty fts
- | _ ->
- let gs = ref FP.empty in
- let collect m gs e = gs := FP.union !gs (gvars_of_term m e) in
+ let collect_subterms acc =
+ let gs = ref acc in
+ let collect m gs e = gs := FP.union !gs (gvars_of_term ~deep m e) in
F.lc_iter (collect m gs) t ;
let s = !gs in
m.footprint <- Tmap.add t s m.footprint ; s
+ in
+ match F.repr t with
+ | Fun(f,[]) ->
+ Gset.singleton f , Fset.empty
+ | Fun(f,_) when not deep || is_coloring_lfun f ->
+ Gset.empty , fset_of_lfun ~deep m f
+ | Fun(f,_) ->
+ collect_subterms (Gset.empty , fset_of_lfun ~deep m f)
+ | Rget(_,fd) ->
+ Gset.empty , Fset.singleton fd
+ | Rdef fts ->
+ Gset.empty ,
+ List.fold_left (fun fs (f,_) -> Fset.add f fs)
+ Fset.empty fts
+ | _ ->
+ collect_subterms FP.empty
and gvars_of_pred m p = gvars_of_term m (F.e_prop p)
@@ -1340,12 +1349,12 @@ struct
let tf = Lang.tau_of_field fd in
Fset.add fd (fset_of_tau tf)
- and fset_of_lemma m d =
- snd (gvars_of_pred m d.Definitions.l_lemma)
+ and fset_of_lemma ~deep m d =
+ snd (gvars_of_pred ~deep m d.Definitions.l_lemma)
and fset_of_var x = fset_of_tau (F.tau_of_var x)
- and fset_of_lfun m f =
+ and fset_of_lfun ~deep m f =
try Gmap.find f m.footcalls
with Not_found ->
(* bootstrap recursive calls *)
@@ -1358,9 +1367,9 @@ struct
let df =
match d.d_definition with
| Logic _ -> Fset.empty
- | Function(_,_,t) -> snd (gvars_of_term m t)
- | Predicate(_,p) -> snd (gvars_of_pred m p)
- | Inductive ds -> fsetmap (fset_of_lemma m) ds
+ | Function(_,_,t) -> snd (gvars_of_term ~deep m t)
+ | Predicate(_,p) -> snd (gvars_of_pred ~deep m p)
+ | Inductive ds -> fsetmap (fset_of_lemma ~deep m) ds
in Fset.union ds df
with Not_found ->
Fset.empty
@@ -1368,7 +1377,7 @@ struct
let collect_have m p =
begin
- m.gs <- FP.union m.gs (gvars_of_pred m p) ;
+ m.gs <- FP.union m.gs (gvars_of_pred ~deep:true m p) ;
m.xs <- Vars.union m.xs (F.varsp p) ;
end
@@ -1387,7 +1396,7 @@ struct
| _ ->
if Vars.subset (F.varsp p) m.xs then
begin
- let gs = gvars_of_pred m p in
+ let gs = gvars_of_pred ~deep:false m p in
if FP.subset gs m.gs then p else
if FP.intersect gs m.gs then
(m.fixpoint <- false ; m.gs <- FP.union gs m.gs ; p)
@@ -1425,6 +1434,7 @@ struct
footcalls = Gmap.empty ;
} in
List.iter (collect_step m) seq.seq_list ; collect_have m g ;
+ Kernel.debug ~level:3 "Collected %a" pp_used m ;
let rec loop () =
m.fixpoint <- true ;
let hs' = filter_steplist m seq.seq_list in
diff --git a/src/plugins/wp/Cvalues.ml b/src/plugins/wp/Cvalues.ml
index d26aee33e7d63313fd60a43d4d65ceaa2d7354db..207ac81a387db1f63c5eff26e6a0e0d47d0d1ad9 100644
--- a/src/plugins/wp/Cvalues.ml
+++ b/src/plugins/wp/Cvalues.ml
@@ -241,7 +241,7 @@ struct
and is_record c s =
Definitions.call_pred
- (Lang.generated_p (C.prefix ^ Lang.comp_id c))
+ (Lang.generated_p ~coloring:true (C.prefix ^ Lang.comp_id c))
(fun lfun ->
let basename = if c.cstruct then "S" else "U" in
let s = Lang.freshvar ~basename (Lang.t_comp c) in
@@ -261,7 +261,7 @@ struct
and is_array elt ds t =
Definitions.call_pred
- (Lang.generated_p (array_name elt ds))
+ (Lang.generated_p ~coloring:true (array_name elt ds))
(fun lfun ->
let cluster =
match elt with
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 7003dcb3557536e46ec4500519fe2700ebe83c8d..d7ec3fb726f64d6c0aa4fd778ee20f86324b0c2c 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -430,6 +430,7 @@ and model = {
m_result : sort ;
m_typeof : tau option list -> tau ;
m_source : source ;
+ m_coloring : bool ;
}
and source =
@@ -448,6 +449,10 @@ let tau_of_lfun phi ts =
| Sbool -> Bool
| _ -> m.m_typeof ts
+let is_coloring_lfun = function
+ | ACSL _ | CTOR _ -> false
+ | Model { m_coloring } -> m_coloring
+
type balance = Nary | Left | Right
let not_found _ = raise Not_found
@@ -467,6 +472,7 @@ let symbolf
?(params=[])
?(sort=Logic.Sdata)
?(result:tau option)
+ ?(coloring=false)
?(typecheck:(tau option list -> tau) option)
name =
let buffer = Buffer.create 80 in
@@ -500,20 +506,21 @@ let symbolf
m_result = result ;
m_typeof = typeof ;
m_source = source ;
+ m_coloring = coloring ;
}
) (Format.formatter_of_buffer buffer) name
let extern_s
- ~library ?link ?category ?params ?sort ?result ?typecheck name =
+ ~library ?link ?category ?params ?sort ?result ?coloring ?typecheck name =
symbolf
- ~library ?category ?params ?sort ?result ?typecheck ?link "%s" name
+ ~library ?category ?params ?sort ?result ?coloring ?typecheck ?link "%s" name
let extern_f
- ~library ?link ?balance ?category ?params ?sort ?result ?typecheck name =
+ ~library ?link ?balance ?category ?params ?sort ?result ?coloring ?typecheck name =
symbolf
- ~library ?category ?params ?link ?balance ?sort ?result ?typecheck name
+ ~library ?category ?params ?link ?balance ?sort ?result ?coloring ?typecheck name
-let extern_p ~library ?bool ?prop ?link ?(params=[]) () =
+let extern_p ~library ?bool ?prop ?link ?(params=[]) ?(coloring=false) () =
let link =
match bool,prop,link with
| Some b , Some p , None -> infoprover (Engine.F_bool_prop(b,p))
@@ -526,10 +533,11 @@ let extern_p ~library ?bool ?prop ?link ?(params=[]) () =
m_params = params ;
m_result = Logic.Sprop;
m_typeof = not_found;
- m_source = Extern (new_extern ~library ~link ~debug)
+ m_source = Extern (new_extern ~library ~link ~debug) ;
+ m_coloring = coloring ;
}
-let extern_fp ~library ?(params=[]) ?link phi =
+let extern_fp ~library ?(params=[]) ?link ?(coloring=false) phi =
let link = match link with
| None -> infoprover (Engine.F_call phi)
| Some link -> map_infoprover (fun phi -> Engine.F_call(phi)) link in
@@ -541,19 +549,21 @@ let extern_fp ~library ?(params=[]) ?link phi =
m_source = Extern (new_extern
~library
~link
- ~debug:phi)
+ ~debug:phi) ;
+ m_coloring = coloring ;
}
-let generated_f ?context ?category ?params ?sort ?result name =
- symbolf ?context ?category ?params ?sort ?result name
+let generated_f ?context ?category ?params ?sort ?result ?coloring name =
+ symbolf ?context ?category ?params ?sort ?result ?coloring name
-let generated_p ?context name =
+let generated_p ?context ?(coloring=false) name =
Model {
m_category = Logic.Function ;
m_params = [] ;
m_result = Logic.Sprop;
m_typeof = not_found;
- m_source = generated ?context name
+ m_source = generated ?context name ;
+ m_coloring = coloring ;
}
let extern_t name ~link ~library =
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index d2c06c5839ab1b92ca83851017b3a28ca8f12d71..c878c17272d250ad5d54fda44901680b9cc14485 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -92,6 +92,7 @@ and model = {
m_result : sort ;
m_typeof : tau option list -> tau ;
m_source : source ;
+ m_coloring : bool ;
}
and source =
@@ -123,6 +124,7 @@ val extern_s :
?params:sort list ->
?sort:sort ->
?result:tau ->
+ ?coloring:bool ->
?typecheck:(tau option list -> tau) ->
string -> lfun
@@ -134,6 +136,7 @@ val extern_f :
?params:sort list ->
?sort:sort ->
?result:tau ->
+ ?coloring:bool ->
?typecheck:(tau option list -> tau) ->
('a,Format.formatter,unit,lfun) format4 -> 'a
(** balance just give a default when link is not specified *)
@@ -144,16 +147,17 @@ val extern_p :
?prop:string ->
?link:Engine.link infoprover ->
?params:sort list ->
+ ?coloring:bool ->
unit -> lfun
val extern_fp : library:library -> ?params:sort list ->
- ?link:string infoprover -> string -> lfun
+ ?link:string infoprover -> ?coloring:bool -> string -> lfun
val generated_f : ?context:bool -> ?category:lfun category ->
- ?params:sort list -> ?sort:sort -> ?result:tau ->
+ ?params:sort list -> ?sort:sort -> ?result:tau -> ?coloring:bool ->
('a,Format.formatter,unit,lfun) format4 -> 'a
-val generated_p : ?context:bool -> string -> lfun
+val generated_p : ?context:bool -> ?coloring:bool -> string -> lfun
val extern_t:
string -> link:string infoprover -> library:library -> mdt
@@ -193,6 +197,8 @@ val parameters : (lfun -> sort list) -> unit (** definitions *)
val name_of_lfun : lfun -> string
val name_of_field : field -> string
+val is_coloring_lfun : lfun -> bool
+
(** {2 Logic Formulae} *)
module ADT : Logic.Data with type t = adt
diff --git a/src/plugins/wp/LogicCompiler.ml b/src/plugins/wp/LogicCompiler.ml
index 238250786e76b477634e4d5700ceee7c10bf460a..81aa77b29c469e1cb91c7915c20944925ac0e41d 100644
--- a/src/plugins/wp/LogicCompiler.ml
+++ b/src/plugins/wp/LogicCompiler.ml
@@ -759,7 +759,7 @@ struct
let frame = logic_frame lt_name [] in
in_frame frame
begin fun () ->
- let lfun = Lang.generated_p ("is_" ^ lt_name) in
+ let lfun = Lang.generated_p ~coloring:true ("is_" ^ lt_name) in
let tau_lt = Lang.tau_of_ltype (Ltype(lt, [])) in
Typedefs.update lt (Some lfun) ;
let term_constraint ltyp =
diff --git a/src/plugins/wp/MemMemory.ml b/src/plugins/wp/MemMemory.ml
index cc27b7e46b1b1fabf531ae155d018ae3b8fce248..2a1f2ec14ab720ecd36bbcfad79c12668358e1c1 100644
--- a/src/plugins/wp/MemMemory.ml
+++ b/src/plugins/wp/MemMemory.ml
@@ -80,15 +80,15 @@ let p_separated = Lang.extern_fp ~library "separated"
let p_included = Lang.extern_fp ~library "included"
let p_eqmem = Lang.extern_fp ~library "eqmem"
let f_havoc = Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_havoc "havoc"
-let f_region = Lang.extern_f ~library ~result:L.Int "region" (* base -> region *)
-let p_framed = Lang.extern_fp ~library "framed" (* m-pointer -> prop *)
-let p_linked = Lang.extern_fp ~library "linked" (* allocation-table -> prop *)
-let p_sconst = Lang.extern_fp ~library "sconst" (* int-memory -> prop *)
+let f_region = Lang.extern_f ~coloring:true ~library ~result:L.Int "region" (* base -> region *)
+let p_framed = Lang.extern_fp ~coloring:true ~library "framed" (* m-pointer -> prop *)
+let p_linked = Lang.extern_fp ~coloring:true ~library "linked" (* allocation-table -> prop *)
+let p_sconst = Lang.extern_fp ~coloring:true ~library "sconst" (* int-memory -> prop *)
let p_addr_lt = Lang.extern_p ~library ~bool:"addr_lt_bool" ~prop:"addr_lt" ()
let p_addr_le = Lang.extern_p ~library ~bool:"addr_le_bool" ~prop:"addr_le" ()
let f_set_init =
Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_set_init "set_init"
-let p_cinits = Lang.extern_fp ~library "cinits" (* initializaton-table -> prop *)
+let p_cinits = Lang.extern_fp ~coloring:true ~library "cinits" (* initializaton-table -> prop *)
let p_is_init_r = Lang.extern_fp ~library "is_init_range"
let p_monotonic = Lang.extern_fp ~library "monotonic_init"
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 0eee23062cc8620b7753382fea1758285d8f9bcf..f79ee802cf54e287c0282b3048637d50ca121947 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -987,7 +987,7 @@ module ChunkContent = WpContext.Generator(Chunk)
let p = Lang.freshvar ~basename:"m" (Chunk.tau_of_chunk c) in
let m = e_var p in
let name = Format.asprintf "is_%a_chunk" Ctypes.pp_int k in
- let lfun = Lang.generated_p name in
+ let lfun = Lang.generated_p ~coloring:true name in
let l = Lang.freshvar ~basename:"l" (Lang.t_addr()) in
let is_int = Cint.range k in
let def = p_forall [l] (is_int (F.e_get m (e_var l))) in
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_898.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_898.res.oracle
index d832b6f57960c51cd42578d6398f586a9028bc4f..34e350f7826cb6fed5b48e3e9a8ef03bf65231a0 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_898.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_898.res.oracle
@@ -8,7 +8,13 @@
Goal Post-condition (file tests/wp_bts/issue_898.i, line 8) in 'job':
Let a = job_0.F1_S_value.
-Assume { (* Pre-condition *) Have: is_finite_f64(a). }
+Assume {
+ Type: IsS1_S(job_0).
+ (* Pre-condition *)
+ Have: is_finite_f64(a).
+ (* Initializer *)
+ Init: (job_0.F1_S_valid) = 0.
+}
Prove: eq_f64(a, a).
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/init_const_filter.i b/src/plugins/wp/tests/wp_plugin/init_const_filter.i
new file mode 100644
index 0000000000000000000000000000000000000000..4dbc3e6224d776ce95739be959f5e6d88cc52fa4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/init_const_filter.i
@@ -0,0 +1,9 @@
+int const GlobalConst[16];
+
+/*@ requires 0 ≤ ClientId < 16; */
+void default_init(char const ClientId)
+{
+ int R1;
+ R1 = GlobalConst[ClientId];
+ //@ check X: GlobalConst[ClientId] == R1 == 0 ;
+}
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/init_const_filter.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/init_const_filter.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7fbd425a815b65e75d15de09b8782012161e7d91
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/init_const_filter.res.oracle
@@ -0,0 +1,22 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/init_const_filter.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function default_init
+------------------------------------------------------------
+
+Goal Check 'X' (file tests/wp_plugin/init_const_filter.i, line 8):
+Let x = GlobalConst_0[ClientId_0].
+Assume {
+ Type: is_sint8(ClientId_0) /\ is_sint32(x).
+ (* Heap *)
+ Type: IsArray_sint32(GlobalConst_0).
+ (* Initializer *)
+ Init: forall i : Z. ((0 <= i) -> ((i <= 15) -> (GlobalConst_0[i] = 0))).
+ (* Pre-condition *)
+ Have: (0 <= ClientId_0) /\ (ClientId_0 <= 15).
+}
+Prove: x = 0.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_filter.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_filter.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1b112dcee99ef1c95f5e50b97dfc8f8899619198
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_filter.res.oracle
@@ -0,0 +1,13 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/init_const_filter.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 1 goal scheduled
+[wp] [Alt-Ergo] Goal typed_default_init_check_X : Valid
+[wp] Proved goals: 1 / 1
+ Qed: 0
+ Alt-Ergo: 1
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ default_init - 1 1 100%
+------------------------------------------------------------