package goblint

You can search for identifiers within the package.

in-package search v0.2.0

Static analysis framework for C

Install

dune-project

Dependency

sha256=af01aac256229f33a90a9fcbfed04b01e3097f154d4d124f006476d6387c6a66

sha512=2a93bfe16881adbc2d8dcbfe38c1e19cd24ca105d8e1eda13d02440f3002874ffe2957dfd937510765233a054a40568b0052db92e31d382a5bd215d1ec12565c

Find out if two addresses are not equal by using the MayPointTo query

module AD = ValueDomain.AD

val dummy_var : GoblintCil.typ -> Goblint_lib__UnionFind.term

val dummy_lval_print : GoblintCil.typ -> GoblintCil.exp

val return_var : GoblintCil.typ -> Goblint_lib__UnionFind.term

val ask_may_point_to : 
  Queries.ask ->
  GoblintCil.exp ->
  ValueDomain.AD.t Queries.result

val may_point_to_all_equal_terms : 
  Queries.ask ->
  GoblintCil.exp ->
  data ->
  TMap.key ->
  Z.t ->
  AD.t

Ask MayPointTo not only for the term `term`, but also for all terms that are in the same equivalence class as `term`. Then meet the result.

val may_point_to_address : 
  Queries.ask ->
  AD.t ->
  TMap.key ->
  Z.t ->
  data ->
  bool

Find out if an addresse is possibly equal to one of the addresses in `addresses` by using the MayPointTo query.

val may_point_to_same_address : 
  Queries.ask ->
  T.t ->
  T.t ->
  Z.t ->
  data ->
  bool

Find out if two addresses `t1` and `t2` are possibly equal by using the MayPointTo query.

val may_be_equal : Queries.ask -> data -> Z.t -> term -> term -> bool

Returns true iff by assigning to t1, the value of t2 could change. The parameter s is the size in bits of the variable t1 we are assigning to.

val may_point_to_one_of_these_addresses : 
  Queries.ask ->
  AD.t ->
  data ->
  term ->
  bool

Returns true if `t2` or any subterm of `t2` may possibly point to one of the addresses in `addresses`.