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=20d5b7332a9f6072ab9ba86c4a53b898eaf681286c56a8805c41850bbf3ddf41

sha512=7c7685cfcd9aa866bc40e813df2bfcb3c79b3d40e615d8d6d0939c5798b9d70dd7f2ba87a741f5ba0ce891e9d254627207fb28057f1f2f6611e4e0d128fd6a71

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`.