cil 1.7.3 (latest) · OCaml Package

Parameters

module S : SOLVER

Signature

type boolLat =

| True
| False
| Top
| Bottom

val combineBoolLat : boolLat -> boolLat -> boolLat

val d_bl : unit -> boolLat -> Pretty.doc

type funcSig = {

mutable fsFormals : Cil.varinfo list;
mutable fsReturn : Cil.varinfo option;
mutable fsAllPreds : Cil.exp list;
mutable fsFPPreds : Cil.exp list;
mutable fsRetPreds : Cil.exp list;

}

type stmtState =

| ILState of boolLat IH.t list
| StmState of boolLat IH.t

type absState = stmtState IH.t

type context = {

mutable cFuncSigs : funcSig IH.t;
mutable cPredicates : Cil.exp IH.t;
mutable cRPredMap : int ExpIntHash.t;
mutable cNextPred : int;

}

val emptyContext : unit -> context

class returnFinderClass : Cil.varinfo option Pervasives.ref -> object ... end

val findReturn : Cil.fundec -> Cil.varinfo option

class viFinderClass : Cil.varinfo -> bool Pervasives.ref -> object ... end

val expContainsVi : Cil.exp -> Cil.varinfo -> bool

class derefFinderClass : 'a -> bool Pervasives.ref -> object ... end

val expContainsDeref : Cil.exp -> 'a -> bool

class globalFinderClass : bool Pervasives.ref -> object ... end

val expContainsGlobal : Cil.exp -> bool

class aliasFinderClass : Cil.exp -> bool Pervasives.ref -> object ... end

val expHasAlias : Cil.exp -> Cil.exp -> bool

val makeFormalPreds : Cil.varinfo list -> Cil.exp list -> Cil.exp list

val makeReturnPreds : 
  Cil.varinfo option ->
  Cil.varinfo list ->
  Cil.varinfo list ->
  Cil.exp list ->
  Cil.exp list ->
  Cil.exp list

val funSigHash : funcSig IH.t

class funcSigMakerClass : object ... end

val makeFunctionSigs : Cil.file -> funcSig IH.t

val h_equals : 'a IH.t -> 'a IH.t -> bool

val hl_equals : 'a IH.t list -> 'a IH.t list -> bool

val h_combine : boolLat IH.t -> boolLat IH.t -> boolLat IH.t

val hl_combine : boolLat IH.t list -> boolLat IH.t list -> boolLat IH.t list

val substitute : Cil.exp -> Cil.lval -> Cil.exp -> Cil.exp

val weakestPrecondition : Cil.instr -> Cil.exp -> Cil.exp option

val getPred : context -> int -> Cil.exp

val buildPreAndTest : 
  context ->
  boolLat IH.t ->
  boolLat IH.t ->
  Cil.exp list ->
  bool ->
  Cil.instr option ->
  boolLat IH.t

val handleSetInstr : 
  context ->
  Cil.exp list ->
  boolLat IH.t ->
  Cil.instr ->
  boolLat IH.t ->
  boolLat IH.t

val handleCallInstr : 
  context ->
  Cil.exp list ->
  boolLat IH.t ->
  Cil.instr ->
  boolLat IH.t ->
  boolLat IH.t

val fixForExternCall : 
  context ->
  boolLat IH.t ->
  Cil.lval option ->
  Cil.exp list ->
  boolLat IH.t

val handleIl : context -> Cil.instr list -> stmtState -> stmtState

val handleStmt : context -> Cil.stmt -> stmtState -> stmtState

val handleBranch : context -> Cil.exp -> stmtState -> stmtState

val listInit : int -> 'a -> 'a list

val currentContext : context

module PredFlow : sig ... end

module PA : sig ... end

val registerFile : Cil.file -> unit

val makePreds : Cil.exp list -> unit

val makeAllBottom : Cil.exp IH.t -> boolLat IH.t

val analyze : Cil.fundec -> unit

val getPAs : int -> stmtState option

class paVisitorClass : object ... end

val query : boolLat IH.t -> Cil.exp -> boolLat

package cil

Parameters

Signature