package goblint

  1. Overview
  2. Docs
Static analysis framework for C

Install 

dune-project
 Dependency

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

Authors

  1. S
    Simmo Saan
  2. M
    Michael Schwarz
  3. J
    Julian Erhard
  4. S
    Sarah Tilscher
  5. K
    Karoliine Holter
  6. R
    Ralf Vogler
  7. K
    Kalmer Apinis
  8. V
    Vesal Vojdani

Maintainers

  1. S
    Simmo Saan <simmo.saan@gmail.com>
  2. M
    Michael Schwarz <michael.schwarz93@gmail.com>
  3. K
    Karoliine Holter <karoliine.holter@ut.ee>

Sources

goblint-2.6.0.tbz
sha256=20d5b7332a9f6072ab9ba86c4a53b898eaf681286c56a8805c41850bbf3ddf41
sha512=7c7685cfcd9aa866bc40e813df2bfcb3c79b3d40e615d8d6d0939c5798b9d70dd7f2ba87a741f5ba0ce891e9d254627207fb28057f1f2f6611e4e0d128fd6a71

doc/goblint.solver/Goblint_solver/SideWPointSelect/Cycle/index.html

Module SideWPointSelect.CycleSource

Destabilized a called or start var. Problem: two partial context calls will be precise, but third call will widen the state. If this side destabilized some of the initial unknowns vs, there may be a side-cycle between vs and we should make y a wpoint

Parameters

module HM : Batteries.Hashtbl.S with type key = S.v
module VS : Batteries.Set.S with type elt = S.v

Signature

Sourcetype data
Sourceval create_data : (S.v -> bool) -> (S.v -> S.v -> unit) -> data

Create data required by this widening point selection strategy. The parameters are not necessarily used by all strategies.

  • parameter is_stable

    This callback should return whether an unknown is stable.

  • parameter add_infl

    Allows the strategy to record additional influences. This is mainly intended for strategies like unstable-self, which records the influence of a side-effecting unknown x to the leaf y.

Sourceval notify_side : data -> S.v option -> S.v -> unit

Notifies this strategy that a side-effect has occurred. This allows the strategy to adapt its internal data structure.

  • parameter data

    The internal state of this strategy

  • parameter x

    The optional source of the side-effect

  • parameter y

    The leaf receiving the side-effect

Sourceval record_destabilized_vs : bool

Whether the destabilization of the side-effected var should record the destabilization of called variables and start variables. This information should be passed to should_mark_wpoint by the solver.

Sourceval veto_widen : data -> unit HM.t -> VS.t -> S.v option -> S.v -> bool

This strategy can decide to prevent widening. Note that, if this strategy does not veto, this does not mean that widening will necessarily be performed. Nor does a call to this function imply that the value of the leaf has grown.

  • parameter data

    The internal state of this strategy

  • parameter called

    Set of called unknowns

  • parameter old_sides

    Prior side-effects to leaf y

  • parameter x

    Optional source of the side-effect

  • parameter y

    Side-effected leaf y

  • returns

    true: widening will not be applied; false: widening might be applied

Sourceval should_mark_wpoint : data -> unit HM.t -> VS.t -> S.v option -> S.v -> bool option -> bool

The value of the leaf has grown. Should it be marked a widening point? Widening points are widened when their value grows, unless vetoed. Even if this function is called, leaf y might already be a widening point from an earlier side-effect.

  • parameter data

    The internal state of this strategy

  • parameter called

    Set of called unknowns

  • parameter old_sides

    Prior side-effects to leaf y

  • parameter x

    Optional source of the side-effect

  • parameter y

    Side-effected leaf y

  • parameter destabilized_vs

    Optional destabilization info, described in record_destabilized_vs

  • returns

    true: mark as widening point; false: do not mark as widening point