Previous  Up  Next

Module Logic_typing

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/IndexPI, 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
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 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 : unit -> bool;
   anonCompFieldName : string;
   conditionalConversion : Cil_types.typ -> Cil_types.typ -> Cil_types.typ;
   find_macro : string -> Logic_ptree.lexpr;
   find_var : ?label:string -> string -> Cil_types.logic_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 : string -> Cil_types.exp * Cil_types.typ;
   find_comp_field : Cil_types.compinfo -> string -> Cil_types.offset;
   find_type : type_namespace -> string -> Cil_types.typ;
   find_label : string -> Cil_types.stmt Stdlib.ref;
   remove_logic_function : string -> unit;
   remove_logic_info : Cil_types.logic_info -> unit;
   remove_logic_type : string -> unit;
   remove_logic_ctor : string -> unit;
   add_logic_function : Cil_types.logic_info -> unit;
   add_logic_type : string -> Cil_types.logic_type_info -> unit;
   add_logic_ctor : string -> Cil_types.logic_ctor_info -> unit;
   find_all_logic_functions : string -> Cil_types.logic_info list;
   find_logic_type : string -> Cil_types.logic_type_info;
   find_logic_ctor : string -> Cil_types.logic_ctor_info;
   pre_state : Lenv.t;
   post_state : Cil_types.termination_kind list -> Lenv.t;
   assigns_env : Lenv.t;
   silent : bool;
   logic_type : typing_context ->
Cil_types.location ->
Lenv.t -> Logic_ptree.logic_type -> Cil_types.logic_type;
   type_predicate : typing_context ->
Lenv.t -> Logic_ptree.lexpr -> Cil_types.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.

*)
   type_term : typing_context ->
Lenv.t -> Logic_ptree.lexpr -> Cil_types.term;
   type_assigns : typing_context ->
accept_formal:bool ->
Lenv.t -> Logic_ptree.assigns -> Cil_types.assigns;
   error : 'a 'b.
Cil_types.location ->
('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a;
   on_error : 'a 'b. ('a -> 'b) -> (unit -> unit) -> 'a -> 'b;
}

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.

val error : Cil_types.location ->
       ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a

raises an error at the given location and with the given message.

val on_error : ('a -> 'b) -> (unit -> 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.

Internal use

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