package frama-c

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

Module LogicCompiler.MakeSource

Parameters

module M : Sigs.Model

Signature

Definitions

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

Frames

Sourcetype call
Sourcetype frame
Sourceval pp_frame : Format.formatter -> frame -> unit
Sourceval local : descr:string -> frame
Sourceval call_pre : sigma -> call -> sigma -> frame
Sourceval call_post : sigma -> call -> sigma Sigs.sequence -> frame
Sourceval 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 Clabels.LabelMap.t -> ?descr:string -> unit -> frame
Sourceval result : unit -> result
Sourceval status : unit -> Lang.F.var
Sourceval trigger : Definitions.trigger -> unit
Sourceval guards : frame -> Lang.F.pred list
Sourceval mem_frame : Clabels.c_label -> sigma
Sourceval has_at_frame : frame -> Clabels.c_label -> bool
Sourceval mem_at_frame : frame -> Clabels.c_label -> sigma
Sourceval set_at_frame : frame -> Clabels.c_label -> sigma -> unit
Sourceval in_frame : frame -> ('a -> 'b) -> 'a -> 'b
Sourceval get_frame : unit -> frame

Environment

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

Compiler

Sourceval bootstrap_term : (env -> Frama_c_kernel.Cil_types.term -> Lang.F.term) -> unit
Sourceval bootstrap_pred : (polarity -> env -> Frama_c_kernel.Cil_types.predicate -> Lang.F.pred) -> unit
Sourceval bootstrap_logic : (env -> Frama_c_kernel.Cil_types.term -> logic) -> unit
Sourceval 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