Module `Shapes.Spec`

include module type of struct include Analyses.DefaultSpec end

type marshal = unit

val finalize : unit -> unit

val should_join : 'a -> 'b -> bool

val call_descr : Cil.fundec -> 'a -> string

val intrpt : ('a, 'b, 'c) Analyses.ctx -> 'a

val vdecl : ('a, 'b, 'c) Analyses.ctx -> 'd -> 'a

val asm : ('a, 'b, 'c) Analyses.ctx -> 'a

val skip : ('a, 'b, 'c) Analyses.ctx -> 'a

val event : ('a, 'b, 'c) Analyses.ctx -> 'd -> 'e -> 'a

val morphstate : 'a -> 'b -> 'b

val context : 'a -> 'b -> 'b

val name : unit -> string

module LD = ShapeDomain.Dom

module D : sig ... end

module C : sig ... end

module G : sig ... end

val tryReallyHard : 'a -> 'b -> 'c -> (LD.t -> 'd) -> LD.t -> 'd

val vars : Prelude.Ana.exp -> ShapeDomain.Var.t list

val re_context : 
  (D.t, G.t, C.t) Analyses.ctx ->
  Re.D.t ->
  (Re.D.t, Re.G.t, C.t) Analyses.ctx

val threadenter : 
  (D.t, G.t, C.t) Analyses.ctx ->
  'a ->
  'b ->
  'c ->
  (LD.t * [> `Lifted of Region.RegMap.t ]) list

val threadspawn : ('a, 'b, 'c) Analyses.ctx -> 'd -> 'e -> 'f -> 'g -> 'a

val sync_ld : 
  Queries.ask ->
  'a ->
  (CilType.Varinfo.t -> bool -> 'b) ->
  LD.t ->
  LD.t
  * (Cil.varinfo * bool) list
  * RegionDomain.RegMap.t
  * RegionDomain.RegPart.t

val reclaimLostRegions : 
  Usedef.VS.t ->
  ('a, bool * RegionDomain.RegPart.t, 'b) Analyses.ctx ->
  (Prelude.Ana.varinfo * 'c) ->
  RegionDomain.RS.t ->
  unit

val sync : (D.t, G.t, C.t) Analyses.ctx -> 'a -> D.t

val assign_ld : 
  Queries.ask ->
  (CilType.Varinfo.t -> bool) ->
  (CilType.Varinfo.t -> bool -> 'a) ->
  Prelude.Ana.lval ->
  Prelude.Ana.exp ->
  LD.t ->
  LD.t

val assign : 
  (D.t, G.t, C.t) Analyses.ctx ->
  Prelude.Ana.lval ->
  Prelude.Ana.exp ->
  D.t

val invariant : 
  'a ->
  (CilType.Varinfo.t -> bool) ->
  ShapeDomain.lexp ->
  ShapeDomain.lexp ->
  LD.t ->
  bool ->
  LD.t

val branch_ld : 
  'a ->
  (CilType.Varinfo.t -> bool) ->
  LD.t ->
  Prelude.Ana.exp ->
  bool ->
  LD.t

val branch : (D.t, G.t, C.t) Analyses.ctx -> Prelude.Ana.exp -> bool -> D.t

val body : (D.t, G.t, C.t) Analyses.ctx -> Prelude.Ana.fundec -> D.t

val return_ld : 
  Queries.ask ->
  'a ->
  (CilType.Varinfo.t -> bool -> 'b) ->
  LD.t ->
  Prelude.Ana.exp option ->
  Prelude.Ana.fundec ->
  LD.t

val return : 
  (D.t, G.t, C.t) Analyses.ctx ->
  Prelude.Ana.exp option ->
  Prelude.Ana.fundec ->
  D.t

val enter_func_ld : 
  Queries.ask ->
  (CilType.Varinfo.t -> bool) ->
  (CilType.Varinfo.t -> bool -> 'a) ->
  Prelude.Ana.lval option ->
  Prelude.Ana.fundec ->
  Prelude.Ana.exp list ->
  LD.t ->
  LD.t

val enter : 
  (D.t, G.t, C.t) Analyses.ctx ->
  Prelude.Ana.lval option ->
  Prelude.Ana.fundec ->
  Prelude.Ana.exp list ->
  ((LD.t * Re.D.t) * (LD.t * Re.D.t)) list

val combine : 
  'a ->
  Prelude.Ana.lval option ->
  'b ->
  Prelude.Ana.fundec ->
  Prelude.Ana.exp list ->
  'c ->
  D.t ->
  D.t

val special_fn_ld : 
  Queries.ask ->
  (CilType.Varinfo.t -> bool) ->
  (CilType.Varinfo.t -> bool -> 'a) ->
  Prelude.Ana.lval option ->
  Prelude.Ana.varinfo ->
  Prelude.Ana.exp list ->
  LD.t ->
  (LD.t * Prelude.Ana.exp * bool) list

val special : 
  (D.t, G.t, C.t) Analyses.ctx ->
  Prelude.Ana.lval option ->
  Prelude.Ana.varinfo ->
  Prelude.Ana.exp list ->
  D.t

val query : (D.t, G.t, C.t) Analyses.ctx -> 'a Queries.t -> 'a Queries.result

val startstate : 'a -> LD.t * [> `Lifted of Region.RegMap.t ]

val exitstate : 'a -> LD.t * [> `Lifted of Region.RegMap.t ]

val init : 'a -> unit

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Shapes/Spec/index.html

Module `Shapes.Spec`

package goblint

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Shapes/Spec/index.html

Module Shapes.Spec

Module `Shapes.Spec`