package frama-c

  1. Overview
  2. Docs
On This Page
  1. Internal use
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 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 append_init_label : Lenv.t -> Lenv.t

appends the "Init" label in the environment

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

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct