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 (10)

Authors

  1. S
    Simmo Saan
  2. M
    Michael Schwarz
  3. J
    Julian Erhard
  4. S
    Sarah Tilscher
  5. K
    Karoliine Holter
  6. M
    Michael Petter
  7. A
    Ali Rasim Kocal
  8. R
    Ralf Vogler
  9. K
    Kalmer Apinis
  10. 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.7.1.tbz
sha256=af01aac256229f33a90a9fcbfed04b01e3097f154d4d124f006476d6387c6a66
sha512=2a93bfe16881adbc2d8dcbfe38c1e19cd24ca105d8e1eda13d02440f3002874ffe2957dfd937510765233a054a40568b0052db92e31d382a5bd215d1ec12565c

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

Module SideWPointSelect.NeverSource

Never widen side-effects.

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