Make (frama-c.Frama_c_kernel.Logic

Parameters

module C : sig ... end

Signature

val type_of_field : 
  Cil_types.location ->
  string ->
  Cil_types.logic_type ->
  Cil_types.term_offset * Cil_types.logic_type

since Nitrogen-20111001

val mk_cast : 
  ?explicit:bool ->
  Cil_types.term ->
  Cil_types.logic_type ->
  Cil_types.term

parameter explicit
true if the cast is present in original source. defaults to false

since Nitrogen-20111001

val term : Lenv.t -> Logic_ptree.lexpr -> Cil_types.term

type-checks a term.

val predicate : Lenv.t -> Logic_ptree.lexpr -> Cil_types.predicate

val code_annot : 
  Cil_types.location ->
  string list ->
  Cil_types.logic_type ->
  Logic_ptree.code_annot ->
  Cil_types.code_annotation

code_annot loc behaviors rt annot type-checks an in-code annotation.

parameter loc
current location

parameter behaviors
list of existing behaviors

parameter rt
return type of current function

parameter annot
the annotation

val type_annot : 
  Cil_types.location ->
  Logic_ptree.type_annot ->
  Cil_types.logic_info

val model_annot : 
  Cil_types.location ->
  Logic_ptree.model_annot ->
  Cil_types.model_info

val annot : Logic_ptree.decl -> Cil_types.global_annotation

val funspec : 
  string list ->
  Cil_types.varinfo ->
  Cil_types.varinfo list option ->
  Cil_types.typ ->
  Logic_ptree.spec ->
  Cil_types.funspec

funspec behaviors f prms typ spec type-checks a function contract.

parameter behaviors
list of existing behaviors (outside of the current spec, e.g. in the spec of the corresponding declaration when type-checking the spec of a definition)

parameter f
the function

parameter prms
its parameters

parameter its
type

parameter spec
the spec to typecheck