Module `Wp.CfgDump`Source

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

val new_env : 
  ?lvars:Frama_c_kernel.Cil_types.logic_var list ->
  Frama_c_kernel.Cil_types.kernel_function ->
  t_env

optionally init env with user logic variables

Sourceval add_axiom : WpPropId.prop_id -> LogicUsage.logic_lemma -> unit

Source

val add_probe : 
  t_env ->
  ?stmt:Frama_c_kernel.Cil_types.stmt ->
  string ->
  Frama_c_kernel.Cil_types.term ->
  t_prop ->
  t_prop

Source

val add_hyp : 
  ?for_pid:WpPropId.prop_id ->
  t_env ->
  WpPropId.pred_info ->
  t_prop ->
  t_prop

Sourceval add_goal : t_env -> WpPropId.pred_info -> t_prop -> t_prop

Source

val 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

Source

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

Source

val label : 
  t_env ->
  Frama_c_kernel.Cil_types.stmt option ->
  Clabels.c_label ->
  t_prop ->
  t_prop

Source

val init : 
  t_env ->
  Frama_c_kernel.Cil_types.varinfo ->
  Frama_c_kernel.Cil_types.init option ->
  t_prop ->
  t_prop

Sourceval const : t_env -> Frama_c_kernel.Cil_types.varinfo -> t_prop -> t_prop

Source

val assign : 
  t_env ->
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.lval ->
  Frama_c_kernel.Cil_types.exp ->
  t_prop ->
  t_prop

Source

val return : 
  t_env ->
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.exp option ->
  t_prop ->
  t_prop

Source

val test : 
  t_env ->
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.exp ->
  t_prop ->
  t_prop ->
  t_prop

Source

val 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_prop

Sourceval has_init : t_env -> bool

Sourceval loop_entry : t_prop -> t_prop

Sourceval loop_step : t_prop -> t_prop

Source

val call_dynamic : 
  t_env ->
  Frama_c_kernel.Cil_types.stmt ->
  WpPropId.prop_id ->
  Frama_c_kernel.Cil_types.exp ->
  (Frama_c_kernel.Cil_types.kernel_function * t_prop) list ->
  t_prop

Source

val 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_prop

Source

val 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_prop

Source

val 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_prop

Source

val 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_prop

Source

val 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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-wp.core/Wp/CfgDump/index.html

Module `Wp.CfgDump`Source

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-wp.core/Wp/CfgDump/index.html

Module Wp.CfgDumpSource

Module `Wp.CfgDump`Source