Frama-C API - W
val pretty : Stdlib.Format.formatter -> t_prop -> unitval empty : t_propval new_env : ?lvars:Frama_c_kernel.Cil_types.logic_var list -> Frama_c_kernel.Cil_types.kernel_function -> t_envoptionally init env with user logic variables
val add_axiom : WpPropId.prop_id -> LogicUsage.logic_lemma -> unitval add_probe : t_env -> ?stmt:Frama_c_kernel.Cil_types.stmt -> string -> Frama_c_kernel.Cil_types.term -> t_prop -> t_propval add_hyp : ?for_pid:WpPropId.prop_id -> t_env -> WpPropId.pred_info -> t_prop -> t_propval add_goal : t_env -> WpPropId.pred_info -> t_prop -> t_propval add_terminates_subgoal : t_env -> (WpPropId.prop_id * 'a) -> ?deps:Frama_c_kernel.Property.Set.t -> Frama_c_kernel.Cil_types.predicate -> Frama_c_kernel.Cil_types.stmt -> Wp__.Mcfg.terminates_source -> t_prop -> t_propval add_assigns : t_env -> WpPropId.assigns_info -> t_prop -> t_propval use_assigns : t_env -> WpPropId.prop_id option -> WpPropId.assigns_desc -> t_prop -> t_propuse_assigns env hid kind assgn goal performs the havoc on the goal. * hid should be None iff assgn is WritesAny, * and tied to the corresponding identified_property otherwise.
val label : t_env -> Frama_c_kernel.Cil_types.stmt option -> Clabels.c_label -> t_prop -> t_propval init : t_env -> Frama_c_kernel.Cil_types.varinfo -> Frama_c_kernel.Cil_types.init_or_str option -> t_prop -> t_propval const : t_env -> Frama_c_kernel.Cil_types.varinfo -> t_prop -> t_propval assign : t_env -> Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.lval -> Frama_c_kernel.Cil_types.exp -> t_prop -> t_propval return : t_env -> Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.exp option -> t_prop -> t_propval test : t_env -> Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.exp -> t_prop -> t_prop -> t_propval switch : t_env -> Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.exp -> (Frama_c_kernel.Cil_types.exp list * t_prop) list -> t_prop -> t_propval has_init : t_env -> boolval call_dynamic : t_env -> Frama_c_kernel.Cil_types.stmt -> WpPropId.prop_id -> Frama_c_kernel.Cil_types.lhost -> (Frama_c_kernel.Cil_types.kernel_function * t_prop) list -> t_propval call_goal_precond : t_env -> Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.exp list -> pre:WpPropId.pred_info list -> t_prop -> t_propval call_terminates : t_env -> Frama_c_kernel.Cil_types.stmt -> kind:Wp__.Mcfg.terminates_source -> ?kf:Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.exp list -> WpPropId.pred_info -> callee_t:Frama_c_kernel.Cil_types.predicate -> t_prop -> t_propval call_decreases : t_env -> Frama_c_kernel.Cil_types.stmt -> ?kf:Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.exp list -> WpPropId.variant_info -> ?caller_t:Frama_c_kernel.Cil_types.predicate -> ?callee_d:Frama_c_kernel.Cil_types.variant -> t_prop -> t_propval call : t_env -> Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.lval option -> Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.exp list -> pre:WpPropId.pred_info list -> post:WpPropId.pred_info list -> pexit:WpPropId.pred_info list -> assigns:Frama_c_kernel.Cil_types.assigns -> p_post:t_prop -> p_exit:t_prop -> t_propval scope : t_env -> Frama_c_kernel.Cil_types.varinfo list -> Wp__.Mcfg.scope -> t_prop -> t_propval build_prop_of_from : t_env -> WpPropId.pred_info list -> t_prop -> t_propbuild p => alpha(p) for functional dependencies verification.