module WpStrategy:sig
..end
This file provide all the functions to build a stategy that can then
be used by the main generic calculus.
val dkey : Log.category
val debug : ('a, Format.formatter, unit) Pervasives.format -> 'a
type
annot_kind =
| |
Ahyp |
(* |
annotation is an hypothesis,
but not a goal (see Aboth) : A => ...
| *) |
| |
Agoal |
(* |
annotation is a goal,
but not an hypothesis (see Aboth): A /\ ...
| *) |
| |
Aboth of |
(* |
annotation can be used as both hypothesis and goal :
| *) |
| |
AcutB of |
(* |
annotation is use as a cut :
| *) |
| |
AcallHyp of |
(* |
annotation is a called function property to consider as an Hyp.
The pre are not here but in AcallPre since they can also
be considered as goals.
| *) |
| |
AcallPre of |
(* |
annotation is a called function precondition :
to be considered as hyp, and goal if bool=true
| *) |
An annotation can be used for different purpose.
module ForCall: Kernel_function.Map
type
annots = {
|
p_hyp : |
|
p_goal : |
|
p_both : |
|
p_cut : |
|
call_hyp : |
|
call_pre : |
|
call_asgn : |
|
a_goal : |
|
a_hyp : |
|
a_call : |
as_goal
to tell if the element is to be
considered as a goal. If false
, the element can still be used as hypthesis.type
t_annots = {
|
has_asgn_goal : |
|
has_prop_goal : |
|
info : |
val empty_acc : t_annots
val add_prop : t_annots ->
annot_kind ->
NormAtLabels.label_mapping ->
WpPropId.prop_id ->
Cil_types.predicate Cil_types.named -> t_annots
add_prop_xxx
functions below use this one.val add_prop_fct_pre : t_annots ->
annot_kind ->
Cil_types.kernel_function ->
Cil_types.funbehavior ->
assumes:Cil_types.predicate Cil_types.named option ->
Cil_types.identified_predicate -> t_annots
assumes => pre
if assumes
is given.val add_prop_fct_post : t_annots ->
annot_kind ->
Cil_types.kernel_function ->
Cil_types.funbehavior ->
Cil_types.termination_kind ->
Cil_types.identified_predicate -> t_annots
val add_prop_fct_bhv_pre : t_annots ->
annot_kind ->
Cil_types.kernel_function ->
Cil_types.funbehavior -> impl_assumes:bool -> t_annots
impl_assumes
, add b_assumes => b_requires
else add both the b_requires
and the b_assumes
val add_prop_stmt_pre : t_annots ->
annot_kind ->
Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.funbehavior ->
assumes:Cil_types.predicate Cil_types.named option ->
Cil_types.identified_predicate -> t_annots
assumes => pre
if assumes
is given.val add_prop_stmt_bhv_requires : t_annots ->
annot_kind ->
Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.funbehavior -> with_assumes:bool -> t_annots
b_requires
. Add b_assumes => b_requires
if with_assumes
val add_prop_stmt_spec_pre : t_annots ->
annot_kind ->
Cil_types.kernel_function ->
Cil_types.stmt ->
('a, Cil_types.identified_predicate, Cil_types.identified_term)
Cil_types.spec -> t_annots
assumes => requires
for all the behaviors.
Process the stmt spec precondition as an hypothesis for external properties.
Add assumes => requires
for all the behaviors.
val add_prop_stmt_post : t_annots ->
annot_kind ->
Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.funbehavior ->
Cil_types.termination_kind ->
Cil_types.logic_label option ->
assumes:Cil_types.predicate Cil_types.named option ->
Cil_types.identified_predicate -> t_annots
\old (assumes) => post
if assumes
is given.val add_prop_call_pre : t_annots ->
annot_kind ->
WpPropId.prop_id ->
assumes:Cil_types.predicate Cil_types.named ->
Cil_types.identified_predicate -> t_annots
val add_prop_call_post : t_annots ->
annot_kind ->
Cil_types.kernel_function ->
Cil_types.funbehavior ->
Cil_types.termination_kind ->
assumes:Cil_types.predicate Cil_types.named ->
Cil_types.identified_predicate -> t_annots
kf
and bhv
are the called one.val add_prop_assert : t_annots ->
annot_kind ->
Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.code_annotation ->
Cil_types.predicate Cil_types.named -> t_annots
val add_prop_loop_inv : t_annots ->
annot_kind ->
Cil_types.stmt ->
WpPropId.prop_id ->
Cil_types.predicate Cil_types.named -> t_annots
val fold_bhv_post_cond : warn:bool ->
('a -> Cil_types.identified_predicate -> 'a) ->
('b -> Cil_types.identified_predicate -> 'b) ->
'a * 'b -> (Cil_types.identified_predicate, 'c) Cil_types.behavior -> 'a * 'b
f_normal
on the Normal
postconditions,
f_exits
on the Exits
postconditions, and warn on the others.
apply f_normal
on the Normal
postconditions,
f_exits
on the Exits
postconditions, and warn on the others.
val add_assigns : t_annots ->
annot_kind ->
WpPropId.prop_id -> WpPropId.assigns_desc -> t_annots
val add_assigns_any : t_annots ->
annot_kind -> WpPropId.assigns_full_info -> t_annots
val assigns_upper_bound : ('a, 'b, 'c) Cil_types.spec ->
(('b, 'c) Cil_types.behavior * 'c Cil_types.from list) option
val add_stmt_spec_assigns_hyp : t_annots ->
Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.logic_label option ->
('a, Cil_types.identified_predicate, Cil_types.identified_term)
Cil_types.spec -> t_annots
val add_call_assigns_any : t_annots -> Cil_types.stmt -> t_annots
val add_call_assigns_hyp : t_annots ->
Cil_types.kernel_function ->
Cil_types.stmt ->
called_kf:Cil_types.kernel_function ->
Cil_types.logic_label option ->
('a, Cil_types.identified_predicate, Cil_types.identified_term)
Cil_types.spec option -> t_annots
val add_loop_assigns_hyp : t_annots ->
Cil_types.kernel_function ->
Cil_types.stmt ->
(Cil_types.code_annotation * Cil_types.identified_term Cil_types.from list)
option -> t_annots
val add_fct_bhv_assigns_hyp : t_annots ->
Cil_types.kernel_function ->
Cil_types.termination_kind -> Cil_types.funbehavior -> t_annots
val get_goal_only : t_annots -> WpPropId.pred_info list
val get_hyp_only : t_annots -> WpPropId.pred_info list
val filter_both : (bool * 'a) list -> 'a list * 'a list
val get_both_hyp_goals : t_annots -> WpPropId.pred_info list * WpPropId.pred_info list
val get_call_hyp : t_annots -> ForCall.key -> WpPropId.pred_info list
get_call_pre_goal
)val get_call_pre : t_annots ->
ForCall.key -> WpPropId.pred_info list * WpPropId.pred_info list
get_both_hyp_goals
).val get_call_asgn : t_annots -> ForCall.key option -> WpPropId.assigns_full_info
val get_cut : t_annots -> (bool * WpPropId.pred_info) list
bool
in get_cut
results says if the property has to be
considered as a both goal and hyp (goal=true
, or hyp only (goal=false
)val get_asgn_hyp : t_annots -> WpPropId.assigns_full_info
val get_asgn_goal : t_annots -> WpPropId.assigns_full_info
val pp_annots : Format.formatter -> t_annots -> unit
val merge_calls : ('a -> 'a -> 'a) -> 'a ForCall.t -> 'a ForCall.t -> 'a ForCall.t
val merge_acc : annots -> annots -> annots
module Hannots:Cil2cfg.HE
(
sig
typet =
WpStrategy.annots
end
)
type
annots_tbl = {
|
tbl_annots : |
|
mutable tbl_axioms : |
|
mutable tbl_has_prop_goal : |
|
mutable tbl_has_asgn_goal : |
val create_tbl : unit -> annots_tbl
val add_on_edges : annots_tbl -> t_annots -> Cil2cfg.edge list -> unit
val add_node_annots : annots_tbl ->
Cil2cfg.t ->
Cil2cfg.node ->
t_annots * (t_annots * t_annots) -> unit
add_node_annots cfg annots v (before, (after, exits))
add the annotations for the node :
(before,(post,exits))
: exits
: \exits propertiesbefore
: preconditionsval add_loop_annots : annots_tbl ->
Cil2cfg.t ->
Cil2cfg.node ->
entry:t_annots ->
back:t_annots -> core:t_annots -> unit
val add_axiom : annots_tbl -> LogicUsage.logic_lemma -> unit
val add_all_axioms : annots_tbl -> unit
val get_annots : strategy -> Cil2cfg.edge -> t_annots
type
strategy_for_froms = {
|
get_pre : |
|
more_vars : |
type
strategy_kind =
| |
SKannots |
(* |
normal mode for annotations
| *) |
| |
SKfroms of |
type
strategy = {
|
desc : |
|
cfg : |
|
behavior_name : |
|
new_loops : |
|
strategy_kind : |
|
annots : |
val get_kf : strategy -> Kernel_function.t
val get_bhv : strategy -> string option
val is_default_behavior : strategy -> bool
val mk_strategy : string ->
Cil2cfg.t ->
string option ->
bool ->
strategy_kind -> annots_tbl -> strategy
val cfg_of_strategy : strategy -> Cil2cfg.t
val behavior_name_of_strategy : strategy -> string option
val global_axioms : strategy -> WpPropId.axiom_info list
val strategy_kind : strategy -> strategy_kind
val strategy_has_prop_goal : strategy -> bool
val strategy_has_asgn_goal : strategy -> bool
val get_annots : strategy -> Cil2cfg.edge -> t_annots
val new_loop_computation : strategy -> bool
val pp_info_of_strategy : Format.formatter -> strategy -> unit
val is_main_init : Kernel_function.t -> bool
val isInitConst : unit -> bool
-const-readonly
and -wp-init
are positionned,
and the variable is global, not extern, with a "const"
type
(see hasConstAttribute
).val isGlobalInitConst : Cil_types.varinfo -> bool
"const"
qualifier type.
Should only apply when isInitConst
is true.val mk_variant_properties : Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.code_annotation ->
Cil_types.term ->
(WpPropId.prop_id * Cil_types.predicate Cil_types.named) *
(WpPropId.prop_id * Cil_types.predicate Cil_types.named)