Make (frama-c-wp.Wp.LogicCompiler.Make)

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 frame : Frama_c_kernel.Cil_types.kernel_function -> 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 formal : Frama_c_kernel.Cil_types.varinfo -> value option

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

val env_let : env -> Frama_c_kernel.Cil_types.logic_var -> logic -> env

val env_letp : env -> Frama_c_kernel.Cil_types.logic_var -> Lang.F.pred -> env

val env_letval : env -> Frama_c_kernel.Cil_types.logic_var -> value -> env

Compiler

val term : env -> Frama_c_kernel.Cil_types.term -> Lang.F.term

val pred : polarity -> env -> Frama_c_kernel.Cil_types.predicate -> Lang.F.pred

val logic : env -> Frama_c_kernel.Cil_types.term -> logic

val region : env -> Frama_c_kernel.Cil_types.term -> M.loc Sigs.region

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

val call_fun : 
  env ->
  Lang.F.tau ->
  Frama_c_kernel.Cil_types.logic_info ->
  Frama_c_kernel.Cil_types.logic_label list ->
  Lang.F.term list ->
  Lang.F.term

val call_pred : 
  env ->
  Frama_c_kernel.Cil_types.logic_info ->
  Frama_c_kernel.Cil_types.logic_label list ->
  Lang.F.term list ->
  Lang.F.pred

Logic Variable and ACSL Constants

val logic_var : env -> Frama_c_kernel.Cil_types.logic_var -> logic

val logic_info : 
  env ->
  Frama_c_kernel.Cil_types.logic_info ->
  Lang.F.pred option

val has_ltype : 
  Frama_c_kernel.Cil_types.logic_type ->
  Lang.F.term ->
  Lang.F.pred

Logic Lemmas

val lemma : LogicUsage.logic_lemma -> Definitions.dlemma