package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

module M : Sigs.Model

Signature

Definitions

type value = M.loc Sigs.value
type logic = M.loc Sigs.logic
type result = M.loc Sigs.result
type sigma = M.Sigma.t
type chunk = M.Chunk.t

Frames

type call
type frame
val pp_frame : Stdlib.Format.formatter -> frame -> unit
val local : descr:string -> frame
val call : ?result:M.loc -> Frama_c_kernel.Cil_types.kernel_function -> value list -> call
val call_pre : sigma -> call -> sigma -> frame
val call_post : sigma -> call -> sigma Sigs.sequence -> frame
val mk_frame : ?kf:Frama_c_kernel.Cil_types.kernel_function -> ?result:result -> ?status:Lang.F.var -> ?formals:value Frama_c_kernel.Cil_datatype.Varinfo.Map.t -> ?labels:sigma Wp__.Clabels.LabelMap.t -> ?descr:string -> unit -> frame
val return : unit -> Frama_c_kernel.Cil_types.typ
val result : unit -> result
val status : unit -> Lang.F.var
val trigger : Definitions.trigger -> unit
val guards : frame -> Lang.F.pred list
val mem_frame : Clabels.c_label -> sigma
val has_at_frame : frame -> Clabels.c_label -> bool
val mem_at_frame : frame -> Clabels.c_label -> sigma
val set_at_frame : frame -> Clabels.c_label -> sigma -> unit
val in_frame : frame -> ('a -> 'b) -> 'a -> 'b
val get_frame : unit -> frame

Environment

type env
val mk_env : ?here:sigma -> ?lvars:Frama_c_kernel.Cil_datatype.Logic_var.t list -> unit -> env
val current : env -> sigma
val move_at : env -> sigma -> env
val env_at : env -> Clabels.c_label -> env
val mem_at : env -> Clabels.c_label -> sigma

Compiler

val bootstrap_term : (env -> Frama_c_kernel.Cil_types.term -> Lang.F.term) -> unit
val bootstrap_pred : (polarity -> env -> Frama_c_kernel.Cil_types.predicate -> Lang.F.pred) -> unit
val bootstrap_logic : (env -> Frama_c_kernel.Cil_types.term -> logic) -> unit
val bootstrap_region : (env -> Frama_c_kernel.Cil_types.term -> M.loc Sigs.region) -> unit

Application

Logic Variable and ACSL Constants

Logic Lemmas

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