package goblint

  1. Overview
  2. Docs
package goblint
Legend:
Library
Module
Module type
Parameter
Class
Class type

This allows us to query information about library functions.

type categories = [
  1. | `Malloc of Prelude.Ana.exp
  2. | `Calloc of Prelude.Ana.exp * Prelude.Ana.exp
  3. | `Realloc of Prelude.Ana.exp * Prelude.Ana.exp
  4. | `Assert of Prelude.Ana.exp
  5. | `Lock of bool * bool * bool
  6. | `Unlock
  7. | `ThreadCreate of Prelude.Ana.exp * Prelude.Ana.exp * Prelude.Ana.exp
  8. | `ThreadJoin of Prelude.Ana.exp * Prelude.Ana.exp
  9. | `Unknown of string
]

Categories of special functions

val classify : string -> Prelude.Ana.exp list -> categories
type action = [
  1. | `Write
    (*

    argument may be read or written to

    *)
  2. | `Read
    (*

    argument may be read

    *)
]

Specifies what is known about an argument.

val get_invalidate_action : string -> (action -> Prelude.Ana.exp list -> Prelude.Ana.exp list) option

Returns None if nothing is known about given function. * Otherwise will return function that filters out arguments * that may be read or also written to.

val get_threadsafe_inv_ac : string -> (action -> Prelude.Ana.exp list -> Prelude.Ana.exp list) option

Same as get_invalidate_action, but replaces arguments for thread-safe functions.

val add_lib_funs : string list -> unit
val add_effects : (string -> Cil.exp list -> (Cil.lval * ValueDomain.Compound.t) list option) -> unit
val effects_for : string -> Cil.exp list -> (Cil.lval * ValueDomain.Compound.t) list list
val use_special : string -> bool

This is for when we need to use special transfer function on functions calls that have definitions.

val osek_renames : bool Prelude.Ana.ref
val is_safe_uncalled : string -> bool
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct