Module `ShapeDomain`

module Q = Queries

module GU = Goblintutil

module Var = Basetype.Variables

module Bool = IntDomain.Booleans

module Offs : sig ... end

module CLval = Lval.CilLval

module ListPtr : sig ... end

module ListPtrSet : sig ... end

module ListPtrSetR : sig ... end

module Edges : sig ... end

module Rhs : sig ... end

val is_private : Queries.ask -> ListPtr.t -> bool

val is_broken : (CilType.Varinfo.t -> 'a) -> ListPtr.t -> 'a

val empty_list : ListPtr.t -> Rhs.t

val nonempty_list : ListPtr.t -> Rhs.t

val unknown : ListPtr.t -> Rhs.t

exception PleaseMaterialize of ListPtr.t

exception PleaseKillMe of ListPtr.t

module SHMap : sig ... end

type listField = [

| `Prev
| `Next
| `NA

]

type lexp = ListPtr.t * listField

val list_head_type : Cil.typ -> bool

val list_head_ptr_type : Cil.typ -> bool

val eval_lp : 'a -> Cil.exp -> lexp option

val warn_todo : string -> unit

val alias_top : SHMap.key -> SHMap.t -> SHMap.t

val change_all : 
  Queries.ask ->
  'a ->
  (CilType.Varinfo.t -> bool -> 'b) ->
  ListPtrSet.t ->
  (Edges.t * Edges.t * ListPtrSet.t) ->
  SHMap.t ->
  SHMap.t

val get_backpointers : ListPtr.t -> SHMap.t -> ListPtrSet.t

val write_edge : 
  Queries.ask ->
  'a ->
  (CilType.Varinfo.t -> bool -> 'b) ->
  (ListPtrSetR.t -> Edges.t) ->
  ListPtr.t ->
  [ `Next | `Prev ] ->
  ListPtr.t ->
  SHMap.t ->
  SHMap.t

val normal : 
  Queries.ask ->
  'a ->
  (CilType.Varinfo.t -> bool -> 'b) ->
  ListPtr.t ->
  [ `Next | `Prev ] ->
  ListPtr.t ->
  SHMap.t ->
  SHMap.t

val summ : 
  Queries.ask ->
  'a ->
  (CilType.Varinfo.t -> bool -> 'b) ->
  ListPtr.t ->
  [ `Next | `Prev ] ->
  ListPtr.t ->
  SHMap.t ->
  SHMap.t

val summary_ok : 'a -> 'b -> ListPtr.t -> [ `Next | `Prev ] -> SHMap.t -> bool

val push_summary : 
  Queries.ask ->
  'a ->
  (CilType.Varinfo.t -> bool -> 'b) ->
  [ `Next | `Prev ] ->
  ListPtr.t ->
  ListPtr.t ->
  ListPtr.t ->
  SHMap.t ->
  SHMap.t

val collapse_summary : 
  Queries.ask ->
  'a ->
  (CilType.Varinfo.t -> bool -> 'b) ->
  ListPtr.t ->
  ListPtr.t ->
  SHMap.t ->
  SHMap.t

val alias : 
  Queries.ask ->
  (CilType.Varinfo.t -> bool) ->
  (CilType.Varinfo.t -> bool -> 'a) ->
  ListPtr.t ->
  ListPtr.t ->
  SHMap.t ->
  SHMap.t

val proper_list_segment : 'a -> 'b -> ListPtr.t -> SHMap.t -> bool

val proper_list_segment' : 
  'a ->
  'b ->
  ListPtr.t ->
  ListPtr.t ->
  SHMap.t ->
  bool

val kill : 
  Queries.ask ->
  'a ->
  (CilType.Varinfo.t -> bool -> 'b) ->
  ListPtr.t ->
  SHMap.t ->
  SHMap.t

val kill_vars : 
  Queries.ask ->
  'a ->
  (CilType.Varinfo.t -> bool -> 'b) ->
  Var.t list ->
  SHMap.t ->
  SHMap.t

val add_alias : 
  Queries.ask ->
  (CilType.Varinfo.t -> bool) ->
  (CilType.Varinfo.t -> bool -> 'a) ->
  ListPtr.t ->
  lexp ->
  SHMap.t ->
  SHMap.t list

val must_alias : 
  'a ->
  (CilType.Varinfo.t -> bool) ->
  lexp ->
  lexp ->
  SHMap.t ->
  bool

val write_null : 
  Queries.ask ->
  'a ->
  (CilType.Varinfo.t -> bool -> 'b) ->
  SHMap.key ->
  [< `Next | `Prev ] ->
  SHMap.t ->
  SHMap.t

val reflTransBack : 
  'a ->
  'b ->
  SHMap.t ->
  ListPtrSet.elt ->
  ListPtrSet.t ->
  ListPtrSet.t

val noone_points_at_me : ListPtr.t -> SHMap.t -> bool

val reachable : 'a -> 'b -> ListPtrSet.elt -> SHMap.t -> ListPtrSet.t

val sync_one : 
  Queries.ask ->
  'a ->
  (CilType.Varinfo.t -> bool -> 'b) ->
  SHMap.t ->
  SHMap.t
  * (Cil.varinfo * bool) list
  * (Cil.varinfo list * Cil.varinfo list) list

module Dom : sig ... end

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/ShapeDomain/index.html

Module `ShapeDomain`

package goblint

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/ShapeDomain/index.html

Module ShapeDomain

Module `ShapeDomain`