package frama-c

  1. Overview
  2. Docs
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

  1. M
    Michele Alberti
  2. T
    Thibaud Antignac
  3. G
    Gergö Barany
  4. P
    Patrick Baudin
  5. T
    Thibaut Benjamin
  6. A
    Allan Blanchard
  7. L
    Lionel Blatter
  8. F
    François Bobot
  9. R
    Richard Bonichon
  10. Q
    Quentin Bouillaguet
  11. D
    David Bühler
  12. Z
    Zakaria Chihani
  13. L
    Loïc Correnson
  14. J
    Julien Crétin
  15. P
    Pascal Cuoq
  16. Z
    Zaynah Dargaye
  17. B
    Basile Desloges
  18. J
    Jean-Christophe Filliâtre
  19. P
    Philippe Herrmann
  20. M
    Maxime Jacquemin
  21. F
    Florent Kirchner
  22. A
    Alexander Kogtenkov
  23. T
    Tristan Le Gall
  24. J
    Jean-Christophe Léchenet
  25. M
    Matthieu Lemerre
  26. D
    Dara Ly
  27. D
    David Maison
  28. C
    Claude Marché
  29. A
    André Maroneze
  30. T
    Thibault Martin
  31. F
    Fonenantsoa Maurica
  32. M
    Melody Méaulle
  33. B
    Benjamin Monate
  34. Y
    Yannick Moy
  35. A
    Anne Pacalet
  36. V
    Valentin Perrelle
  37. G
    Guillaume Petiot
  38. D
    Dario Pinto
  39. V
    Virgile Prevosto
  40. A
    Armand Puccetti
  41. F
    Félix Ridoux
  42. V
    Virgile Robles
  43. M
    Muriel Roger
  44. J
    Julien Signoles
  45. N
    Nicolas Stouls
  46. K
    Kostyantyn Vorobyov
  47. B
    Boris Yakobowski

Maintainers

  1. F
    frama-ci-bot@frama-c.com

Sources

frama-c-27.1-Cobalt.tar.gz
sha256=5b13574a16a58971c27909bee94ae7f37b17d897852b40c768a3d4e2e09e39d2

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

Module Frama_c_kernel.Logic_const

Smart constructors for logic annotations.

Nodes with a unique ID

creates a code annotation with a fresh id.

val fresh_code_annotation : unit -> int
  • returns

    a fresh id for a code annotation.

val refresh_code_annotation : Cil_types.code_annotation -> Cil_types.code_annotation

set a fresh id to an existing code annotation

val refresh_spec : Cil_types.funspec -> Cil_types.funspec

set fresh id to properties of an existing funspec

  • since Sodium-20150201

creates a new toplevel predicate. predicate_kind is Assert by default. It can be set to:

  • Check for a predicate that should only be used to check a property, without adding it as hypothesis for the rest of the verification.
  • Admit for a predicate that is an hypothesis for the rest of the verification and should not be checked by Frama-C.

See Cil_types.toplevel_predicate for more information.

  • since 22.0-Titanium

creates a new identified predicate with a fresh id.

  • before 22.0-Titanium

    no only_check parameter.

  • before 23.0-Vanadium

    kind parameter was named only_check.

val new_acsl_extension : string -> Cil_types.location -> bool -> Cil_types.acsl_extension_kind -> Cil_types.acsl_extension

creates a new acsl_extension with a fresh id.

  • since Chlorine-20180501

Gives a new id to an existing predicate.

  • since Oxygen-20120901
val fresh_predicate_id : unit -> int
  • returns

    a fresh id for predicates

extract a named predicate for an identified predicate.

val new_identified_term : Cil_types.term -> Cil_types.identified_term

creates a new identified term with a fresh id

val refresh_identified_term : Cil_types.identified_term -> Cil_types.identified_term

Gives a new id to an existing term.

  • since Oxygen-20120901
val fresh_term_id : unit -> int
  • returns

    a fresh id from an identified term

Logic labels

val pre_label : Cil_types.logic_label
val post_label : Cil_types.logic_label
val here_label : Cil_types.logic_label
val old_label : Cil_types.logic_label
val loop_current_label : Cil_types.logic_label
val loop_entry_label : Cil_types.logic_label
val init_label : Cil_types.logic_label
  • since Sodium-20150201

Predicates

makes a predicate with no name. Default location is unknown.

\true

val pfalse : Cil_types.predicate

