package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t_env
type t_prop
val pretty : Format.formatter -> t_prop -> unit
val merge : t_env -> t_prop -> t_prop -> t_prop
val empty : t_prop

optionally init env with user logic variables

val add_axiom : WpPropId.prop_id -> LogicUsage.logic_lemma -> unit
val add_hyp : ?for_pid:WpPropId.prop_id -> t_env -> WpPropId.pred_info -> t_prop -> t_prop
val add_goal : t_env -> WpPropId.pred_info -> t_prop -> t_prop
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
val add_assigns : t_env -> WpPropId.assigns_info -> t_prop -> t_prop
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.

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

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

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