package frama-c

  1. Overview
  2. Docs

Module LogicCompiler.MakeSource

Parameters

module M : Memory.Model

Signature

Definitions

Frames

Sourcetype call
Sourcetype frame
Sourceval pp_frame : Format.formatter -> frame -> unit
Sourceval local : descr:string -> frame
Sourceval call_pre : Sigma.sigma -> call -> Sigma.sigma -> frame
Sourceval call_post : Sigma.sigma -> call -> Sigma.sigma Memory.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.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 has_at_frame : frame -> Clabels.c_label -> bool
Sourceval mem_at_frame : frame -> Clabels.c_label -> Sigma.sigma
Sourceval set_at_frame : frame -> Clabels.c_label -> Sigma.sigma -> unit
Sourceval in_frame : frame -> ('a -> 'b) -> 'a -> 'b
Sourceval get_frame : unit -> frame

Environment

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

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 Memory.region) -> unit

Application

Logic Variable and ACSL Constants

Logic Lemmas