package goblint

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

Global flags for analysis state.

val should_warn : bool ref

If this is true we output messages and collect accesses. This is set to true in control.ml before we verify the result (or already before solving if warn = 'early')

val executing_speculative_computations : bool ref

If this is true, any overflows happening in IntDomains will not lead to warnings being produced or svcomp_may_overflow being set to true. This is useful when, e.g., BaseInvariant.Make.invariant executes computations that are not in the actual program

val svcomp_may_overflow : bool ref

Whether signed overflow or underflow happened

val svcomp_may_not_terminate : bool ref

Whether the termination analysis detects the program as non-terminating

Whether an invalid free happened

val svcomp_may_invalid_free : bool ref

Whether an invalid free happened

val svcomp_may_invalid_deref : bool ref

Whether an invalid pointer dereference happened

val svcomp_may_invalid_memtrack : bool ref

Whether a memory leak occurred and there's no reference to the leaked memory

val svcomp_may_invalid_memcleanup : bool ref

Whether a memory leak occurred

val global_initialization : bool ref

A hack to see if we are currently doing global inits

val postsolving : bool ref

Whether currently in postsolver evaluations (e.g. verify, warn)

val verified : bool option ref
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