This library exposes the following toplevel modules:
BCHAnalysisTypes BCHAnalyzeApp BCHAnalyzeProcedure BCHExtractInvariants BCHFileIO BCHInterrupt BCHNumericalConstraints BCHReachingDefs BCHSaveExports BCHTrace This library exposes the following toplevel modules:
This library exposes the following toplevel modules:
BCHARMFunctionInterface BCHBCAttributes BCHBCDictionary BCHBCFiles BCHBCFunDeclarations BCHBCSumTypeSerializer BCHBCTypePretty BCHBCTypeTransformer BCHBCTypeUtil Utility functions to construct, destruct, or examine c-like types.BCHBCTypeXml BCHBCTypes BCHBCWriteXml BCHBTerm BCHBasicTypes BCHByteUtilities Utility functions to read and write binary dataBCHCPURegisters Encapsulation of architecture-specific registers into a generic register typeBCHCStruct BCHCStructConstant BCHCallSemanticsRecorder BCHCallTarget BCHCallTargetInfo Implementation of call_target_info_int class type.BCHCallbackTables BCHCallgraph BCHCodegraph BCHConstantDefinitions Storage for externally defined named constants, addresses, and flag constantsBCHCppClass BCHDataBlock BCHDataExportSpec BCHDemangler BCHDictionary BCHDisassemblySummary BCHDoubleword BCHExternalPredicate BCHFloc The principal access point for commands on and analysis results of an assembly instruction.BCHFtsParameter Function-type-signature parameterBCHFunctionData BCHFunctionInfo The principal access point for analysis results for an assembly function.BCHFunctionInterface The externally provided or internally inferred function api of an assembly function.BCHFunctionSemantics BCHFunctionStackframe BCHFunctionStub BCHFunctionSummary Function summary containing signature, semantics, and documentation.BCHFunctionSummaryLibrary BCHGlobalState BCHImmediate A constant value with a given size in bytes and signedness.BCHInterfaceDictionary BCHInvDictionary BCHJavaBasicTypes BCHJavaSignatures BCHJni BCHJumpTable BCHLibTypes Principal type definitions for bchlib.BCHLocation Creates and manipulates locations in assembly functions.BCHLocationInvariant BCHLocationVarInvariant BCHMIPSFunctionInterface BCHMakeCallTargetInfo Utility functions to create call targets for individual call sites.BCHMemoryRecorder BCHMemoryReference BCHMetrics BCHMetricsHandler BCHPostcondition BCHPreFileIO BCHPrecondition Function precondition on the function interfaceBCHProofObligations BCHSectionHeadersInfo BCHSideeffect BCHSpecializations BCHStreamWrapper Utility to wrap file/string input for big or little-endianBCHStrings BCHStructTables BCHSumTypeSerializer BCHSystemData BCHSystemInfo BCHSystemSettings BCHTypeConstraintDictionary BCHTypeConstraintGraph BCHTypeConstraintStore System-wide collection of type constraints.BCHTypeConstraintUtil Utilies for creating type constraints.BCHTypeDefinitions BCHUserProvidedDirections BCHUtilities BCHVarDictionary BCHVarInvDictionary BCHVariable BCHVariableNames BCHVersion BCHXPODictionary BCHXPOPredicate BCHXprUtil This library exposes the following toplevel modules:
BCHARMAnalysisResults BCHARMAssemblyBlock BCHARMAssemblyFunction BCHARMAssemblyFunctions Provides the access point to retrieve assembly functions.BCHARMAssemblyInstruction BCHARMAssemblyInstructions Holds an array of all of the assembly instructions, made available through a class instance reference.BCHARMCHIFSystem BCHARMCallSitesRecords BCHARMCodePC BCHARMConditionalExpr BCHARMDictionary BCHARMDisassemblyUtils BCHARMInstructionAggregate Sequence of consecutive assembly instructions that represents a semantic unit.BCHARMJumptable Facility to identify and construct jump tables for TBB/TBH, LDR, and BXBCHARMLoopStructure BCHARMMetrics BCHARMOpcodeRecords BCHARMOperand BCHARMPseudocode BCHARMSumTypeSerializer BCHARMTestSupport BCHARMTypes Principal type definitions for bchlibarm32.BCHConstructARMFunction BCHDisassembleARM BCHDisassembleARMInstruction BCHDisassembleARMStream Facility to disassemble a stream of bytes into arm or Thumb instructions.BCHDisassembleThumbInstruction BCHFnARMDictionary BCHFnARMTypeConstraints Generation of type constraints from assembly instructions.BCHLoadStoreMultipleSequence Facility to identify and construct idiomatic constructs with LDM/STM.BCHThumbITSequence Facility to identify and construct Thumb idiomatic constructs with IT.BCHTranslateARMToCHIF This library exposes the following toplevel modules:
BCHDwarf BCHDwarfOperationRecords BCHDwarfQueryService BCHDwarfTypes BCHDwarfUtils BCHELFDebugARangesSection BCHELFDebugAbbrevSection BCHELFDebugInfoSection BCHELFDebugLocSection BCHELFDebugStrSection BCHELFDictionary BCHELFDynamicSegment BCHELFDynamicTable BCHELFHeader BCHELFPrettyStrings BCHELFProgramHeader BCHELFProgramSection BCHELFRelocationTable BCHELFSection BCHELFSectionHeader BCHELFSectionHeaderCreator BCHELFSegment BCHELFStringTable BCHELFSymbolTable BCHELFTypes BCHELFUtil This library exposes the following toplevel modules:
BCHAssembleMIPSInstruction Assembles a MIPS assembly instruction into a doubleword.BCHDisassembleMIPS BCHDisassembleMIPSInstruction Disassembles a doubleword into a MIPS assembly instruction.BCHFnMIPSDictionary BCHMIPSAnalysisResults BCHMIPSAssemblyBlock BCHMIPSAssemblyFunction BCHMIPSAssemblyFunctions BCHMIPSAssemblyInstruction BCHMIPSAssemblyInstructions Holds an array of all of the assembly instructions, made available through a class instance reference.BCHMIPSCHIFSystem BCHMIPSCodePC BCHMIPSDictionary Provides the global dictionary for opcodes and related types.BCHMIPSDisassemblyUtils BCHMIPSLoopStructure BCHMIPSMetrics BCHMIPSOpcodeRecords BCHMIPSOperand The implementation of the assembly instruction operand type.BCHMIPSSumTypeSerializer BCHMIPSTypes BCHTranslateMIPSToCHIF This library exposes the following toplevel modules:
BCHLibPETypes BCHPEAssemblyTableLayout BCHPEExnHandler BCHPEExportDirectory BCHPEHeader BCHPEImportDirectory BCHPELoadConfigurationStructure BCHPEResourceDirectory BCHPESection BCHPESectionHeader BCHPESections Access point for all sectionsBCHPEStringTable BCHPESymbolTable This library exposes the following toplevel modules:
BCHConstructPowerFunction BCHDisassemblePower BCHDisassemblePowerInstruction BCHDisassembleVLEInstruction BCHFnPowerDictionary BCHPowerAnalysisResults BCHPowerAssemblyBlock BCHPowerAssemblyFunction BCHPowerAssemblyFunctions Provides the access point to retrieve assembly functions.BCHPowerAssemblyInstruction BCHPowerAssemblyInstructions BCHPowerCHIFSystem BCHPowerCodePC BCHPowerConditionalExpr BCHPowerDictionary BCHPowerDisassemblyUtils BCHPowerLoopStructure BCHPowerMetrics BCHPowerOpcodeRecords BCHPowerOperand BCHPowerPseudocode BCHPowerSumTypeSerializer BCHPowerTypes BCHTranslatePowerToCHIF This library exposes the following toplevel modules:
BCHAssemblyBlock BCHAssemblyFunction BCHAssemblyFunctions BCHAssemblyInstruction BCHAssemblyInstructionAnnotations BCHAssemblyInstructions Holds an array of all of the assembly instructions, made available through a class instance reference.BCHCodePC BCHConditionalJumpExpr BCHDisassemble BCHDisassembleELF BCHDisassembleInstruction BCHDisassembleStream Facility to disassemble a stream of bytes into x86 instructions.BCHDisassembleX0 BCHDisassembleX8 BCHDisassembleX9 BCHDisassembleXc BCHDisassembleXd BCHDisassembleXf BCHDisassemblyMetrics BCHDisassemblyUtils BCHFileFormatUtil BCHFnX86Dictionary BCHFunctionHashes BCHFunctionLoops BCHIFSystem BCHLibx86Types BCHLoopStructure BCHOperand BCHPredefined64bitEDKSemantics BCHPredefinedAllocaSemantics BCHPredefinedCallSemantics BCHPredefinedDelphiRTLClassSemantics BCHPredefinedDelphiRTLSemantics BCHPredefinedDelphiRTLSysUtilsSemantics BCHPredefinedDelphiRTLTypesSemantics BCHPredefinedELFSemantics BCHPredefinedErrnoSemantics BCHPredefinedFPSemantics BCHPredefinedGettersSemantics BCHPredefinedLibInternalCRTSemantics BCHPredefinedLibMemSemantics BCHPredefinedLibMiscSemantics BCHPredefinedLibStrSemantics BCHPredefinedLibWcsSemantics BCHPredefinedPredicatesSemantics BCHPredefinedProlog3Semantics BCHPredefinedProlog4Semantics BCHPredefinedSettersSemantics BCHPredefinedUpdatersSemantics BCHPredefinedUtil BCHPredefinedWrappedCallSemantics BCHPullData BCHTranslateToCHIF BCHX86AnalysisResults BCHX86Dictionary BCHX86Metrics BCHX86OpcodeRecords BCHX86Opcodes BCHX86SumTypeSerializer This library exposes the following toplevel modules:
CCHAnalysisTypes CCHAnalyze CCHAssignmentTranslator CCHCallTranslator CCHCfgTranslator CCHCheckImplication Check if a proof obligation is implied by assumptionsCCHCheckValidity CCHCommand CCHCommon CCHControlFlowGraph Translate unstructured statements to CHIFCCHEngineUtil CCHEnvironment CCHExpTranslator CCHExpr CCHExtractInvariantFacts CCHFunctionTranslator CCHGenerateAndCheck CCHGenerateLocalInvariants CCHInvariantStore CCHNumericalConstraints CCHOperationsProvider CCHOrakel CCHPOCheckAllocationBase CCHPOCheckBuffer CCHPOCheckCast CCHPOCheckCommonBase CCHPOCheckCommonBaseType CCHPOCheckControlledResource CCHPOCheckFormatCast CCHPOCheckInScope CCHPOCheckIndexLowerBound CCHPOCheckIndexUpperBound CCHPOCheckInitialized CCHPOCheckInitializedRange CCHPOCheckIntOverflow CCHPOCheckIntUnderflow CCHPOCheckIntUtil CCHPOCheckLowerBound CCHPOCheckNoOverlap CCHPOCheckNonNegative CCHPOCheckNotNull CCHPOCheckNotZero CCHPOCheckNullTerminated CCHPOCheckPointerCast CCHPOCheckPreservedAllMemory CCHPOCheckPtrLowerBound CCHPOCheckPtrUpperBound CCHPOCheckSignedToSignedCastLB CCHPOCheckSignedToSignedCastUB CCHPOCheckSignedToUnsignedCastLB CCHPOCheckSignedToUnsignedCastUB CCHPOCheckStackAddressEscape CCHPOCheckUIntUnderflow CCHPOCheckUnsignedToSignedCast CCHPOCheckUnsignedToUnsignedCast CCHPOCheckUpperBound CCHPOCheckValidMem CCHPOCheckValueConstraint CCHPOCheckValuePreserved CCHPOCheckWidthOverflow CCHPOChecker CCHPOQuery CCHPostCondition This library exposes the following toplevel modules:
CHCilDeclarations CHCilDictionary CHCilFileUtil CHCilFunDeclarations CHCilSumTypeSerializer CHCilTypes CHCilWriteXml This library exposes the following toplevel modules:
CCHBasicTypes CCHBasicTypesXml CCHBasicUtil CCHCAttributes CCHCodewalker CCHContext Representation of a location within a programCCHDeclarations CCHDictionary CCHExternalPredicate CCHFileContract CCHFileEnvironment CCHFunDeclarations CCHFunctionSummary CCHIndexedCollections CCHInterfaceDictionary CCHLibTypes CCHMachineSizes CCHSettings CCHSumTypeSerializer CCHTypesCompare CCHTypesSize CCHTypesToPretty CCHTypesTransformer CCHTypesUtil CCHUtilities This library exposes the following toplevel modules:
CCHApiAssumption CCHAssignDictionary CCHCallsite CCHCheckValid CCHContractAssumption CCHCreatePrimaryProofObligations CCHDataStructureInvariants CCHDsAssumption CCHFunctionAPI CCHGlobalAssignment CCHGlobalAssumption CCHInvDictionary CCHInvariantFact CCHMemoryBase CCHMemoryReference CCHMemoryRegion CCHPODictionary CCHPOExplanations CCHPOPredicate CCHPPO CCHPostRequest CCHPreFileIO File organizationCCHPreSumTypeSerializer CCHPreTypes CCHPredicateDictionary CCHPrimaryProofObligations CCHProofObligation CCHProofScaffolding CCHReturnsite CCHSPO CCHVarDictionary CCHVariable This library exposes the following toplevel modules:
CHAtlas CHAtlasTable CHBitstring CHBooleanConstantsDomainNoArrays CHBounds CHChernikova CHCollections CHCommon CHCommunications CHConstantPropagationNoArrays CHConstants CHDomain CHDomainObserver CHExternalValues CHGaussSeidelSigmaCombinator CHIndexedHTable CHInternalization CHIntervals CHIntervalsDomainExtensiveArrays CHIntervalsDomainNoArrays CHIterator CHLanguage CHLinearEqualitiesDomainNoArrays CHLocalIterationSigmaCombinator CHMatrix CHNonRelationalDatabase CHNonRelationalDomainBase CHNonRelationalDomainExtensiveArrays CHNonRelationalDomainNoArrays CHNonRelationalDomainValues CHNonRelationalTable CHNumerical CHNumericalConstantsDomainExtensiveArrays CHNumericalConstantsDomainNoArrays CHNumericalConstraints CHOnlineCodeSet CHPEPRBounds CHPEPRDictionary CHPEPRDomainNoArrays CHPEPRTypes CHPEPRange CHPolyhedra CHPolyhedraDomainNoArrays CHPolyhedraGlobalData CHPretty CHSCC CHSaturationMatrix CHSigmaCombinator CHStack CHStateSetsDomainNoArrays CHStaticChecker CHStaticInliner CHStridedGaussSeidelSigmaCombinator CHStridedIntervals CHStridedIntervalsDomainExtensiveArrays CHStridedIntervalsDomainNoArrays CHSymbolicConstantsDomainExtensiveArrays CHSymbolicConstantsDomainNoArrays CHSymbolicSets CHSymbolicSetsDomainExtensiveArrays CHSymbolicSetsDomainNoArrays CHSymbolicTypeRefinement CHTIntervals CHTimedSymbolicSetsDomainNoArrays CHUnionFind CHUtils CHValueSets CHValueSetsDomainNoArrays CHVector This library exposes the following toplevel modules:
CHAnalysisSetup Utilities to set up an analysisCHCHIFXml CHDot Utilities to output a GraphViz dot fileCHFileIO CHFormatStringParser Utility to parse C-style format stringsCHGc Utility to extract garbage collector settingsCHIndexTable CHInvAccess Utilities to access invariants in standard domainsCHInvStore Utilities to store invariantsCHLogger Facility to record problems during a run of the analyzer.CHLoopStructure CHMaps CHMemoryRecorder Utility to take snapshots of memory usageCHNestedCommands CHNumConstraintPrinter Pretty printer for various forms of numerical constraintsCHNumRecordTable data structure to store records identified by numerical id'sCHPrettyUtil CHReportUtil CHStats Utilities to keep track of tagged statisticsCHStringIndexTable CHSumTypeSerializer Serialization of sum typesCHTiming Utility to keep track of CPU time used on various tasksCHTimingLog Utility to log events and timingCHTraceResult Result values with a list of strings as error value.CHUtil CHXmlDocument Utilities to build xml filesCHXmlReader Utilities to read xml filesThis library exposes the following toplevel modules:
JCHCostAPI JCHCostBound JCHCostBounds JCHCostBoundsAnalysis JCHCostBoundsDomainNoArrays JCHCostBoundsModel JCHCostModelUtil JCHCostUtils JCHLoopCostAbstractor JCHMethodCostBoundsAbstractor JCHOpcodeCosts This library exposes the following toplevel modules:
JCHExprFeatureExtraction JCHFeatureDictionary JCHFeatureExtraction JCHFeatureSumTypeSerializer JCHFeaturesAPI Extract key-value pairs from class filesJCHMethodExprs JCHSubgraph This library exposes the following toplevel modules:
JCHArrayInstantiation JCHBasicTypes JCHBasicTypesAPI Definition of most data types used in jchlibJCHBcDictionary JCHBytecode JCHClass JCHCopyPropagationNoArrays JCHDictionary JCHDumpBasicTypes JCHFile JCHIFUtil Utility functions for CHIF data typesJCHInstruction JCHJTDictionary JCHJTerm JCHMethod JCHParse JCHParseCode JCHParseUTF8Signature JCHRaw2IF JCHRawBasicTypes JCHRawClass JCHSignature JCHSimplify JCHStackLayout JCHSumTypeSerializer JCHTransform JCHTranslateToCHIF JCHUnparse JCHUnparseSignature JCHXmlUtil This library exposes the following toplevel modules:
JCHAnalysis JCHAnalysisUtils JCHArrayUtils JCHCollectors JCHFields JCHIntStubs JCHIntervalArray JCHLinearConstraint JCHNumericAnalysis JCHNumericInfo JCHNumericUtils JCHPoly JCHPolyIntDomainNoArrays JCHPolyIntervalArray JCHTGraph JCHTGraphAnalysis JCHTGraphStubs JCHTGraphTransformers JCHTNode JCHTOriginGraphs JCHTaintLoopUtils This library exposes the following toplevel modules:
JCHAPISummaryTemplate JCHAnalysisResults JCHAnnotationsPre JCHApplication JCHBCFunction JCHBcPattern JCHBcPatternSummary JCHBytecodeData JCHBytecodeLocation JCHCGDictionary Dictionary of typesJCHCHAUtil JCHCallgraphBase JCHClassAnalysis JCHClassInfo JCHClassLoader JCHClassSummary JCHClassSummaryTemplate JCHClassUserTemplate JCHCodegraph JCHFieldInfo JCHFunctionSummary JCHFunctionSummaryLibrary JCHFunctionSummaryXmlDecoder JCHIFSemantics JCHIFSystem JCHInstructionInfo JCHIntegrateSummaries JCHInvariant JCHLoops JCHMethodAssumptions JCHMethodImplementations JCHMethodInfo JCHNativeMethods JCHPreAPI JCHPreFileIO JCHPreSumTypeSerializer JCHProfileSummaryTemplate JCHSignatureBindings JCHStackSlotValue JCHStringSets JCHStringSetsDomainNoArrays JCHSupplementSummary JCHSystemSettings JCHTaintOrigin JCHTemplateUtil JCHTypeSets JCHTypeSetsDomainNoArrays JCHUserData This library exposes the following toplevel modules:
JCHAnalysisSetUp JCHCallGraph JCHCodeTransformers JCHDominance JCHGlobals JCHLoopUtils JCHPrintUtils JCHProcInfo JCHRevDominance JCHSSA JCHSplitArray JCHSystem JCHSystemUtils JCHTransformUtils JCHTypeUtils JCHVarInfo JCHVarInfoCollectors JCHVarRepresentative This library exposes the following toplevel modules:
This library exposes the following toplevel modules:
The entry point of this library is the module: TCHBchlibelfAssertion.
This library exposes the following toplevel modules:
This library exposes the following toplevel modules:
TCHAssertion Provides functions evaluating assertions.TCHGenerator Provides functions generating values.TCHReducer Provides functions reducing values to produce smaller counterexamples.TCHSpecification Provides type definitions, base functions, and combinators allowing to encode specificationsTCHTest Provides the functions for creating and running tests.TCHTestApi TCHTestSuite Provides a framework for creating and running tests.TCHUtils This library exposes the following toplevel modules:
This library exposes the following toplevel modules:
XSumTypeSerializer Serialization of sum typesXconsequence XprDictionary XprToPretty XprTypes XprUtil XprXml Xprt Xrewrite Xsimplify