Spec (goblint.Goblint_lib.C2poAnalysis.Spec)

include module type of struct include Analyses.DefaultSpec end

include module type of struct include Analyses.IdentitySpec end

include module type of struct include Analyses.DefaultSpec end

module G = Lattice.Unit

module V = Analyses.EmptyV

module P = Analyses.EmptyP

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 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 = Analyses.UnitA

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

module D = C2poDomain.D

module C = D

val name : unit -> string

val startcontext : unit -> [> `Lifted of CongruenceClosure.t ]

val reachable_from_args : 
  ('a, 'b, 'c, 'd) Analyses.man ->
  GoblintCil.exp list ->
  GoblintCil.varinfo list

Find reachable variables in a function

val eval_guard : 
  Queries.ask ->
  CongruenceClosure.t ->
  GoblintCil.Cil.exp ->
  GoblintCil.Cil.ikind ->
  [> `Lifted of ValueDomainQueries.ID.I.t | `Top ]

val conj_to_invariant : 
  'a ->
  Goblint_lib__UnionFind.prop list ->
  [ `Bot | `Lifted of Invariant.ExpLat.t | `Top ]

Convert a conjunction to an invariant.

val query : 
  ([< `Bot | `Lifted of CongruenceClosure.t ], 'b, 'c, 'd) Analyses.man ->
  'a Queries.t ->
  'a Queries.result

val assign_term : 
  CongruenceClosure.t ->
  Queries.ask ->
  UnionFind.T.t ->
  (UnionFind.T.t option * Z.t option) ->
  GoblintCil.Cil.typ ->
  CongruenceClosure.t

Assign the right hand side rhs (that is already converted to a C-2PO term) to the term `lterm`.

val assign_lval : 
  CongruenceClosure.t ->
  Queries.ask ->
  GoblintCil.lval ->
  (UnionFind.T.t option * Z.t option) ->
  CongruenceClosure.t

Assign Cil Lval to a right hand side that is already converted to C-2PO terms.

val assign : 
  ([< `Bot | `Lifted of CongruenceClosure.t ], 'a, 'b, 'c) Analyses.man ->
  GoblintCil.lval ->
  GoblintCil.exp ->
  [> `Bot | `Lifted of CongruenceClosure.t ]

val branch : 
  ([< `Bot | `Lifted of CongruenceClosure.t ], 'a, 'b, 'c) Analyses.man ->
  GoblintCil.Cil.exp ->
  bool ->
  [> `Bot | `Lifted of CongruenceClosure.t ]

val body : ('a, 'b, 'c, 'd) Analyses.man -> 'e -> 'a

val assign_return : 
  Queries.ask ->
  CongruenceClosure.t ->
  CongruenceClosure.term ->
  GoblintCil.exp ->
  CongruenceClosure.t

val return : 
  ([ `Bot | `Lifted of CongruenceClosure.t ], 'a, 'b, 'c) Analyses.man ->
  GoblintCil.exp option ->
  'd ->
  [ `Bot | `Lifted of CongruenceClosure.t ]

val special : 
  ([ `Bot | `Lifted of CongruenceClosure.t ], 'a, 'b, 'c) Analyses.man ->
  GoblintCil.lval option ->
  GoblintCil.Cil.varinfo ->
  LibraryDesc.Cil.Cil.exp list ->
  [ `Bot | `Lifted of CongruenceClosure.t ]

var_opt is the variable we assign to. It has type lval. v=malloc.

val enter : 
  ([< `Bot | `Lifted of CongruenceClosure.t & CongruenceClosure.t Bot ] as 'a,
    'b,
    'c,
    'd)
    Analyses.man ->
  GoblintCil.lval option ->
  GoblintCil.fundec ->
  GoblintCil.exp list ->
  ('a * [> `Bot | `Lifted of CongruenceClosure.t ]) list

First all local variables of the function are duplicated, then we remember the value of each local variable at the beginning of the function by using the analysis startState. This way we can infer the relations between the local variables of the caller and the pointers that were modified by the function.

val remove_out_of_scope_vars : 
  CongruenceClosure.data ->
  GoblintCil.fundec ->
  CongruenceClosure.data

val combine_env : 
  ([< `Bot | `Lifted of CongruenceClosure.t & CongruenceClosure.t ],
    'a,
    'b,
    'c)
    Analyses.man ->
  GoblintCil.lval option ->
  'd ->
  GoblintCil.fundec ->
  GoblintCil.exp list ->
  'e ->
  [< `Bot | `Lifted of CongruenceClosure.t & CongruenceClosure.t ] ->
  Queries.ask ->
  [> `Bot | `Lifted of CongruenceClosure.t ]

val combine_assign : 
  ([< `Bot | `Lifted of CongruenceClosure.t ], 'a, 'b, 'c) Analyses.man ->
  GoblintCil.lval option ->
  'd ->
  'e ->
  'f ->
  'g ->
  'h ->
  Queries.ask ->
  [> `Bot | `Lifted of CongruenceClosure.t ]

val startstate : 'a -> [> `Lifted of CongruenceClosure.t ]

val threadenter : 
  'a ->
  multiple:'b ->
  'c ->
  'd ->
  'e ->
  [> `Lifted of CongruenceClosure.t ] list

val threadspawn : 
  'a ->
  multiple:'b ->
  'c ->
  'd ->
  'e ->
  'f ->
  [> `Lifted of CongruenceClosure.t ]

val exitstate : 'a -> [> `Lifted of CongruenceClosure.t ]