MakeSpec (p.goblint.1.1.1.doc.goblint.lib.MutexAnalysis.MakeSpec)

Parameters

module P : SpecParam

Signature

include module type of struct include Analyses.DefaultSpec end

type marshal = unit

val finalize : unit -> unit

val call_descr : Cil.fundec -> 'a -> string

val intrpt : ('a, 'b, 'c) Analyses.ctx -> 'a

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

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

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

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

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

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

val context : 'a -> 'b -> 'b

val name : unit -> string

name for the analysis (btw, it's "Only Mutex Must")

module D = Lockset

Add current lockset alongside to the base analysis domain. Global data is collected using dirty side-effecting.

module C = Lockset

module G = P.G

We do not add global state, so just lift from BS

val should_join : D.t -> D.t -> bool

val conv_offset : 
  ([< `Field of 'b * 'a | `Index of Prelude.Ana.exp * 'a | `NoOffset ] as 'a) ->
  [> `Field of 'b * 'c | `Index of ValueDomain.IndexDomain.t * 'c | `NoOffset ] as 'c

val conv_offset_inv : 
  ([< `Field of 'b * 'a | `Index of 'c * 'a | `NoOffset ] as 'a) ->
  [> `Field of 'b * 'd | `Index of Cil.exp * 'd | `NoOffset ] as 'd

val conv_const_offset : 
  Prelude.Ana.offset ->
  [> `Field of Prelude.Ana.fieldinfo * 'a
  | `Index of ValueDomain.IndexDomain.t * 'a
  | `NoOffset ] as 'a

val replace_elem : 
  ('a
   * ([< `Field of 'c * 'b | `Index of Prelude.Ana.exp * 'b | `NoOffset ] as 'b)) ->
  Basetype.CilExp.t ->
  Prelude.Ana.exp ->
  'a
  * ([> `Field of 'c * 'd
     | `Index of ValueDomain.IndexDomain.t * 'd
     | `NoOffset ] as 'd)

val part_access : 
  (Lockset.ReverseAddrSet.t, 'a, 'b) Analyses.ctx ->
  'c ->
  'd ->
  bool ->
  Access.LSSSet.t * Access.LSSet.t

val eval_exp_addr : Queries.ask -> Cil.exp -> ValueDomain.Addr.t list

val lock : 
  (Lockset.ReverseAddrSet.t, 'a, 'b) Analyses.ctx ->
  Lockset.RW.t ->
  bool ->
  bool ->
  Queries.ask ->
  Prelude.Ana.lval option ->
  Cil.exp list ->
  Lockset.ReverseAddrSet.t ->
  Lockset.ReverseAddrSet.t

val arinc_analysis_activated : bool Prelude.Ana.ref

val do_access : 
  (D.t, G.t, C.t) Analyses.ctx ->
  bool ->
  bool ->
  int ->
  Prelude.Ana.exp ->
  unit

val access_one_top : 
  ?force:bool ->
  (D.t, G.t, C.t) Analyses.ctx ->
  bool ->
  bool ->
  Prelude.Ana.exp ->
  unit

val startstate : 'a -> Lockset.ReverseAddrSet.t

We just lift start state, global and dependency functions:

val threadenter : 'a -> 'b -> 'c -> 'd -> Lockset.ReverseAddrSet.t list

val exitstate : 'a -> Lockset.ReverseAddrSet.t

val query : 
  (Lockset.ReverseAddrSet.t, G.t, 'b) Analyses.ctx ->
  'a Queries.t ->
  'a Queries.result

Transfer functions:

val assign : 
  (D.t, G.t, C.t) Analyses.ctx ->
  Prelude.Ana.lval ->
  Prelude.Ana.exp ->
  D.t

val branch : (D.t, G.t, C.t) Analyses.ctx -> Prelude.Ana.exp -> 'a -> D.t

val return : 
  (D.t, G.t, C.t) Analyses.ctx ->
  Prelude.Ana.exp option ->
  Prelude.Ana.fundec ->
  D.t

val body : 
  (Lockset.ReverseAddrSet.t, 'a, 'b) Analyses.ctx ->
  Prelude.Ana.fundec ->
  D.t

val special : 
  (D.t, G.t, C.t) Analyses.ctx ->
  Prelude.Ana.lval option ->
  Prelude.Ana.varinfo ->
  Prelude.Ana.exp list ->
  D.t

val enter : (D.t, 'a, 'b) Analyses.ctx -> 'c -> 'd -> 'e -> (D.t * D.t) list

val combine : 
  (D.t, G.t, C.t) Analyses.ctx ->
  Prelude.Ana.lval option ->
  Prelude.Ana.exp ->
  'a ->
  Prelude.Ana.exp list ->
  'b ->
  'c ->
  'c

val threadspawn : 
  (D.t, G.t, C.t) Analyses.ctx ->
  Prelude.Ana.lval option ->
  'a ->
  'b ->
  'c ->
  D.t

val init : 'a -> unit