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 =
| Typedef
| Struct
| Union
| Enum(*

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

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

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