module Logic_typing:sig
..end
Logic typing and logic environment.
val type_rel : Logic_ptree.relation -> Cil_types.relation
Relation operators conversion
val type_binop : Logic_ptree.binop -> Cil_types.binop
Arithmetic binop conversion. Addition and Subtraction are always considered as being used on integers. It is the responsibility of the user to introduce PlusPI, MinusPI and MinusPP where needed.
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 is_list_type : Cil_types.logic_type -> bool
val type_of_list_elem : Cil_types.logic_type -> Cil_types.logic_type
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
val arithmetic_conversion : Cil_types.logic_type -> Cil_types.logic_type -> Cil_types.logic_type
module Lenv:sig
..end
Local logic environment
type
type_namespace =
| |
Typedef |
| |
Struct |
| |
Union |
| |
Enum |
The different namespaces a C type can belong to, used when we are searching a type by its name.
module Type_namespace:Datatype.S
with type t = type_namespace
type
typing_context = {
|
is_loop : |
|||
|
anonCompFieldName : |
|||
|
conditionalConversion : |
|||
|
find_macro : |
|||
|
find_var : |
(* | the label argument is a C label (obeying the restrictions of which label can be present in a \at). If present, the scope for searching local C variables is the one of the statement with the corresponding label. | *) |
|
find_enum_tag : |
|||
|
find_comp_field : |
|||
|
find_type : |
|||
|
find_label : |
|||
|
remove_logic_function : |
|||
|
remove_logic_info : |
|||
|
remove_logic_type : |
|||
|
remove_logic_ctor : |
|||
|
add_logic_function : |
|||
|
add_logic_type : |
|||
|
add_logic_ctor : |
|||
|
find_all_logic_functions : |
|||
|
find_logic_type : |
|||
|
find_logic_ctor : |
|||
|
pre_state : |
|||
|
post_state : |
|||
|
assigns_env : |
|||
|
silent : |
|||
|
logic_type : |
|||
|
type_predicate : |
(* | typechecks a predicate. Note that the first argument is itself a
| *) |
|
type_term : |
|||
|
type_assigns : |
|||
|
error : |
|||
|
on_error : |
(* |
| *) |
}
Functions that can be called when type-checking an extension of ACSL.
module Make:functor (
C
:
sig
val is_loop :unit -> bool
whether the annotation we want to type is contained in a loop. Only useful when creating objects of type
code_annotation
.val anonCompFieldName :string
val conditionalConversion :Cil_types.typ -> Cil_types.typ -> Cil_types.typ
val find_macro :string -> Logic_ptree.lexpr
val find_var :?label:string -> string -> Cil_types.logic_var
see corresponding field in
Logic_typing.typing_context
.val find_enum_tag :string -> Cil_types.exp * Cil_types.typ
val find_type :Logic_typing.type_namespace -> string -> Cil_types.typ
val find_comp_field :Cil_types.compinfo -> string -> Cil_types.offset
val find_label :string -> Cil_types.stmt Stdlib.ref
val remove_logic_function :string -> unit
val remove_logic_info :Cil_types.logic_info -> unit
val remove_logic_type :string -> unit
val remove_logic_ctor :string -> unit
val add_logic_function :Cil_types.logic_info -> unit
val add_logic_type :string -> Cil_types.logic_type_info -> unit
val add_logic_ctor :string -> Cil_types.logic_ctor_info -> unit
val find_all_logic_functions :string -> Cil_types.logic_info list
val find_logic_type :string -> Cil_types.logic_type_info
val find_logic_ctor :string -> Cil_types.logic_ctor_info
val integral_cast :Cil_types.typ -> Cil_types.term -> Cil_types.term
What to do when we have a term of type Integer in a context expecting a C integral type.
- Since Nitrogen-20111001
- Raises
Failure
to reject such conversionval error :Cil_types.location ->
('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'araises an error at the given location and with the given message.
- Since Magnesium-20151001
val on_error :('a -> 'b) -> (Cil_types.location * string -> unit) -> 'a -> 'b
see
Logic_typing.typing_context
.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 append_init_label : Lenv.t -> Lenv.t
appends the "Init" 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.
val set_extension_handler : is_extension:(string -> bool) ->
typer:(string ->
typing_context ->
Cil_types.location ->
Logic_ptree.lexpr list -> bool * Cil_types.acsl_extension_kind) ->
typer_block:(string ->
typing_context ->
Filepath.position * Filepath.position ->
string * Logic_ptree.extended_decl list ->
bool * Cil_types.acsl_extension_kind) ->
unit
Used to setup references related to the handling of ACSL extensions.
If your name is not Acsl_extension
, do not call this
val get_typer : string ->
typing_context:typing_context ->
loc:Filepath.position * Filepath.position ->
Logic_ptree.lexpr list -> bool * Cil_types.acsl_extension_kind
val get_typer_block : string ->
typing_context:typing_context ->
loc:Logic_ptree.location ->
string * Logic_ptree.extended_decl list ->
bool * Cil_types.acsl_extension_kind