Module Wp.CfgDumpSource

Sourcetype t_env
Sourcetype t_prop
Sourceval pretty : Format.formatter -> t_prop -> unit
Sourceval merge : t_env -> t_prop -> t_prop -> t_prop
Sourceval empty : t_prop

optionally init env with user logic variables

Sourceval add_hyp : ?for_pid:WpPropId.prop_id -> t_env -> WpPropId.pred_info -> t_prop -> t_prop
Sourceval 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_prop
Sourceval add_assigns : t_env -> WpPropId.assigns_info -> t_prop -> t_prop
Sourceval use_assigns : t_env -> WpPropId.prop_id option -> WpPropId.assigns_desc -> t_prop -> t_prop

use_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.

Sourceval has_init : t_env -> bool
Sourceval loop_entry : t_prop -> t_prop
Sourceval loop_step : t_prop -> t_prop
Sourceval scope : t_env -> Frama_c_kernel.Cil_types.varinfo list -> Wp__.Mcfg.scope -> t_prop -> t_prop
Sourceval close : t_env -> t_prop -> t_prop
Sourceval build_prop_of_from : t_env -> WpPropId.pred_info list -> t_prop -> t_prop

build p => alpha(p) for functional dependencies verification.

Sourceval fopen : Frama_c_kernel.Cil_types.kernel_function -> string option -> unit
Sourceval flush : unit -> unit