package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

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

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

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 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;
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, 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 -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.

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

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:(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

On This Page

Internal use