Logic_typing.Make
module _ : sig ... end
val type_of_field :
Cil_types.location ->
string ->
Cil_types.logic_type ->
Cil_types.term_offset * Cil_types.logic_type
val mk_cast :
?explicit:bool ->
Cil_types.term ->
Cil_types.logic_type ->
Cil_types.term
val conditional_conversion :
Cil_types.location ->
Logic_ptree.relation option ->
Cil_types.term ->
Cil_types.term ->
Cil_types.logic_type
conditional_conversion loc rel t1 t2
tries to find a common type between two terms, either as part of a comparison or a conditional. comparisons can notably introduce logic coercions to Real, potentially with a warning if acsl-float-compare
is active.
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.
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.