package goblint

  1. Overview
  2. Docs
package goblint
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module SingleThreadedLifter.SingleThreadedLifter

Parameters

Signature

include module type of struct include S end
include Analyses.Spec
module D = S.D
module G = S.G
module C = S.C
module V = S.V

Global constraint variables.

module P = S.P

Global constraint variables.

val name : unit -> string
type marshal = S.marshal

Auxiliary data (outside of solution domains) that needs to be marshaled and unmarshaled. This includes: * hashtables, * varinfos (create_var), * RichVarinfos.

val init : marshal option -> unit

Initialize using unmarshaled auxiliary data (if present).

val finalize : unit -> marshal

Finalize and return auxiliary data to be marshaled.

val startstate : GoblintCil.varinfo -> D.t
val morphstate : GoblintCil.varinfo -> D.t -> D.t
val exitstate : GoblintCil.varinfo -> D.t
val context : (D.t, G.t, C.t, V.t) Analyses.man -> GoblintCil.fundec -> D.t -> C.t
val startcontext : unit -> C.t
val sync : (D.t, G.t, C.t, V.t) Analyses.man -> [ `Normal | `Join | `JoinCall of CilType.Fundec.t | `Return ] -> D.t

A transfer function used for declaring local variables. By default only for variable-length arrays (VLAs).

val asm : (D.t, G.t, C.t, V.t) Analyses.man -> D.t

A transfer function meant to handle inline assembler program points

val skip : (D.t, G.t, C.t, V.t) Analyses.man -> D.t

A transfer function which works as the identity function, i.e., it skips and does nothing. Used for empty loops.

val paths_as_set : (D.t, G.t, C.t, V.t) Analyses.man -> D.t list
val event : (D.t, G.t, C.t, V.t) Analyses.man -> Events.t -> (D.t, G.t, C.t, V.t) Analyses.man -> D.t
module A = S.A
val access : (D.t, G.t, C.t, V.t) Analyses.man -> Queries.access -> A.t
val is_multithreaded : Queries.ask -> bool
val query : (D.t, G.t, C.t, V.t) Analyses.man -> 'a Queries.t -> 'a
val branch : (D.t, G.t, C.t, V.t) Analyses.man -> GoblintCil.exp -> bool -> D.t
val body : (D.t, G.t, C.t, V.t) Analyses.man -> GoblintCil.fundec -> D.t
val return : (D.t, G.t, C.t, V.t) Analyses.man -> GoblintCil.exp option -> GoblintCil.fundec -> D.t
val special : (D.t, G.t, C.t, V.t) Analyses.man -> GoblintCil.lval option -> GoblintCil.varinfo -> GoblintCil.exp list -> D.t
val enter : (D.t, G.t, C.t, V.t) Analyses.man -> GoblintCil.lval option -> GoblintCil.fundec -> GoblintCil.exp list -> (D.t * D.t) list
val combine_env : (D.t, G.t, C.t, V.t) Analyses.man -> GoblintCil.lval option -> GoblintCil.exp -> GoblintCil.fundec -> GoblintCil.exp list -> C.t option -> D.t -> Queries.ask -> D.t
val combine_assign : (D.t, G.t, C.t, V.t) Analyses.man -> GoblintCil.lval option -> GoblintCil.exp -> GoblintCil.fundec -> GoblintCil.exp list -> C.t option -> D.t -> Queries.ask -> D.t
val threadenter : 'a -> multiple:'b -> 'c -> 'd -> 'e -> D.t list
val threadspawn : 'a -> multiple:'b -> 'c -> 'd -> 'e -> 'f -> D.t