WidenContextLifterSide (p.goblint.1.1.1.doc.goblint.lib.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