Module Frama_c_kernel.Logic_typing

Logic typing and logic environment.

Relation operators conversion

  • since Nitrogen-20111001

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.

  • 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 is_list_type : Cil_types.logic_type -> bool
  • since Aluminium-20160501
val type_of_list_elem : Cil_types.logic_type -> Cil_types.logic_type
  • since Aluminium-20160501
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
module Lenv : sig ... end

Local logic environment

type type_namespace =
  1. | Typedef
  2. | Struct
  3. | Union
  4. | Enum
    (*

    The different namespaces a C type can belong to, used when we are searching a type by its name.

    *)
type typing_context = {
  1. is_loop : unit -> bool;
  2. anonCompFieldName : string;
  3. conditionalConversion : Cil_types.typ -> Cil_types.typ -> Cil_types.typ;
  4. find_macro : string -> Logic_ptree.lexpr;
  5. 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.

    *)
  6. find_enum_tag : string -> Cil_types.exp * Cil_types.typ;
  7. find_comp_field : Cil_types.compinfo -> string -> Cil_types.offset;
  8. find_type : type_namespace -> string -> Cil_types.typ;
  9. find_label : string -> Cil_types.stmt ref;
  10. remove_logic_function : string -> unit;
  11. remove_logic_info : Cil_types.logic_info -> unit;
  12. remove_logic_type : string -> unit;
  13. remove_logic_ctor : string -> unit;
  14. add_logic_function : Cil_types.logic_info -> unit;
  15. add_logic_type : string -> Cil_types.logic_type_info -> unit;
  16. add_logic_ctor : string -> Cil_types.logic_ctor_info -> unit;
  17. find_all_logic_functions : string -> Cil_types.logic_info list;
  18. find_logic_type : string -> Cil_types.logic_type_info;
  19. find_logic_ctor : string -> Cil_types.logic_ctor_info;
  20. pre_state : Lenv.t;
  21. post_state : Cil_types.termination_kind list -> Lenv.t;
  22. assigns_env : Lenv.t;
  23. silent : bool;
  24. logic_type : typing_context -> Cil_types.location -> Lenv.t -> Logic_ptree.logic_type -> Cil_types.logic_type;
  25. 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.

    *)
  26. type_term : typing_context -> Lenv.t -> Logic_ptree.lexpr -> Cil_types.term;
  27. type_assigns : typing_context -> accept_formal:bool -> Lenv.t -> Logic_ptree.assigns -> Cil_types.assigns;
  28. error : 'a 'b. Cil_types.location -> ('a, Format.formatter, unit, 'b) format4 -> 'a;
  29. 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
    • before 25.0-Manganese

      rollback didn't take loc and cause as argument

    *)
}

Functions that can be called when type-checking an extension of ACSL.

module type S = sig ... end
module Make (_ : sig ... end) : S
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

  • since Sodium-20150201
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

  • since 21.0-Scandium
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