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, 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) -> (Cil_types.location * string -> unit) -> 'a -> 'b; (*

on_error f rollback x will attempt to evaluate f x. If this triggers an error while in -continue-annot-error mode, rollback (loc,cause) will be executed (where loc is the location of the error and cause a text message indicating the issue) and the exception will be re-raised.

  • Since Chlorine-20180501
    • Change in 25.0-Manganese: rollback takes as argument the 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.

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) -> (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.

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