module Logic_typing:sig
..end
val type_rel : Logic_ptree.relation -> Cil_types.relation
val type_binop : Logic_ptree.binop -> Cil_types.binop
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
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
typing_context , which allows for open recursion. Namely, it is
possible for the extension to change the type-checking functions for
the sub-nodes of the parsed tree, and not only for the toplevel lexpr .Consult the Plugin Development Guide for additional details. | *) |
|
type_term : |
|||
|
type_assigns : |
|||
|
error : |
|||
|
on_error : |
val register_behavior_extension : string ->
bool ->
(typing_context:typing_context ->
loc:Cil_types.location ->
Logic_ptree.lexpr list -> Cil_types.acsl_extension_kind) ->
unit
register_behavior_extension name status f
registers a
typing function f
to
be used to type function contract clause with name name
.
The boolean flags specifies if the extension can be assigned
a property status or not.
Here is a basic example:
let count = ref 0 in
let foo_typer ~typing_context ~loc ps =
match ps with p::[] ->
Ext_preds
)
| [] -> let id = !count in incr count; Ext_id id
| _ -> typing_context.error loc "expecting a predicate after keyword FOO"
let () = register_behavior_extension "FOO" false foo_typer
(typing_context.type_predicate
typing_context
(typing_context.post_state [Normal])
p)
Since Carbon-20101201
Consult the Plugin Development Guide for additional details.
Change in Silicon-20161101: change type of the function
Change in 19.0-Potassium: add status
argument
val register_global_extension : string ->
bool ->
(typing_context:typing_context ->
loc:Cil_types.location ->
Logic_ptree.lexpr list -> Cil_types.acsl_extension_kind) ->
unit
val register_code_annot_extension : string ->
bool ->
(typing_context:typing_context ->
loc:Cil_types.location ->
Logic_ptree.lexpr list -> Cil_types.acsl_extension_kind) ->
unit
val register_code_annot_next_stmt_extension : string ->
bool ->
(typing_context:typing_context ->
loc:Cil_types.location ->
Logic_ptree.lexpr list -> Cil_types.acsl_extension_kind) ->
unit
val register_code_annot_next_loop_extension : string ->
bool ->
(typing_context:typing_context ->
loc:Cil_types.location ->
Logic_ptree.lexpr list -> Cil_types.acsl_extension_kind) ->
unit
val register_code_annot_next_both_extension : string ->
bool ->
(typing_context:typing_context ->
loc:Cil_types.location ->
Logic_ptree.lexpr list -> Cil_types.acsl_extension_kind) ->
unit
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 typecode_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 -> var:string -> Cil_types.logic_var
see corresponding field inLogic_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 Pervasives.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
RaisesFailure
to reject such conversion
val error :Cil_types.location ->
('a, Format.formatter, unit, 'b) Pervasives.format4 -> 'araises an error at the given location and with the given message.
Since Magnesium-20151001
val on_error :('a -> 'b) -> (unit -> unit) -> 'a -> 'b
seeLogic_typing.typing_context
.
end
) ->
sig
..end
val append_old_and_post_labels : Lenv.t -> Lenv.t
val append_here_label : Lenv.t -> Lenv.t
val append_pre_label : Lenv.t -> Lenv.t
val append_init_label : Lenv.t -> Lenv.t
val add_var : string -> Cil_types.logic_var -> Lenv.t -> Lenv.t
val add_result : Lenv.t -> Cil_types.logic_type -> Lenv.t
\result
in the environment.val enter_post_state : Lenv.t -> Cil_types.termination_kind -> Lenv.t
val post_state_env : Cil_types.termination_kind -> Cil_types.logic_type -> Lenv.t
\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) ->
unit
Acsl_extension
, do not call this