SpecFunctor (goblint.Goblint_lib.RelationAnalysis.SpecFunctor)

Parameters

module Priv : RelationPriv.S

module RD : RelationDomain.RD

module PCU : RelationPrecCompareUtil.Util

Signature

include module type of struct include Analyses.DefaultSpec end

Relatively safe default implementations of some boring Spec functions.

type marshal = unit

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

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

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

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

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

module A = Analyses.UnitA

val access : 'a -> 'b -> unit

module Priv : sig ... end

module D : sig ... end

module G = Priv.G

include sig ... end

module C : sig ... end

val startcontext : unit -> D.t

module V : sig ... end

module P : sig ... end

module RV = RD.V

module PCU : sig ... end

val results : RD.t PCU.RH.t

val context : 'a -> GoblintCil.fundec -> D.t -> D.t

val exitstate : 'a -> (RD.t, Priv.D.t) RelationDomain.relcomponents_t

val startstate : 'a -> (RD.t, Priv.D.t) RelationDomain.relcomponents_t

val read_global : 
  Queries.ask ->
  (Priv.V.t -> Priv.G.t) ->
  RelationDomain.RelComponents(RD)(Priv.D).t ->
  GoblintCil.varinfo ->
  GoblintCil.varinfo ->
  RD.t

module VH : sig ... end

val read_globals_to_locals : 
  Queries.ask ->
  (Priv.V.t -> Priv.G.t) ->
  (RD.t, Priv.D.t) RelationDomain.relcomponents_t ->
  GoblintCil.exp ->
  RD.t * GoblintCil.exp * GoblintCil.varinfo VH.t

val read_globals_to_locals_inv : 
  Queries.ask ->
  (Priv.V.t -> Priv.G.t) ->
  (RD.t, Priv.D.t) RelationDomain.relcomponents_t ->
  GoblintCil.varinfo list ->
  RD.t * (GoblintCil.exp -> GoblintCil.exp) * GoblintCil.varinfo VH.t

