Module `Constraints.WidenContextLifterSide`

Parameters

module S : Analyses.Spec

Signature

module DD : sig ... end

module M : sig ... end

module D : sig ... end

module G = S.G

module C = S.C

val name : unit -> string

type marshal = S.marshal

val init : S.marshal option -> unit

val finalize : unit -> S.marshal

val should_join : (S.D.t * 'a) -> (S.D.t * 'b) -> bool

val inj : ('a -> 'b) -> 'a -> 'b * M.t

val startstate : Cil.varinfo -> S.D.t * M.t

val exitstate : Cil.varinfo -> S.D.t * M.t

val morphstate : Cil.varinfo -> (S.D.t * 'a) -> S.D.t * 'a

val context : Cil.fundec -> (S.D.t * 'a) -> S.C.t

val call_descr : Cil.fundec -> S.C.t -> string

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

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

val sync : 
  (S.D.t * 'a, S.G.t, S.C.t) Analyses.ctx ->
  [ `Join | `Normal | `Return ] ->
  S.D.t * 'a

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

val assign : 
  (S.D.t * 'a, S.G.t, S.C.t) Analyses.ctx ->
  Cil.lval ->
  Cil.exp ->
  S.D.t * 'a

val vdecl : 
  (S.D.t * 'a, S.G.t, S.C.t) Analyses.ctx ->
  Cil.varinfo ->
  S.D.t * 'a

val branch : 
  (S.D.t * 'a, S.G.t, S.C.t) Analyses.ctx ->
  Cil.exp ->
  bool ->
  S.D.t * 'a

val body : (S.D.t * 'a, S.G.t, S.C.t) Analyses.ctx -> Cil.fundec -> S.D.t * 'a

val return : 
  (S.D.t * 'a, S.G.t, S.C.t) Analyses.ctx ->
  Cil.exp option ->
  Cil.fundec ->
  S.D.t * 'a

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

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

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

val special : 
  (S.D.t * 'a, S.G.t, S.C.t) Analyses.ctx ->
  Cil.lval option ->
  Cil.varinfo ->
  Cil.exp list ->
  S.D.t * 'a

val threadenter : 
  (S.D.t * 'a, S.G.t, S.C.t) Analyses.ctx ->
  Cil.lval option ->
  Cil.varinfo ->
  Cil.exp list ->
  (S.D.t * 'a) list

val threadspawn : 
  (S.D.t * 'a, S.G.t, S.C.t) Analyses.ctx ->
  Cil.lval option ->
  Cil.varinfo ->
  Cil.exp list ->
  (S.D.t * 'b, S.G.t, S.C.t) Analyses.ctx ->
  S.D.t * 'a

val enter : 
  (S.D.t * M.t, S.G.t, S.C.t) Analyses.ctx ->
  Cil.lval option ->
  CilType.Fundec.t ->
  Cil.exp list ->
  ((S.D.t * M.t) * (S.D.t * M.t)) list

val combine : 
  (S.D.t * 'a, S.G.t, S.C.t) Analyses.ctx ->
  Cil.lval option ->
  Cil.exp ->
  Cil.fundec ->
  Cil.exp list ->
  S.C.t ->
  (S.D.t * 'b) ->
  S.D.t * 'a

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Constraints/WidenContextLifterSide/index.html

Module `Constraints.WidenContextLifterSide`

Parameters

Signature

package goblint

Install

Dune Dependency

Authors

Maintainers

Sources

doc/goblint.lib/Constraints/WidenContextLifterSide/index.html

Module Constraints.WidenContextLifterSide

Parameters

Signature

Module `Constraints.WidenContextLifterSide`