copilot-sbv-0.5: A compiler for CoPilot targeting SBV.

Index

allocMetaTableCopilot.Compile.SBV.MetaTable
ArgCopilot.Compile.SBV.MetaTable
arrInputCopilot.Compile.SBV.Copilot2SBV
arrTypeCopilot.Compile.SBV.Copilot2SBV
BitsInst 
1 (Type/Class)Copilot.Compile.SBV.Witness
2 (Data Constructor)Copilot.Compile.SBV.Witness
bitsInstCopilot.Compile.SBV.Witness
BVDivisibleInst 
1 (Type/Class)Copilot.Compile.SBV.Witness
2 (Data Constructor)Copilot.Compile.SBV.Witness
c2ArgsCopilot.Compile.SBV.MetaTable
c2sExprCopilot.Compile.SBV.Copilot2SBV
CastInst 
1 (Type/Class)Copilot.Compile.SBV.Witness
2 (Data Constructor)Copilot.Compile.SBV.Witness
castInstCopilot.Compile.SBV.Witness
collectArgsCopilot.Compile.SBV.MetaTable
compileCopilot.Compile.SBV
compileWithSBVCopilot.Compile.SBV
defaultParamsCopilot.Compile.SBV.Params, Copilot.Compile.SBV
divInstCopilot.Compile.SBV.Witness
driverCopilot.Compile.SBV.Driver
driverNameCopilot.Compile.SBV.Driver
EqInst 
1 (Type/Class)Copilot.Compile.SBV.Witness
2 (Data Constructor)Copilot.Compile.SBV.Witness
eqInstCopilot.Compile.SBV.Witness
ExtCopilot.Compile.SBV.Copilot2SBV
extArrsCopilot.Compile.SBV.Copilot2SBV
ExternCopilot.Compile.SBV.MetaTable
ExternArrCopilot.Compile.SBV.MetaTable
ExternArrInfoMapCopilot.Compile.SBV.MetaTable
externArrInfoMapCopilot.Compile.SBV.MetaTable
ExternFunCopilot.Compile.SBV.MetaTable
ExternFunInfoMapCopilot.Compile.SBV.MetaTable
externFunInfoMapCopilot.Compile.SBV.MetaTable
ExternVarInfoMapCopilot.Compile.SBV.MetaTable
externVarInfoMapCopilot.Compile.SBV.MetaTable
extFunsCopilot.Compile.SBV.Copilot2SBV
ExtInput 
1 (Type/Class)Copilot.Compile.SBV.Copilot2SBV
2 (Data Constructor)Copilot.Compile.SBV.Copilot2SBV
extInputCopilot.Compile.SBV.Copilot2SBV
ExtQueCopilot.Compile.SBV.Copilot2SBV
extQuesCopilot.Compile.SBV.Copilot2SBV
extTypeCopilot.Compile.SBV.Copilot2SBV
extVarsCopilot.Compile.SBV.Copilot2SBV
fireTriggersCopilot.Compile.SBV.Code
getExtArrsCopilot.Compile.SBV.Code
getExtFunsCopilot.Compile.SBV.Code
guardArgsCopilot.Compile.SBV.MetaTable
HasSignAndSizeInst 
1 (Type/Class)Copilot.Compile.SBV.Witness
2 (Data Constructor)Copilot.Compile.SBV.Witness
hasSignAndSizeInstCopilot.Compile.SBV.Witness
Inputs 
1 (Type/Class)Copilot.Compile.SBV.Copilot2SBV
2 (Data Constructor)Copilot.Compile.SBV.Copilot2SBV
lookaheadCopilot.Compile.SBV.Queue
makefileCopilot.Compile.SBV.Makefile
makefileNameCopilot.Compile.SBV.Makefile
MergeableInst 
1 (Type/Class)Copilot.Compile.SBV.Witness
2 (Data Constructor)Copilot.Compile.SBV.Witness
mergeableInstCopilot.Compile.SBV.Witness
MetaTable 
1 (Type/Class)Copilot.Compile.SBV.MetaTable
2 (Data Constructor)Copilot.Compile.SBV.MetaTable
mkArgIdxCopilot.Compile.SBV.Common
mkExtArrFnCopilot.Compile.SBV.Common
mkExtFunArgFnCopilot.Compile.SBV.Common
mkExtTmpTagCopilot.Compile.SBV.Common
mkExtTmpVarCopilot.Compile.SBV.Common
mkObserverFnCopilot.Compile.SBV.Common
mkQueuePtrVarCopilot.Compile.SBV.Common
mkQueueVarCopilot.Compile.SBV.Common
mkTmpStVarCopilot.Compile.SBV.Common
mkTriggerArgFnCopilot.Compile.SBV.Common
mkTriggerGuardFnCopilot.Compile.SBV.Common
mkUpdateStFnCopilot.Compile.SBV.Common
NumInst 
1 (Type/Class)Copilot.Compile.SBV.Witness
2 (Data Constructor)Copilot.Compile.SBV.Witness
numInstCopilot.Compile.SBV.Witness
observerArgsCopilot.Compile.SBV.MetaTable
ObserverInfo 
1 (Type/Class)Copilot.Compile.SBV.MetaTable
2 (Data Constructor)Copilot.Compile.SBV.MetaTable
ObserverInfoMapCopilot.Compile.SBV.MetaTable
observerInfoMapCopilot.Compile.SBV.MetaTable
OrdInst 
1 (Type/Class)Copilot.Compile.SBV.Witness
2 (Data Constructor)Copilot.Compile.SBV.Witness
ordInstCopilot.Compile.SBV.Witness
Params 
1 (Type/Class)Copilot.Compile.SBV.Params, Copilot.Compile.SBV
2 (Data Constructor)Copilot.Compile.SBV.Params, Copilot.Compile.SBV
prefixCopilot.Compile.SBV.Params, Copilot.Compile.SBV
QueInput 
1 (Type/Class)Copilot.Compile.SBV.Copilot2SBV
2 (Data Constructor)Copilot.Compile.SBV.Copilot2SBV
quePtrCopilot.Compile.SBV.Copilot2SBV
Queue 
1 (Type/Class)Copilot.Compile.SBV.Queue
2 (Data Constructor)Copilot.Compile.SBV.Queue
3 (Data Constructor)Copilot.Compile.SBV.MetaTable
queue 
1 (Function)Copilot.Compile.SBV.Queue
2 (Function)Copilot.Compile.SBV.Copilot2SBV
QueueIn 
1 (Type/Class)Copilot.Compile.SBV.Copilot2SBV
2 (Data Constructor)Copilot.Compile.SBV.Copilot2SBV
QueueSizeCopilot.Compile.SBV.Queue
sbvCastCopilot.Compile.SBV.Witness
sbvDirNameCopilot.Compile.SBV
StreamInfoMapCopilot.Compile.SBV.MetaTable
streamInfoMapCopilot.Compile.SBV.MetaTable
SymWordInst 
1 (Type/Class)Copilot.Compile.SBV.Witness
2 (Data Constructor)Copilot.Compile.SBV.Witness
symWordInstCopilot.Compile.SBV.Witness
tagExtractCopilot.Compile.SBV.Common
triggerArgArgsCopilot.Compile.SBV.MetaTable
TriggerInfo 
1 (Type/Class)Copilot.Compile.SBV.MetaTable
2 (Data Constructor)Copilot.Compile.SBV.MetaTable
TriggerInfoMapCopilot.Compile.SBV.MetaTable
triggerInfoMapCopilot.Compile.SBV.MetaTable
updateObserversCopilot.Compile.SBV.Code
updateStatesCopilot.Compile.SBV.Code
withPrefixCopilot.Compile.SBV.Params, Copilot.Compile.SBV