val read_from_globals_wrapper : 
  Queries.ask ->
  (Priv.V.t -> Priv.G.t) ->
  (RD.t, Priv.D.t) RelationDomain.relcomponents_t ->
  GoblintCil.exp ->
  (RD.t -> GoblintCil.exp -> 'a) ->
  'b

val assign_from_globals_wrapper : 
  Queries.ask ->
  (Priv.V.t -> Priv.G.t) ->
  (RD.t, Priv.D.t) RelationDomain.relcomponents_t ->
  GoblintCil.exp ->
  (RD.t -> GoblintCil.exp -> RD.t) ->
  RD.t

val write_global : 
  Queries.ask ->
  (Priv.V.t -> Priv.G.t) ->
  (Priv.V.t -> Priv.G.t -> unit) ->
  RelationDomain.RelComponents(RD)(Priv.D).t ->
  GoblintCil.varinfo ->
  GoblintCil.varinfo ->
  RelationDomain.RelComponents(RD)(Priv.D).t

val assign_to_global_wrapper : 
  Queries.ask ->
  (Priv.V.t -> Priv.G.t) ->
  (Priv.V.t -> Priv.G.t -> unit) ->
  (RD.t, Priv.D.t) RelationDomain.relcomponents_t ->
  GoblintCil.lval ->
  ((RD.t, Priv.D.t) RelationDomain.relcomponents_t ->
    GoblintCil.varinfo ->
    RD.t) ->
  (RD.t, Priv.D.t) RelationDomain.relcomponents_t

An extended overflow handling inside relationAnalysis for expression assignments when overflows are assumed to occur. Since affine equalities can only keep track of integer bounds of expressions evaluating to definite constants, we now query the integer bounds information for expressions from other analysis. If an analysis returns bounds that are unequal to min and max of ikind , we can exclude the possibility that an overflow occurs and the abstract effect of the expression assignment can be used, i.e. we do not have to set the variable's value to top.

val no_overflow : Queries.ask -> GoblintCil.exp -> bool lazy_t

val assert_type_bounds : Queries.ask -> RD.t -> GoblintCil.varinfo -> RD.t

val replace_deref_exps : 
  (ValueDomain.AD.t Queries.t -> ValueDomain.AD.t) ->
  GoblintCil.exp ->
  GoblintCil.exp

val assign : 
  ((RD.t, Priv.D.t) RelationDomain.relcomponents_t, Priv.G.t, 'a, Priv.V.t)
    Analyses.ctx ->
  GoblintCil.lval ->
  GoblintCil.exp ->
  (RD.t, Priv.D.t) RelationDomain.relcomponents_t

val branch : 
  ((RD.t, Priv.D.t) RelationDomain.relcomponents_t, Priv.G.t, 'a, Priv.V.t)
    Analyses.ctx ->
  GoblintCil.exp ->
  bool ->
  (RD.t, Priv.D.t) RelationDomain.relcomponents_t

val any_local_reachable : GoblintCil.fundec -> VS.t -> bool

val reachable_from_args : 
  ('a, 'b, 'c, 'd) Analyses.ctx ->
  GoblintCil.exp list ->
  VS.t

val pass_to_callee : GoblintCil.fundec -> bool -> GobApron.Var.t -> bool

val make_callee_rel : 
  thread:bool ->
  ((RD.t, Priv.D.t) RelationDomain.relcomponents_t, Priv.G.t, 'a, Priv.V.t)
    Analyses.ctx ->
  GoblintCil.fundec ->
  GoblintCil.exp list ->
  RD.t

val enter : 
  ((RD.t, Priv.D.t) RelationDomain.relcomponents_t, Priv.G.t, 'a, Priv.V.t)
    Analyses.ctx ->
  'b ->
  GoblintCil.fundec ->
  GoblintCil.exp list ->
  ((RD.t, Priv.D.t) RelationDomain.relcomponents_t
   * (RD.t, Priv.D.t) RelationDomain.relcomponents_t)
    list

val body : 
  ((RD.t, 'a) RelationDomain.relcomponents_t, 'b, 'c, 'd) Analyses.ctx ->
  GoblintCil.fundec ->
  (RD.t, 'e) RelationDomain.relcomponents_t

val return : 
  ((RD.t, Priv.D.t) RelationDomain.relcomponents_t, Priv.G.t, 'a, Priv.V.t)
    Analyses.ctx ->
  GoblintCil.exp option ->
  GoblintCil.fundec ->
  RelationDomain.RelComponents(RD)(Priv.D).t

val combine_env : 
  (D.t, Priv.G.t, 'a, Priv.V.t) Analyses.ctx ->
  'b ->
  'c ->
  GoblintCil.fundec ->
  GoblintCil.exp list ->
  'd ->
  D.t ->
  Queries.ask ->
  (RD.t, Priv.D.t) RelationDomain.relcomponents_t

val combine_assign : 
  ((RD.t, Priv.D.t) RelationDomain.relcomponents_t, Priv.G.t, 'a, Priv.V.t)
    Analyses.ctx ->
  GoblintCil.lval option ->
  'b ->
  GoblintCil.fundec ->
  'c ->
  'd ->
  'e ->
  Queries.ask ->
  (RD.t, Priv.D.t) RelationDomain.relcomponents_t

val invalidate_one : 
  Queries.ask ->
  ('a, Priv.G.t, 'b, Priv.V.t) Analyses.ctx ->
  (RD.t, Priv.D.t) RelationDomain.relcomponents_t ->
  GoblintCil.lval ->
  (RD.t, Priv.D.t) RelationDomain.relcomponents_t

val reachables : Queries.ask -> GoblintCil.exp list -> ValueDomain.AD.t option

val forget_reachable : 
  ('a, Priv.G.t, 'b, Priv.V.t) Analyses.ctx ->
  (RD.t, Priv.D.t) RelationDomain.relcomponents_t ->
  GoblintCil.exp list ->
  (RD.t, Priv.D.t) RelationDomain.relcomponents_t

val assert_fn : 
  ((RD.t, Priv.D.t) RelationDomain.relcomponents_t, Priv.G.t, 'a, Priv.V.t)
    Analyses.ctx ->
  GoblintCil.exp ->
  bool ->
  (RD.t, Priv.D.t) RelationDomain.relcomponents_t

val special : 
  ((RD.t, Priv.D.t) RelationDomain.relcomponents_t, Priv.G.t, 'a, Priv.V.t)
    Analyses.ctx ->
  GoblintCil.lval option ->
  GoblintCil.Cil.varinfo ->
  LibraryDesc.Cil.Cil.exp list ->
  (RD.t, Priv.D.t) RelationDomain.relcomponents_t

val query_invariant : 
  (RelationDomain.RelComponents(RD)(Priv.D).t, Priv.G.t, 'a, Priv.V.t)
    Analyses.ctx ->
  'b ->
  [ `Bot | `Lifted of Invariant.ExpLat.t | `Top ]

val query : 
  ((RD.t, Priv.D.t) RelationDomain.relcomponents_t, Priv.G.t, 'b, Priv.V.t)
    Analyses.ctx ->
  'a Queries.t ->
  'a0 Queries.result

val threadenter : 
  (RelationDomain.RelComponents(RD)(Priv.D).t, Priv.G.t, 'a, Priv.V.t)
    Analyses.ctx ->
  multiple:'b ->
  'c ->
  Cilfacade.VarinfoH.key ->
  GoblintCil.exp list ->
  (RD.t, Priv.D.t) RelationDomain.relcomponents_t list

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

val event : 
  (RelationDomain.RelComponents(RD)(Priv.D).t, Priv.G.t, 'a, Priv.V.t)
    Analyses.ctx ->
  Events.t ->
  'b ->
  RelationDomain.RelComponents(RD)(Priv.D).t

val sync : 
  ((RD.t, Priv.D.t) RelationDomain.relcomponents_t, Priv.G.t, 'a, Priv.V.t)
    Analyses.ctx ->
  [< `Init
  | `Join
  | `JoinCall of CilType.Fundec.t
  | `Normal
  | `Return
  | `Thread ] ->
  RelationDomain.RelComponents(RD)(Priv.D).t

val init : 'a -> unit

val store_data : Fpath.t -> unit

val finalize : unit -> unit