cil
  1. Overview
  2. Docs
package cil
Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

module S : SOLVER

Signature

type boolLat =
  1. | True
  2. | False
  3. | Top
  4. | Bottom
val combineBoolLat : boolLat -> boolLat -> boolLat
val d_bl : unit -> boolLat -> Pretty.doc
type funcSig = {
  1. mutable fsFormals : Cil.varinfo list;
  2. mutable fsReturn : Cil.varinfo option;
  3. mutable fsAllPreds : Cil.exp list;
  4. mutable fsFPPreds : Cil.exp list;
  5. mutable fsRetPreds : Cil.exp list;
}
type stmtState =
  1. | ILState of boolLat IH.t list
  2. | StmState of boolLat IH.t
type absState = stmtState IH.t
type context = {
  1. mutable cFuncSigs : funcSig IH.t;
  2. mutable cPredicates : Cil.exp IH.t;
  3. mutable cRPredMap : int ExpIntHash.t;
  4. 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 -> PredFlow.t option
class paVisitorClass : object ... end
val query : boolLat IH.t -> Cil.exp -> boolLat