Module BranchSet.Spec

Semi-interprocedural branch path-sensitivity (branchSet).

  1. Caller doesn't pass branches to callee.
  2. Callee passes branches to caller.
include module type of struct include CommonSpec end
include module type of struct include Analyses.IdentitySpec end
include module type of struct include Analyses.DefaultSpec end
module G = CommonSpec.G
module V = CommonSpec.V
type marshal = unit
val init : 'a -> unit
val finalize : unit -> unit
val vdecl : ('a, 'b, 'c, 'd) Analyses.man -> 'e -> 'a
val asm : ('a, 'b, 'c, 'd) Analyses.man -> 'a
val skip : ('a, 'b, 'c, 'd) Analyses.man -> 'a
val query : 'b -> 'a Queries.t -> 'a
val event : ('a, 'b, 'c, 'd) Analyses.man -> 'e -> 'f -> 'a
val morphstate : 'a -> 'b -> 'b
val sync : ('a, 'b, 'c, 'd) Analyses.man -> 'e -> 'a
val context : 'a -> 'b -> 'c -> 'c
val paths_as_set : ('a, 'b, 'c, 'd) Analyses.man -> 'a list
module A = CommonSpec.A
val access : 'a -> 'b -> unit
val assign : ('a, 'b, 'c, 'd) Analyses.man -> GoblintCil.lval -> GoblintCil.exp -> 'a
val body : ('a, 'b, 'c, 'd) Analyses.man -> GoblintCil.fundec -> 'a
val return : ('a, 'b, 'c, 'd) Analyses.man -> GoblintCil.exp option -> GoblintCil.fundec -> 'a
val combine_assign : ('a, 'b, 'c, 'd) Analyses.man -> GoblintCil.lval option -> 'e -> GoblintCil.fundec -> GoblintCil.exp list -> 'f -> 'g -> Queries.ask -> 'a
val special : ('a, 'b, 'c, 'd) Analyses.man -> GoblintCil.lval option -> GoblintCil.varinfo -> GoblintCil.exp list -> 'a
val threadspawn : ('a, 'b, 'c, 'd) Analyses.man -> multiple:'e -> 'f -> 'g -> 'h -> 'i -> 'a
module Branch = CommonSpec.Branch
module BranchSet = CommonSpec.BranchSet
module D = CommonSpec.D
include sig ... end
module C = CommonSpec.C
val startcontext : unit -> D.t
module P = CommonSpec.P
val branch : (BranchSet.t, 'a, 'b, 'c) Analyses.man -> GoblintCil.exp -> bool -> D.t
val startstate : 'a -> D.t
val threadenter : 'a -> multiple:'b -> 'c -> 'd -> 'e -> D.t list
val exitstate : 'a -> D.t
val name : unit -> string
val enter : (D.t, 'a, 'b, 'c) Analyses.man -> GoblintCil.lval option -> GoblintCil.fundec -> GoblintCil.exp list -> (D.t * D.t) list
val combine_env : (D.t, 'a, 'b, 'c) Analyses.man -> 'd -> 'e -> 'f -> 'g -> 'h -> D.t -> 'i -> D.t