package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Internal use

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-30.0-beta-Zinc.tar.gz

sha256=93a291a8764644df2f3618d7ea18258b5fbe0912ec98dfdfd180967afdf24474

doc/frama-c.kernel/Frama_c_kernel/Logic_typing/index.html

Module `Frama_c_kernel.Logic_typing`

Logic typing and logic environment.

val type_rel : Logic_ptree.relation -> Cil_types.relation

Relation operators conversion

since Nitrogen-20111001

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.

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_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 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 logic_infos =

| Ctor of Cil_types.logic_ctor_info
| Lfun of Cil_types.logic_info list

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 ref;
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, Format.formatter, unit, 'b) 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 -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.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

type module_builder = {

add_logic_type : Cil_types.location -> Cil_types.logic_type_info -> unit;
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