package goblint

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

Transformation for instrumenting the program with computed invariants as assertions (assert).

Instruments a program by inserting asserts either:

  • After an assignment to a variable (unless witness.invariant.full is activated) and
  • At join points about all local variables

OR

  • Only after pthread_mutex_lock (witness.invariant.after-lock), about all locals and globals

Limitations without witness.invariant.after-lock:

  • Currently only works for top-level variables (not inside an array, a struct, ...)
  • Does not work for accesses through pointers
  • At join points asserts all locals, but ideally should only assert ones that are modified in one of the branches

Limitations in general:

  • Removes comments, so if the original program had //UNKNOWN assertions, the annotation will be removed and they will fail on the next iteration
module EvalAssert : sig ... end
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