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 : Stdlib.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 register_lemma : LogicUsage.logic_lemma -> unit
val compile_lemma : LogicUsage.logic_lemma -> Wpo.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct