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 analysisBasePriv 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 workContainDomain 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.orgLattice 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 ProgramMaingoblint 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