package goblint
Static analysis framework for C
Install
Dune Dependency
Authors
Maintainers
Sources
goblint-2.5.0.tbz
sha256=452d8491527aea21f2cbb11defcc14ba0daf9fdb6bdb9fc0af73e56eac57b916
sha512=1993cd45c4c7fe124ca6e157f07d17ec50fab5611b270a434ed1b7fb2910aa85a8e6eaaa77dad770430710aafb2f6d676c774dd33942d921f23e2f9854486551
doc/src/goblint.lib/goblint_lib.ml.html
Source file goblint_lib.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456
(** Main library. *) (** {1 Framework} *) module Maingoblint = Maingoblint module Control = Control module Server = Server (** {2 CFG} Control-flow graphs (CFGs) are used to represent each function. *) module Node = Node module Edge = Edge module MyCFG = MyCFG module CfgTools = CfgTools (** {2 Specification} Analyses are specified by domains and transfer functions. A dynamic composition of analyses is combined with CFGs to produce a constraint system. *) module Analyses = Analyses module ConstrSys = ConstrSys module Constraints = Constraints module CompareConstraints = CompareConstraints module AnalysisState = AnalysisState module AnalysisStateUtil = AnalysisStateUtil module ControlSpecC = ControlSpecC (** Master control program (MCP) is the analysis specification for the dynamic product of activated analyses. *) module MCP = MCP module MCPRegistry = MCPRegistry module MCPAccess = MCPAccess (** MCP allows activated analyses to query each other during the analysis. Query results from different analyses for the same query are {{!Lattice.S.meet} met} for precision. *) module Queries = Queries (** MCP allows activated analyses to emit events to each other during the analysis. *) module Events = Events (** {2 Results} The following modules help query the constraint system solution using semantic information. *) module AnalysisResult = AnalysisResult module ResultQuery = ResultQuery module VarQuery = VarQuery (** {2 Configuration} Runtime configuration is represented as JSON. Options are specified and documented by the JSON schema [src/config/options.schema.json]. *) module GobConfig = GobConfig module AfterConfig = AfterConfig module AutoTune = AutoTune module AutoSoundConfig = AutoSoundConfig module JsonSchema = JsonSchema module Options = Options (** {1 Analyses} Analyses activatable under MCP. *) (** {2 Value} Analyses related to values of program variables. *) module Base = Base module RelationAnalysis = RelationAnalysis module ApronAnalysis = ApronAnalysis module AffineEqualityAnalysis = AffineEqualityAnalysis module LinearTwoVarEqualityAnalysis = LinearTwoVarEqualityAnalysis module VarEq = VarEq module CondVars = CondVars module TmpSpecial = TmpSpecial (** {2 Heap} Analyses related to the heap. *) module Region = Region module MallocFresh = MallocFresh module Malloc_null = Malloc_null module MemLeak = MemLeak module UseAfterFree = UseAfterFree module MemOutOfBounds = MemOutOfBounds (** {2 Concurrency} Analyses related to concurrency. *) (** {3 Locks} Analyses related to locking. *) module MutexEventsAnalysis = MutexEventsAnalysis module LocksetAnalysis = LocksetAnalysis module MutexTypeAnalysis = MutexTypeAnalysis module MutexAnalysis = MutexAnalysis module MayLocks = MayLocks module SymbLocks = SymbLocks module Deadlock = Deadlock (** {3 Threads} Analyses related to threads. *) module ThreadFlag = ThreadFlag module ThreadId = ThreadId module ThreadAnalysis = ThreadAnalysis module ThreadJoins = ThreadJoins module MHPAnalysis = MHPAnalysis module ThreadReturn = ThreadReturn (** {3 Other} *) module RaceAnalysis = RaceAnalysis module BasePriv = BasePriv module RelationPriv = RelationPriv module ThreadEscape = ThreadEscape module PthreadSignals = PthreadSignals module ExtractPthread = ExtractPthread (** {2 Longjmp} Analyses related to [longjmp] and [setjmp]. *) module ActiveSetjmp = ActiveSetjmp module ModifiedSinceSetjmp = ModifiedSinceSetjmp module ActiveLongjmp = ActiveLongjmp module PoisonVariables = PoisonVariables module Vla = Vla (** {2 Tutorial} Analyses for didactic purposes. *) module Constants = Constants module Signs = Signs module Taint = Taint module UnitAnalysis = UnitAnalysis (** {2 Other} *) module Assert = Assert module LoopTermination = LoopTermination module Callstring = Callstring module LoopfreeCallstring = LoopfreeCallstring module Uninit = Uninit module Expsplit = Expsplit module StackTrace = StackTrace (** {2 Helper} Analyses which only support other analyses. *) module AccessAnalysis = AccessAnalysis module WrapperFunctionAnalysis = WrapperFunctionAnalysis module TaintPartialContexts = TaintPartialContexts module UnassumeAnalysis = UnassumeAnalysis module ExpRelation = ExpRelation module AbortUnless = AbortUnless module PtranalAnalysis = PtranalAnalysis (** {1 Analysis lifters} Transformations of analyses into extended analyses. *) module SpecLifters = SpecLifters module LongjmpLifter = LongjmpLifter module RecursionTermLifter = RecursionTermLifter module ContextGasLifter = ContextGasLifter module WideningToken = WideningToken module WideningTokenLifter = WideningTokenLifter module WitnessConstraints = WitnessConstraints (** {1 Domains} Domains used by analysis specifications and constraint systems are {{!Lattice.S} lattices}. Besides lattice operations, their elements can also be compared and output (in various formats). Those operations are specified by {!Printable.S}. *) module Printable = Printable module Lattice = Lattice (** {2 General} Standard general-purpose domains and domain functors. *) module BoolDomain = BoolDomain module SetDomain = SetDomain module MapDomain = MapDomain module TrieDomain = TrieDomain module DisjointDomain = DisjointDomain module HoareDomain = HoareDomain module PartitionDomain = PartitionDomain module FlagHelper = FlagHelper (** {2 Analysis-specific} Domains for specific analyses. *) (** {3 Value} *) (** {4 Non-relational} Domains for {!Base} analysis. *) (** {5 Numeric} *) module IntDomain = IntDomain module FloatDomain = FloatDomain (** {5 Addresses} Memory locations are identified by {{!Mval} mvalues}, which consist of a {{!GoblintCil.varinfo} variable} and an {{!Offset.t} offset}. Mvalues are used throughout Goblint, not just the {!Base} analysis. Addresses extend mvalues with [NULL], unknown pointers and string literals. *) module Mval = Mval module Offset = Offset module StringDomain = StringDomain module AddressDomain = AddressDomain (** {5 Complex} *) module StructDomain = StructDomain module UnionDomain = UnionDomain module ArrayDomain = ArrayDomain module NullByteSet = NullByteSet module JmpBufDomain = JmpBufDomain (** {5 Combined} These combine the above domains together for {!Base} analysis. *) module BaseDomain = BaseDomain module ValueDomain = ValueDomain module ValueDomainQueries = ValueDomainQueries (** {4 Relational} Domains for {!RelationAnalysis}. *) module RelationDomain = RelationDomain module ApronDomain = ApronDomain module AffineEqualityDomain = AffineEqualityDomain module LinearTwoVarEqualityDomain = LinearTwoVarEqualityDomain (** {3 Concurrency} *) module MutexAttrDomain = MutexAttrDomain module LockDomain = LockDomain module SymbLocksDomain = SymbLocksDomain module DeadlockDomain = DeadlockDomain module ThreadFlagDomain = ThreadFlagDomain module ThreadIdDomain = ThreadIdDomain module ConcDomain = ConcDomain module MHP = MHP module EscapeDomain = EscapeDomain module PthreadDomain = PthreadDomain (** {3 Other} *) module Basetype = Basetype module Lval = Lval module Access = Access module AccessDomain = AccessDomain module MusteqDomain = MusteqDomain module RegionDomain = RegionDomain module StackDomain = StackDomain (** {2 Testing} Modules related to (property-based) testing of domains. *) module DomainProperties = DomainProperties module AbstractionDomainProperties = AbstractionDomainProperties module IntDomainProperties = IntDomainProperties (** {1 Incremental} Incremental analysis is for analyzing multiple versions of the same program and reusing as many results as possible. *) module CompareCIL = CompareCIL module CompareAST = CompareAST module CompareCFG = CompareCFG module UpdateCil = UpdateCil module MaxIdUtil = MaxIdUtil module Serialize = Serialize module CilMaps = CilMaps (** {1 I/O} Various input/output interfaces and formats. *) module Messages = Messages module Logs = Logs (** {2 Front-end} The following modules handle program input. *) module Preprocessor = Preprocessor module CompilationDatabase = CompilationDatabase module MakefileUtil = MakefileUtil module TerminationPreprocessing = TerminationPreprocessing (** {2 Witnesses} Witnesses are an exchangeable format for analysis results. *) module Svcomp = Svcomp module SvcompSpec = SvcompSpec module Invariant = Invariant module InvariantCil = InvariantCil module WitnessUtil = WitnessUtil (** {3 GraphML} Automaton-based GraphML witnesses used in SV-COMP. *) module MyARG = MyARG module ArgTools = ArgTools module Witness = Witness module Graphml = Graphml (** {3 YAML} Entry-based YAML witnesses to be used in SV-COMP. *) module YamlWitness = YamlWitness module YamlWitnessType = YamlWitnessType (** {3 Violation} Experimental generation of violation witness automata or refinement with observer automata. *) module Violation = Violation module ViolationZ3 = ViolationZ3 module ObserverAutomaton = ObserverAutomaton module ObserverAnalysis = ObserverAnalysis module Refinement = Refinement (** {2 SARIF} *) module Sarif = Sarif module SarifType = SarifType module SarifRules = SarifRules (** {1 Transformations} Transformations can be activated to transform the program using analysis results. *) module Transform = Transform module DeadCode = DeadCode module EvalAssert = EvalAssert module ExpressionEvaluation = ExpressionEvaluation (** {1 Utilities} *) module Timing = Timing module GoblintDir = GoblintDir (** {2 General} *) module IntOps = IntOps module FloatOps = FloatOps module LazyEval = LazyEval module ResettableLazy = ResettableLazy module ProcessPool = ProcessPool module Timeout = Timeout module TimeUtil = TimeUtil module MessageUtil = MessageUtil module AnsiColors = AnsiColors module XmlUtil = XmlUtil module GobExn = GobExn (** {2 CIL} *) module CilType = CilType module Cilfacade = Cilfacade module CilLocation = CilLocation module RichVarinfo = RichVarinfo module CilCfg = CilCfg module LoopUnrolling = LoopUnrolling (** {2 Library specification} For more precise analysis of C standard library, etc functions, whose definitions are not available, custom specifications can be added. *) module AccessKind = AccessKind module LibraryDesc = LibraryDesc module LibraryDsl = LibraryDsl module LibraryFunctions = LibraryFunctions (** {2 Analysis-specific} *) module BaseUtil = BaseUtil module PrecisionUtil = PrecisionUtil module ContextUtil = ContextUtil module ReturnUtil = ReturnUtil module BaseInvariant = BaseInvariant module CommonPriv = CommonPriv module WideningThresholds = WideningThresholds module VectorMatrix = VectorMatrix module GobApron = GobApron (** {2 Precision comparison} *) module PrecCompare = PrecCompare module PrecCompareUtil = PrecCompareUtil module PrivPrecCompareUtil = PrivPrecCompareUtil module RelationPrecCompareUtil = RelationPrecCompareUtil module ApronPrecCompareUtil = ApronPrecCompareUtil (** {1 Library extensions} OCaml library extensions which are completely independent of Goblint. See {!Goblint_std}. *) (** {2 Standard library} OCaml standard library extensions which are not provided by {!Batteries}. *) module GobFormat = GobFormat
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>