\false

\old

application of predicate

&&

||

^^

!

Folds && over a list of predicates.

Folds || over a list of predicates.

local binding

==>

? :

<==>

Binary relation.

\forall

\exists

\fresh(pt,size)

\allocable

\freeable

\valid_read

\valid

\object_pointer

val pvalid_function : ?loc:Cil_types.location -> Cil_types.term -> Cil_types.predicate

\valid_function

\initialized

\dangling

\at

\valid_index: requires index having integer type or set of integers

\valid_range: requires bounds having integer type

val pseparated : ?loc:Cil_types.location -> Cil_types.term list -> Cil_types.predicate

\separated

Logic types

val instantiate : (string * Cil_types.logic_type) list -> Cil_types.logic_type -> Cil_types.logic_type

instantiate type variables in a logic type.

  • since 18.0-Argon moved from Logic_utils
val is_unrollable_ltdef : Cil_types.logic_type_info -> bool
  • returns

    true if the logic type definition can be expanded.

  • since 18.0-Argon

expands logic type definitions only. To expands both logic part and C part, uses Logic_utils.unroll_type.

  • since 18.0-Argon
val isLogicCType : (Cil_types.typ -> bool) -> Cil_types.logic_type -> bool

isLogicType test typ is false for pure logic types and the result of test for C types.

val is_list_type : Cil_types.logic_type -> bool

returns true if the type is a list<t>.

  • since Aluminium-20160501
val make_type_list_of : Cil_types.logic_type -> Cil_types.logic_type

make_type_list_of t returns the type list<t>.

  • since Aluminium-20160501
val type_of_list_elem : Cil_types.logic_type -> Cil_types.logic_type

returns the type of elements of a list type.

  • raises Failure

    if the input type is not a list type.

  • since Aluminium-20160501
val is_set_type : Cil_types.logic_type -> bool

returns true if the type is a set<t>.

  • since Neon-20140301

set_conversion ty1 ty2 returns a set type as soon as ty1 and/or ty2 is a set. Elements have type ty1, or the type of the elements of ty1 if it is itself a set-type (i.e. we do not build set of sets that way).

converts a type into the corresponding set type if needed. Does nothing if the argument is already a set type.

returns the type of elements of a set type.

  • raises Failure

    if the input type is not a set type.

val plain_or_set : (Cil_types.logic_type -> 'a) -> Cil_types.logic_type -> 'a

plain_or_set f t applies f to t or to the type of elements of t if it is a set type.

transform_element f t is the same as set_conversion (plain_or_set f t) t

  • since Nitrogen-20111001
val is_plain_type : Cil_types.logic_type -> bool

true if the argument is not a set type.

make_arrow_type args rt returns a rt if args is empty or the corresponding Larrow type.

  • since 25.0-Manganese
val is_boolean_type : Cil_types.logic_type -> bool
  • returns

    true if the argument is the boolean type.

val boolean_type : Cil_types.logic_type
  • since Sodium-20150201

Logic Terms

returns a anonymous term of the given type.

val trange : ?loc:Cil_datatype.Location.t -> (Cil_types.term option * Cil_types.term option) -> Cil_types.term

.. of integers

val tinteger : ?loc:Cil_datatype.Location.t -> int -> Cil_types.term

integer constant

val tinteger_s64 : ?loc:Cil_datatype.Location.t -> int64 -> Cil_types.term

integer constant

integer constant

  • since Oxygen-20120901
val treal : ?loc:Cil_datatype.Location.t -> float -> Cil_types.term

real constant

val treal_zero : ?loc:Cil_datatype.Location.t -> ?ltyp:Cil_types.logic_type -> unit -> Cil_types.term

real zero

val tstring : ?loc:Cil_datatype.Location.t -> string -> Cil_types.term

string constant

\at

\old

  • since Nitrogen-20111001

variable

\result

cast to the given C type

coercion to the given logic type

val is_result : Cil_types.term -> bool

true if the term is \result (potentially enclosed in \at)

val is_exit_status : Cil_types.term -> bool

true if the term is \exit_status (potentially enclosed in \at)

  • since Nitrogen-20111001

Logic Offsets

Equivalent to lastOffset for terms.

  • since Oxygen-20120901

Equivalent to addOffset for terms.

  • since Oxygen-20120901

Equivalent to addOffsetLval for terms.

  • since Oxygen-20120901