package goblint

You can search for identifiers within the package.

in-package search v0.2.0

Static analysis framework for C

Install

Dune Dependency

goblint.in.tum.de Readme Changelog Edit opam file Versions (8)

Authors

Maintainers

Sources

goblint-1.1.1.tbz

sha256=999272bfbd3b9b96fcd58987b237ac6e9fa6d92ef935cc89f1ea2b4205185141

sha512=f3bf6ab71cf8c258d3290da4bf9f6fe42d7c671822e0efeb0fc50afdff078ab15e352237e5c1db31c5aa3a9d430691268ed2e5e00da10f2615835f672f91683d

doc/goblint.lib/LibraryFunctions/index.html

Module `LibraryFunctions`

This allows us to query information about library functions.

type categories = [

| `Malloc of Prelude.Ana.exp
| `Calloc of Prelude.Ana.exp * Prelude.Ana.exp
| `Realloc of Prelude.Ana.exp * Prelude.Ana.exp
| `Assert of Prelude.Ana.exp
| `Lock of bool * bool * bool
| `Unlock
| `ThreadCreate of Prelude.Ana.exp * Prelude.Ana.exp * Prelude.Ana.exp
| `ThreadJoin of Prelude.Ana.exp * Prelude.Ana.exp
| `Unknown of string

]

Categories of special functions

val classify : string -> Prelude.Ana.exp list -> categories

type action = [

| `Write
(*
argument may be read or written to
*)
| `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