Frama-C:
Plug-ins:
Libraries:

Frama-C API - 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 ctype_of_pointed : Cil_types.logic_type -> Cil_types.typ
val ctype_of_array_elem : Cil_types.logic_type -> Cil_types.typ
exception Typing_error of Cil_types.location * string
val mk_cast : ?explicit:bool -> Cil_types.term -> Cil_types.logic_type -> Cil_types.term
  • parameter explicit

    defaults to false, when true it means that the coercion must be explicitly introduced (when possible) e.g. we really want the wrapping behavior in the term (int) (INT_MAX+1).

  • since 32.0-Germanium
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 logic_infos =
  1. | Ctor of Cil_types.logic_ctor_info
  2. | Lfun of Cil_types.logic_info list
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 Stdlib.ref;
  10. pre_state : Lenv.t;
  11. post_state : Cil_types.termination_kind list -> Lenv.t;
  12. assigns_env : Lenv.t;
  13. silent : bool;
  14. logic_type : typing_context -> Cil_types.location -> Lenv.t -> Logic_ptree.logic_type -> Cil_types.logic_type;
  15. 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.

    *)
  16. type_term : typing_context -> Lenv.t -> Logic_ptree.lexpr -> Cil_types.term;
  17. type_assigns : typing_context -> accept_formal:bool -> Lenv.t -> Logic_ptree.assigns -> Cil_types.assigns;
  18. error : 'a 'b. Cil_types.location -> ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a;
  19. 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 -kernel-warn-key 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.

  • before 30.0-Zinc

    The following fields were present:

    remove_logic_function : string -> unit;
remove_logic_info: logic_info -> unit;
remove_logic_type: string -> unit;
remove_logic_ctor: string -> unit;
add_logic_function: logic_info -> unit;
add_logic_type: string -> logic_type_info -> unit;
add_logic_ctor: string -> logic_ctor_info -> unit;
find_all_logic_functions: string -> logic_info list;
find_logic_type: string -> logic_type_info;
find_logic_ctor: string -> logic_ctor_info;

    You shall now use directly functions from Logic_env and Logic_utils.

type module_builder = {
  1. add_logic_type : Cil_types.location -> Cil_types.logic_type_info -> unit;
  2. add_logic_function : Cil_types.location -> Cil_types.logic_info -> unit;
}

Functions that can be called when importing external modules into ACSL. See Acsl_extension.register_module_importer for details.

  • since 30.0-Zinc
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 builtin_label : string -> Cil_types.logic_builtin_label option

returns the builtin label corresponding to the given name if it exists

  • since 29.0-Copper
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:(plugin:string -> string -> bool) -> typer: (plugin:string -> string -> typing_context -> Cil_types.location -> Logic_ptree.lexpr list -> bool * Cil_types.acsl_extension_kind) -> typer_block: (plugin:string -> string -> typing_context -> Cil_types.location -> (string * Logic_ptree.extended_decl list) -> bool * Cil_types.acsl_extension_kind) -> importer: (plugin:string -> string -> module_builder -> Cil_types.location -> string list -> unit) -> unit
  • alert acsl_extension_handler This function can only be called by Acsl_extension
val get_typer : plugin:string -> string -> typing_context:typing_context -> loc:Cil_types.location -> Logic_ptree.lexpr list -> bool * Cil_types.acsl_extension_kind

Type the given extension.

  • before 30.0-Zinc

    the function took one less argument, plugin, which is now used to avoid ambiguity if plugins use the same name for an extension

val get_typer_block : plugin:string -> string -> typing_context:typing_context -> loc:Logic_ptree.location -> (string * Logic_ptree.extended_decl list) -> bool * Cil_types.acsl_extension_kind

Type the given extension block.

  • before 30.0-Zinc

    the function took one less argument, plugin, which is now used to avoid ambiguity if plugins use the same name for an extension

val get_importer : plugin:string -> string -> builder:module_builder -> loc:Logic_ptree.location -> string list -> unit

Load the given module importer extension.

  • since 30.0-Zinc

/ *