goblint

API

Library goblint.lib

• AbstractionDomainProperties
• Access
• AddressDomain
• AfterConfig
• Analyses Signatures for analyzers, analysis specifications, and result output.
• ApronAnalysis
• ApronDomain
• ApronPrecCompareUtil
• ApronPriv
• Arinc Tracking of arinc processes and their actions. Output to console, graphviz and promela.
• ArincDomain
• ArincUtil
• ArrayDomain
• Base Value analysis.
• BaseDomain domain of the base analysis
• BasePriv
• BaseUtil
• Basetype
• BoolDomain
• CfgTools
• CilType
• Cilfacade Helpful functions for dealing with Cil.
• CommonPriv
• CompareAST
• CompareCFG
• CompareCIL
• ConcDomain
• CondVars Must equality between variables and logical expressions.
• Config
• Constants
• Constraints How to generate constraints for a solver using specifications described in Analyses.
• Contain Protection using 'private' field modifier in C++. see doi.org/10.1007/978-3-642-28891-3_11 A. Herz, and K. Apinis "Class-Modular, class-escape and points-to analysis for object-oriented languages" Builds on the ability of LLVM < 3.1 to emit semantically equivalent C code as a target Requires a CXX.json file to work
• ContainDomain
• ContextUtil
• Control An analyzer that takes the CFG from MyCFG, a solver from Selector, constraints from Constraints (using the specification from MCP)
• Db
• Deadcode
• Deadlock Deadlock analysis.
• DeadlockDomain
• DeadlocksByRaces Deadlock analysis using data race detection.
• Defaults Default values for GobConfig-style configuration.
• DomainProperties
• Edge
• EffectWConEq
• EscapeDomain
• Events
• Exp
• ExpDomain
• ExpRelation An analysis specification to answer questions about how two expressions relate to each other.
• ExpressionEvaluation
• Extract_arinc Extract function calls and variables.
• Extract_osek Extract osek function calls.
• FileDomain
• FileUse An analysis for checking correct use of file handles.
• Flag Analysis for the OSEK flag pattern.
• FlagModeDomain
• FlagModes Flag state values.
• Generic
• GobConfig New, untyped, path-based configuration subsystem.
• GobFormat
• GobYojson
• Goblintutil Globally accessible flags and utility functions.
• Graphml
• HoareDomain Abstract domains with Hoare ordering.
• IntDomain Abstract Domains for integers. These are domains that support the C * operations on integer values.
• IntDomainProperties
• IntOps
• Invariant
• InvariantCil
• JsonSchema A simpler schema than http://json-schema.org
• Lattice The lattice signature and simple functors for building lattices.
• LazyEval
• LibraryFunctions This allows us to query information about library functions.
• ListDomain
• LockDomain
• Lval
• LvalMapDomain
• MCP Master Control Program
• Maingoblint This is the main program!
• MakefileUtil
• MallocWrapperAnalysis An analysis that handles the case when malloc is called from a wrapper function all over the code.
• Malloc_null Path-sensitive analysis that verifies checking the result of the malloc function.
• MapDomain Specification and functors for maps.
• MayLocks May-lockset analysis.
• MemoryDomain
• MessageCategory
• MessageUtil
• Messages
• MusteqDomain
• MutexAnalysis Data race analysis.
• MyARG
• MyCFG Our Control-flow graph implementation.
• MyCheck
• MyLiveness
• Node
• ObserverAnalysis
• ObserverAutomaton
• Octagon
• OctagonDomain
• OctagonMapDomain
• Oil
• OilLexer
• OilParser
• OilUtil
• Osek Data race analysis for OSEK programs.
• Osektransactionality Another OSEK analysis.
• Osektupel
• PartitionDomain Partitioning domains.
• Pml
• Pml_arinc
• Pml_osek
• PostSolver
• PreValueDomain
• PrecCompare
• PrecCompareUtil
• Prelude
• Printable Some things are not quite lattices ...
• Printer
• PrivPrecCompareUtil
• Queries Structures for the querying subsystem.
• Refinement
• Region Assigning static regions to dynamic memory.
• RegionDomain
• RichVarinfo
• SLR The 'slr*' solvers.
• SLRphased
• SLRterm
• Sarif
• SarifRules
• SarifType
• Selector
• Serialize
• SetDomain
• ShapeDomain
• Shapes Shape analysis for cyclic doubly linked lists.
• Signs An analysis specification for didactic purposes.
• Spec Analysis by specification file.
• SpecCore
• SpecDomain
• SpecLexer
• SpecParser
• SpecUtil
• StackDomain
• StackTrace Stack-trace "analyses".
• StructDomain Abstract domains representing structs.
• Svcomp
• SymbLocks Symbolic lock-sets for use in per-element patterns.
• Td3 Incremental terminating top down solver that optionally only keeps values at widening points and restores other values afterwards.
• Termination Termination of loops.
• ThreadAnalysis Thread creation and uniqueness analyses.
• ThreadEscape Variables that escape threads using the last argument from pthread_create.
• ThreadFlag Multi-threadedness analysis.
• ThreadFlagDomain
• ThreadId Current thread ID analysis.
• ThreadIdDomain
• ThreadJoins
• ThreadReturn Thread returning analysis.
• TimeUtil
• Timeout
• TopDown Top down solver using box/warrow. This is superseded by td3 but kept as a simple version without term & space (& incremental).
• TopDown_deprecated
• TopDown_space_cache_term Terminating top down solver that only keeps values at widening points and restores other values afterwards.
• TopDown_term Top down solver.
• Tracing
• Transform
• Uninit Local variable initialization analysis.
• UnionDomain
• Unit An analysis specification for didactic purposes.
• UpdateCil
• ValueDomain
• VarEq Variable equalities necessary for per-element patterns.
• Version
• VersionLookup
• Violation
• ViolationZ3
• Witness
• WitnessConstraints An analysis specification for witnesses.
• WitnessUtil
• Worklist
• XmlUtil

Library goblint.sites

• Goblint_sites

Library goblint_sites_dune

• Goblint_sites

Library goblint_sites_js

• Goblint_sites