module Logic_typing: sig
.. end
val type_rel : Logic_ptree.relation -> Cil_types.relation
Relation operators conversion
Since Nitrogen-20111001
val type_binop : Logic_ptree.binop -> Cil_types.binop
Arithmetic binop conversion. Addition and Substraction are always
considered as being used on integers. It is the responsibility of the
user to introduce PlusPI/IndexPI, MinusPI and MinusPP where needed.
Since Nitrogen-20111001
val unescape : string -> string
val wcharlist_of_string : string -> int64 list
val is_arithmetic_type : Cil_types.logic_type -> bool
val is_integral_type : Cil_types.logic_type -> bool
val is_set_type : Cil_types.logic_type -> bool
val is_array_type : Cil_types.logic_type -> bool
val is_pointer_type : Cil_types.logic_type -> bool
val type_of_pointed : Cil_types.logic_type -> Cil_types.logic_type
val type_of_array_elem : Cil_types.logic_type -> Cil_types.logic_type
val type_of_set_elem : Cil_types.logic_type -> Cil_types.logic_type
val ctype_of_pointed : Cil_types.logic_type -> Cil_types.typ
val ctype_of_array_elem : Cil_types.logic_type -> Cil_types.typ
val add_offset_lval : Cil_types.term_offset -> Cil_types.term_lval -> Cil_types.term_lval
Deprecated.Neon-20130301 use Logic_const.addTermOffsetLval instead
val arithmetic_conversion : Cil_types.logic_type -> Cil_types.logic_type -> Cil_types.logic_type
module Lenv: sig
.. end
Local logic environment
type
typing_context = {
}
Functions that can be called when type-checking an extension of ACSL.
val register_behavior_extension : string ->
(typing_context:typing_context ->
loc:Cil_types.location ->
Cil_types.funbehavior -> Logic_ptree.lexpr list -> unit) ->
unit
register_behavior_extension name f
registers a typing function f
to
be used to type clause with name name
.
This function may change the funbehavior in place.
Here is a basic example:
let foo_typer ~typing_context ~loc bhv ps =
match ps with p::[] ->
bhv.b_extended <- ("FOO",42,
Logic_const.new_predicate
(typing_context.type_predicate
(typing_context.post_state Normal)
p)
)
::bhv.b_extended
| _ -> typing_context.error loc "expecting a predicate after keyword FOO"
let () = register_behavior_extension "FOO" foo_typer
Since Carbon-20101201
module Make: functor (
C
:
sig
end
) ->
sig
.. end
val append_old_and_post_labels : Lenv.t -> Lenv.t
append the Old and Post labels in the environment
val append_here_label : Lenv.t -> Lenv.t
appends the Here label in the environment
val append_pre_label : Lenv.t -> Lenv.t
appends the "Pre" label in the environment
val add_var : string -> Cil_types.logic_var -> Lenv.t -> Lenv.t
adds a given variable in local environment.
val add_result : Lenv.t -> Cil_types.logic_type -> Lenv.t
add \result
in the environment.
val enter_post_state : Lenv.t -> Cil_types.termination_kind -> Lenv.t
enter a given post-state.
val post_state_env : Cil_types.termination_kind -> Cil_types.logic_type -> Lenv.t
enter a given post-state and put \result
in the env.
NB: if the kind of the post-state is neither Normal
nor Returns
,
this is not a normal ACSL environment. Use with caution.