package goblint

You can search for identifiers within the package.

in-package search v0.2.0

Static analysis framework for C

Install

dune-project

Dependency

goblint.in.tum.de Edit opam file Versions (11)

Authors

Maintainers

Sources

goblint-2.8.0.tbz

sha256=9175eec0143102243964e34a0786584fd590c60422009259c705a89a27f88de4

sha512=9d760007dd8d003cf596516444ed7acc7370fc3d446e75ac71b0176522c3baae090410762f9035e7aae4f6b0e394bf28bb5b1c08ca0476920b94aa919ef04f42

doc/goblint.common/Checks/index.html

Module `Checks`

Implements a method described in this paper from Raphaël Monat, Abdelraouf Ouadjaout and Antoine Miné : https://inria.hal.science/hal-04652657v2

This allows to track checks performed during the analysis, and to mark whether they are safe, unsafe or unknown (resp. Safe, Error, Warning).

module Kind : sig ... end

module Category : sig ... end

module Check : sig ... end

module CheckMap : sig ... end

module CategoryLocationMap : sig ... end

val checks_list : (bool ref * unit CheckMap.t) CategoryLocationMap.t

Store the list of checks raised by the analysis. The bool ref stores whether all checks in the map are safe. The unit CheckMap.t is the set of checks associated with the given Category.t * CilType.Location.t pair. The bool is a reference to avoid having to use the update function when updating the value. The CheckMap.t is mutable anyway so it is not a problem.

val add_check : Check.t -> unit

val check : 
  Kind.t ->
  Category.t ->
  ('a, unit, GoblintCil.Pretty.doc, unit) format4 ->
  'a

val export : 
  unit ->
  [> `List of
       [> `Assoc of
            (string
             * [> `Assoc of
                    (string
                     * [> `Assoc of
                            (string * [> `Int of int | `String of string ])
                              list ])
                      list
               | `Null
               | `String of string ])
              list ]
         list ]

val error : Category.t -> ('a, unit, GoblintCil.Pretty.doc, unit) format4 -> 'a

val warn : Category.t -> ('a, unit, GoblintCil.Pretty.doc, unit) format4 -> 'a

val safe : Category.t -> unit

val safe_msg : 
  Category.t ->
  ('a, unit, GoblintCil.Pretty.doc, unit) format4 ->
  'a