diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml new file mode 100644 index 0000000000..fdfb948cdc --- /dev/null +++ b/.github/workflows/docs.yml @@ -0,0 +1,68 @@ +name: docs + +on: + push: + branches: + - master + + workflow_dispatch: + +permissions: + contents: read + pages: write + id-token: write + +concurrency: + group: "pages" + cancel-in-progress: true + +jobs: + api-build: + strategy: + matrix: + os: + - ubuntu-latest + ocaml-compiler: + - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file + # don't add any other because they won't be used + + runs-on: ${{ matrix.os }} + + steps: + - name: Checkout code + uses: actions/checkout@v3 + + - name: Set up OCaml ${{ matrix.ocaml-compiler }} + env: + # otherwise setup-ocaml pins non-locked dependencies + # https://github.com/ocaml/setup-ocaml/issues/166 + OPAMLOCKED: locked + uses: ocaml/setup-ocaml@v2 + with: + ocaml-compiler: ${{ matrix.ocaml-compiler }} + + - name: Setup Pages + id: pages + uses: actions/configure-pages@v2 + + - name: Install dependencies + run: opam install . --deps-only --locked --with-doc + + - name: Build API docs + run: opam exec -- dune build @doc + + - name: Upload artifact + uses: actions/upload-pages-artifact@v1 + with: + path: _build/default/_doc/_html/ + + api-deploy: + environment: + name: github-pages + url: ${{ steps.deployment.outputs.page_url }} + runs-on: ubuntu-latest + needs: api-build + steps: + - name: Deploy to GitHub Pages + id: deployment + uses: actions/deploy-pages@v1 diff --git a/mkdocs.yml b/mkdocs.yml index f1926e5cec..558c381e66 100644 --- a/mkdocs.yml +++ b/mkdocs.yml @@ -30,6 +30,7 @@ nav: - 👶 Your first analysis: developer-guide/firstanalysis.md - 🏫 Extending library: developer-guide/extending-library.md - 📢 Messaging: developer-guide/messaging.md + - 🗃️ API reference: https://goblint.github.io/analyzer/ - 🚨 Testing: developer-guide/testing.md - 🪲 Debugging: developer-guide/debugging.md - 📉 Profiling: developer-guide/profiling.md diff --git a/src/analyses/abortUnless.ml b/src/analyses/abortUnless.ml index d030ca8a24..813d999ac3 100644 --- a/src/analyses/abortUnless.ml +++ b/src/analyses/abortUnless.ml @@ -1,4 +1,6 @@ -(** An analysis checking whether a function only returns if its only argument has a non-zero value. *) +(** Analysis of [assume_abort_if_not]-style functions ([abortUnless]). + + Such a function only returns if its only argument has a non-zero value. *) open GoblintCil open Analyses diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml index 448345dd78..4ad207b3b8 100644 --- a/src/analyses/accessAnalysis.ml +++ b/src/analyses/accessAnalysis.ml @@ -1,4 +1,4 @@ -(** Access analysis. *) +(** Analysis of memory accesses ([access]). *) module LF = LibraryFunctions open GoblintCil diff --git a/src/analyses/activeLongjmp.ml b/src/analyses/activeLongjmp.ml index 72905862c3..9c9868e32f 100644 --- a/src/analyses/activeLongjmp.ml +++ b/src/analyses/activeLongjmp.ml @@ -1,4 +1,4 @@ -(** Analysis tracking which longjmp is currently active *) +(** Analysis of active [longjmp] targets ([activeLongjmp]). *) open GoblintCil open Analyses diff --git a/src/analyses/activeSetjmp.ml b/src/analyses/activeSetjmp.ml index f144046a44..498d89ea3b 100644 --- a/src/analyses/activeSetjmp.ml +++ b/src/analyses/activeSetjmp.ml @@ -1,4 +1,4 @@ -(** Analysis tracking which setjmp(s) are currently active *) +(** Analysis of active [setjmp] buffers ([activeSetjmp]). *) open GoblintCil open Analyses diff --git a/src/analyses/apron/affineEqualityAnalysis.apron.ml b/src/analyses/apron/affineEqualityAnalysis.apron.ml index fe59209ca6..03a9ecdb57 100644 --- a/src/analyses/apron/affineEqualityAnalysis.apron.ml +++ b/src/analyses/apron/affineEqualityAnalysis.apron.ml @@ -1,5 +1,7 @@ -(* Ref: Affine Relationships Among Variables of a Program, Michael Karr 1976 - https://link.springer.com/content/pdf/10.1007/BF00268497.pdf *) +(** {{!RelationAnalysis} Relational integer value analysis} using an OCaml implementation of the affine equalities domain ([affeq]). + + @see Karr, M. Affine relationships among variables of a program. *) + open Analyses include RelationAnalysis diff --git a/src/analyses/apron/apronAnalysis.apron.ml b/src/analyses/apron/apronAnalysis.apron.ml index f3a2374bc1..29e295a662 100644 --- a/src/analyses/apron/apronAnalysis.apron.ml +++ b/src/analyses/apron/apronAnalysis.apron.ml @@ -1,4 +1,5 @@ -(** Analysis using Apron for integer variables. *) +(** {{!RelationAnalysis} Relational integer value analysis} using {!Apron} domains ([apron]). *) + open Analyses include RelationAnalysis diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index 56710872b1..9d2cd7a5e4 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -1,3 +1,7 @@ +(** Abstract relational {e integer} value analysis. + + See {!ApronAnalysis} and {!AffineEqualityAnalysis}. *) + (** Contains most of the implementation of the original apronDomain, but now solely operates with functions provided by relationDomain. *) open Batteries diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index c2726b42df..160d2b07ed 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -1,4 +1,6 @@ -(** Has been modified to work with any domain that uses the functions provided relationDomain. *) +(** Relational thread-modular value analyses for {!RelationAnalysis}, i.e. {!ApronAnalysis} and {!AffineEqualityAnalysis}. + + @see Schwarz, M., Saan, S., Seidl, H., Erhard, J., Vojdani, V. Clustered Relational Thread-Modular Abstract Interpretation with Local Traces. *) open Batteries open GoblintCil diff --git a/src/analyses/assert.ml b/src/analyses/assert.ml index 33dbe448ec..8247a0d7e8 100644 --- a/src/analyses/assert.ml +++ b/src/analyses/assert.ml @@ -1,3 +1,5 @@ +(** Analysis of [assert] results ([assert]). *) + open Batteries open GoblintCil open Analyses diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 84cd0cbb24..5c7480ad74 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1,4 +1,4 @@ -(** Value analysis. *) +(** Non-relational value analysis aka {e base analysis} ([base]). *) open Batteries open GoblintCil diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index af06d64435..fe7a1069ff 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -1,3 +1,5 @@ +(** {!Analyses.Spec.branch} refinement for {!Base} analysis. *) + open GoblintCil module M = Messages diff --git a/src/analyses/basePriv.mli b/src/analyses/basePriv.mli index 781771c221..767e0e72bb 100644 --- a/src/analyses/basePriv.mli +++ b/src/analyses/basePriv.mli @@ -1,3 +1,7 @@ +(** Non-relational thread-modular value analyses for {!Base}. + + @see Schwarz, M., Saan, S., Seidl, H., Apinis, K., Erhard, J., Vojdani, V. Improving Thread-Modular Abstract Interpretation. *) + open GoblintCil (* Cannot use local module substitutions because ppx_import is still stuck at 4.07 AST: https://github.com/ocaml-ppx/ppx_import/issues/50#issuecomment-775817579. *) (* TODO: try again, because ppx_import is now removed *) diff --git a/src/analyses/baseUtil.mli b/src/analyses/baseUtil.mli index d01d57b146..7054cd57fc 100644 --- a/src/analyses/baseUtil.mli +++ b/src/analyses/baseUtil.mli @@ -1,3 +1,5 @@ +(** Basic analysis utilities. *) + open GoblintCil val is_global: Queries.ask -> varinfo -> bool diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index d473a3c3e1..fa639295b3 100644 --- a/src/analyses/commonPriv.ml +++ b/src/analyses/commonPriv.ml @@ -1,3 +1,5 @@ +(** Thread-modular value analysis utilities for {!BasePriv} and {!RelationPriv}. *) + open Batteries open GoblintCil open Analyses diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml index c4189661d9..abe9f61ae2 100644 --- a/src/analyses/condVars.ml +++ b/src/analyses/condVars.ml @@ -1,4 +1,4 @@ -(** Must equality between variables and logical expressions. *) +(** Symbolic variable - logical expression equalities analysis ([condvars]). *) (* TODO: unused, what is this analysis? *) open Batteries diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml index 09d16eed03..c23d6f4294 100644 --- a/src/analyses/deadlock.ml +++ b/src/analyses/deadlock.ml @@ -1,4 +1,4 @@ -(** Deadlock analysis. *) +(** Deadlock analysis ([deadlock]). *) open Batteries open GoblintCil diff --git a/src/analyses/expRelation.ml b/src/analyses/expRelation.ml index 486cba79b9..39df650bc0 100644 --- a/src/analyses/expRelation.ml +++ b/src/analyses/expRelation.ml @@ -1,6 +1,8 @@ +(** Stateless symbolic comparison expression analysis ([expRelation]). *) + (** An analysis specification to answer questions about how two expressions relate to each other. *) -(** Currently this works purely syntactically on the expressions, and only for =_{must}. *) -(** Does not keep state, this is only formulated as an analysis to integrate well into framework *) +(** Currently this works purely syntactically on the expressions, and only for {m =_{must}}. *) +(** Does not keep state, this is only formulated as an analysis to integrate well into the framework. *) open GoblintCil open Analyses diff --git a/src/analyses/expsplit.ml b/src/analyses/expsplit.ml index d5eac15a93..f702953598 100644 --- a/src/analyses/expsplit.ml +++ b/src/analyses/expsplit.ml @@ -1,3 +1,5 @@ +(** Path-sensitive analysis according to values of arbitrary given expressions ([expsplit]). *) + open Batteries open GoblintCil open Analyses diff --git a/src/analyses/extractPthread.ml b/src/analyses/extractPthread.ml index 62e7d6b605..8aec79f29f 100644 --- a/src/analyses/extractPthread.ml +++ b/src/analyses/extractPthread.ml @@ -1,4 +1,4 @@ -(** Tracking of pthread lib code. Output to promela. *) +(** Promela extraction analysis for Pthread programs ([extract-pthread]). *) open GoblintCil open Pretty diff --git a/src/analyses/fileUse.ml b/src/analyses/fileUse.ml index b44c7d7923..47a01c13ba 100644 --- a/src/analyses/fileUse.ml +++ b/src/analyses/fileUse.ml @@ -1,4 +1,6 @@ -(** An analysis for checking correct use of file handles. *) +(** Analysis of correct file handle usage ([file]). + + @see Vogler, R. Verifying Regular Safety Properties of C Programs Using the Static Analyzer Goblint. Section 3.*) open Batteries open GoblintCil diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml index a477fc1809..e3d52a9cc3 100644 --- a/src/analyses/libraryDesc.ml +++ b/src/analyses/libraryDesc.ml @@ -1,4 +1,5 @@ (** Library function descriptor (specification). *) + module Cil = GoblintCil (** Pointer argument access specification. *) diff --git a/src/analyses/libraryDsl.mli b/src/analyses/libraryDsl.mli index e134ad68d7..fd0bc45c26 100644 --- a/src/analyses/libraryDsl.mli +++ b/src/analyses/libraryDsl.mli @@ -18,11 +18,11 @@ type ('k, 'r) args_desc = | (::): ('k, _, 'm) arg_desc * ('m, 'r) args_desc -> ('k, 'r) args_desc (** Cons one argument descriptor. Argument must occur. *) -(** Create library function descriptor from arguments descriptor and continuation function, which takes as many arguments as are captured using {!__} and returns the corresponding {!LibraryDesc.special}. *) +(** Create library function descriptor from arguments descriptor and continuation function, which takes as many arguments as are captured using {!__} and returns the corresponding {!LibraryDesc.type-special}. *) val special: ?attrs:LibraryDesc.attr list -> ('k, LibraryDesc.special) args_desc -> 'k -> LibraryDesc.t -(** Create library function descriptor from arguments descriptor, which must {!drop} all arguments, and continuation function, which takes as an {!unit} argument and returns the corresponding {!LibraryDesc.special}. - Unlike {!special}, this allows the {!LibraryDesc.special} of an argumentless function to depend on options, such that they aren't evaluated at initialization time in {!LibraryFunctions}. *) +(** Create library function descriptor from arguments descriptor, which must {!drop} all arguments, and continuation function, which takes as an {!unit} argument and returns the corresponding {!LibraryDesc.type-special}. + Unlike {!special}, this allows the {!LibraryDesc.type-special} of an argumentless function to depend on options, such that they aren't evaluated at initialization time in {!LibraryFunctions}. *) val special': ?attrs:LibraryDesc.attr list -> (LibraryDesc.special, LibraryDesc.special) args_desc -> (unit -> LibraryDesc.special) -> LibraryDesc.t (** Create unknown library function descriptor from arguments descriptor, which must {!drop} all arguments. *) diff --git a/src/analyses/libraryFunctions.mli b/src/analyses/libraryFunctions.mli index cd024b6c94..9a8e55a48a 100644 --- a/src/analyses/libraryFunctions.mli +++ b/src/analyses/libraryFunctions.mli @@ -1,4 +1,5 @@ -(** This allows us to query information about library functions. *) +(** Hard-coded database of library function specifications. *) + open GoblintCil val add_lib_funs : string list -> unit diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml index 739ec43455..b2e8a280fa 100644 --- a/src/analyses/mCP.ml +++ b/src/analyses/mCP.ml @@ -1,4 +1,4 @@ -(** Master Control Program *) +(** MCP analysis specification. *) open Batteries open GoblintCil diff --git a/src/analyses/mCPAccess.ml b/src/analyses/mCPAccess.ml index 44b5931496..92db6fbc5d 100644 --- a/src/analyses/mCPAccess.ml +++ b/src/analyses/mCPAccess.ml @@ -1,3 +1,4 @@ +(** {{!Analyses.MCPA} Memory access metadata module} for MCP. *) open MCPRegistry module Pretty = GoblintCil.Pretty diff --git a/src/analyses/mCPRegistry.ml b/src/analyses/mCPRegistry.ml index 48acb7d0be..bbd6dc5c6b 100644 --- a/src/analyses/mCPRegistry.ml +++ b/src/analyses/mCPRegistry.ml @@ -1,3 +1,6 @@ +(** Registry of dynamically activatable analyses. + Analysis specification modules for the dynamic product. *) + open Batteries open GoblintCil open Pretty diff --git a/src/analyses/mHPAnalysis.ml b/src/analyses/mHPAnalysis.ml index 975f059bf2..a24dbc3cd6 100644 --- a/src/analyses/mHPAnalysis.ml +++ b/src/analyses/mHPAnalysis.ml @@ -1,4 +1,5 @@ -(** MHP access analysis. *) +(** May-happen-in-parallel (MHP) analysis for memory accesses ([mhp]). *) + open Analyses module Spec = diff --git a/src/analyses/mallocFresh.ml b/src/analyses/mallocFresh.ml index 3ecce39345..c4a0c035f2 100644 --- a/src/analyses/mallocFresh.ml +++ b/src/analyses/mallocFresh.ml @@ -1,3 +1,5 @@ +(** Analysis of unescaped (i.e. thread-local) heap locations ([mallocFresh]). *) + open GoblintCil open Analyses diff --git a/src/analyses/mallocWrapperAnalysis.ml b/src/analyses/mallocWrapperAnalysis.ml index 1b0ffbcb6f..47a0e4c3a2 100644 --- a/src/analyses/mallocWrapperAnalysis.ml +++ b/src/analyses/mallocWrapperAnalysis.ml @@ -1,4 +1,7 @@ -(** An analysis that handles the case when malloc is called from a wrapper function all over the code. *) +(** Analysis which provides symbolic heap locations for dynamic memory allocations. ([mallocWrapper]). + + Provided heap locations are based on the node and thread ID. + Considers [malloc] wrapper functions and a number of unique heap locations for additional precision. *) open GoblintCil open Analyses diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml index 73524c0c3c..8adffb4065 100644 --- a/src/analyses/malloc_null.ml +++ b/src/analyses/malloc_null.ml @@ -1,4 +1,4 @@ -(** Path-sensitive analysis that verifies checking the result of the malloc function. *) +(** Path-sensitive analysis of failed dynamic memory allocations ([malloc_null]). *) module AD = ValueDomain.AD module IdxDom = ValueDomain.IndexDomain diff --git a/src/analyses/mayLocks.ml b/src/analyses/mayLocks.ml index 182b93ff3e..d2edeba776 100644 --- a/src/analyses/mayLocks.ml +++ b/src/analyses/mayLocks.ml @@ -1,4 +1,6 @@ -(** May lockset analysis (unused). *) +(** May lockset analysis ([maylocks]). *) + +(* TODO: unused *) open Analyses diff --git a/src/analyses/modifiedSinceLongjmp.ml b/src/analyses/modifiedSinceLongjmp.ml index 926c256bd1..f489b08fe9 100644 --- a/src/analyses/modifiedSinceLongjmp.ml +++ b/src/analyses/modifiedSinceLongjmp.ml @@ -1,4 +1,6 @@ -(** Locally track the variables that may have been written since the corresponding jumpbuffer was set *) +(** Analysis of variables modified since [setjmp] ([modifiedSinceLongjmp]). *) + +(* TODO: this name is wrong *) open GoblintCil open Analyses diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 64663da235..775a0bae5e 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -1,4 +1,4 @@ -(** Protecting mutex analysis. Must locksets locally and for globals. *) +(** Must lockset and protecting lockset analysis ([mutex]). *) module M = Messages module Addr = ValueDomain.Addr diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml index b62c688af9..ff6fce9562 100644 --- a/src/analyses/mutexEventsAnalysis.ml +++ b/src/analyses/mutexEventsAnalysis.ml @@ -1,4 +1,6 @@ -(** Mutex events analysis (Lock and Unlock). *) +(** Mutex locking and unlocking analysis ([mutexEvents]). + + Emits {!Events.Lock} and {!Events.Unlock} to other analyses. *) module M = Messages module Addr = ValueDomain.Addr diff --git a/src/analyses/poisonVariables.ml b/src/analyses/poisonVariables.ml index ee2ad4e7aa..5cb34baa26 100644 --- a/src/analyses/poisonVariables.ml +++ b/src/analyses/poisonVariables.ml @@ -1,3 +1,5 @@ +(** Taint analysis of variables that were modified between [setjmp] and [longjmp] and not yet overwritten. ([poisonVariables]). *) + open Batteries open GoblintCil open Analyses diff --git a/src/analyses/pthreadSignals.ml b/src/analyses/pthreadSignals.ml index 7491e74b01..d49a8f12bc 100644 --- a/src/analyses/pthreadSignals.ml +++ b/src/analyses/pthreadSignals.ml @@ -1,4 +1,4 @@ -(** Analysis of must-received pthread_signals. *) +(** Must received signals analysis for Pthread condition variables ([pthreadSignals]). *) open GoblintCil open Analyses diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index d4a09125f1..099dc1bd62 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -1,4 +1,4 @@ -(** Data race analysis. *) +(** Data race analysis ([race]). *) open GoblintCil open Analyses diff --git a/src/analyses/region.ml b/src/analyses/region.ml index 17389b2184..33bef7e014 100644 --- a/src/analyses/region.ml +++ b/src/analyses/region.ml @@ -1,4 +1,6 @@ -(** Assigning static regions to dynamic memory. *) +(** Analysis of disjoint heap regions for dynamically allocated memory ([region]). + + @see Seidl, H., Vojdani, V. Region Analysis for Race Detection. *) open Batteries open GoblintCil diff --git a/src/analyses/spec.ml b/src/analyses/spec.ml index fc6913c743..ed3f0a9a56 100644 --- a/src/analyses/spec.ml +++ b/src/analyses/spec.ml @@ -1,4 +1,8 @@ -(** Analysis by specification file. *) +(** Analysis using finite automaton specification file ([spec]). + + @author Ralf Vogler + + @see Vogler, R. Verifying Regular Safety Properties of C Programs Using the Static Analyzer Goblint. Section 4. *) open Batteries open GoblintCil diff --git a/src/analyses/stackTrace.ml b/src/analyses/stackTrace.ml index 105f0c266b..d3dc0e6caf 100644 --- a/src/analyses/stackTrace.ml +++ b/src/analyses/stackTrace.ml @@ -1,4 +1,4 @@ -(** Stack-trace "analyses". *) +(** Call stack analyses ([stack_trace], [stack_trace_set], [stack_loc]). *) open GoblintCil open Analyses diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml index c29421a130..489fbda918 100644 --- a/src/analyses/symbLocks.ml +++ b/src/analyses/symbLocks.ml @@ -1,6 +1,6 @@ -(** Symbolic lock-sets for use in per-element patterns. +(** Symbolic lockset analysis for per-element (field or index) locking patterns ([symb_locks]). - See Section 5 and 6 in https://dl.acm.org/doi/10.1145/2970276.2970337 for more details. *) + @see Static race detection for device drivers: the Goblint approach. Section 5 and 6. *) module LF = LibraryFunctions module LP = SymbLocksDomain.LockingPattern diff --git a/src/analyses/taintPartialContexts.ml b/src/analyses/taintPartialContexts.ml index aa4990fdd9..5edeb1e403 100644 --- a/src/analyses/taintPartialContexts.ml +++ b/src/analyses/taintPartialContexts.ml @@ -1,3 +1,5 @@ +(** Taint analysis of variables modified in a function ([taintPartialContexts]). *) + (* TaintPartialContexts: Set of Lvalues, which are tainted at a specific Node. *) (* An Lvalue is tainted, if its Rvalue might have been altered in the context of the current function, implying that the Rvalue of any Lvalue not in the set has definitely not been changed within the current context. *) diff --git a/src/analyses/termination.ml b/src/analyses/termination.ml index 51826773e5..6da9225d3f 100644 --- a/src/analyses/termination.ml +++ b/src/analyses/termination.ml @@ -1,4 +1,4 @@ -(** Termination of loops. *) +(** Termination analysis of loops using counter variables ([term]). *) open Batteries open GoblintCil diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml index 97cb76a07c..275de3b005 100644 --- a/src/analyses/threadAnalysis.ml +++ b/src/analyses/threadAnalysis.ml @@ -1,4 +1,4 @@ -(** Thread creation and uniqueness analyses. *) +(** Created threads and their uniqueness analysis ([thread]). *) open GoblintCil open Analyses diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml index 2c3d9bb2f5..3dd6b9ec07 100644 --- a/src/analyses/threadEscape.ml +++ b/src/analyses/threadEscape.ml @@ -1,4 +1,4 @@ -(** Variables that escape threads using the last argument from pthread_create. *) +(** Escape analysis for thread-local variables ([escape]). *) open GoblintCil open Analyses diff --git a/src/analyses/threadFlag.ml b/src/analyses/threadFlag.ml index de50d6c192..15ac86a6dc 100644 --- a/src/analyses/threadFlag.ml +++ b/src/analyses/threadFlag.ml @@ -1,4 +1,4 @@ -(** Multi-threadedness analysis. *) +(** Multi-threadedness analysis ([threadflag]). *) module LF = LibraryFunctions diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml index 9ff781b160..ec10ec001c 100644 --- a/src/analyses/threadId.ml +++ b/src/analyses/threadId.ml @@ -1,4 +1,4 @@ -(** Current thread ID analysis. *) +(** Current thread ID analysis ([threadid]). *) module LF = LibraryFunctions diff --git a/src/analyses/threadJoins.ml b/src/analyses/threadJoins.ml index ea5b13934c..19433aae9f 100644 --- a/src/analyses/threadJoins.ml +++ b/src/analyses/threadJoins.ml @@ -1,4 +1,7 @@ -(** Thread join analysis. *) +(** Joined threads analysis ([threadJoins]). + + @see Schwarz, M., Saan, S., Seidl, H., Erhard, J., Vojdani, V. Clustered Relational Thread-Modular Abstract Interpretation with Local Traces. Appendix F. *) + open GoblintCil open Analyses diff --git a/src/analyses/threadReturn.ml b/src/analyses/threadReturn.ml index 0b4cc7c673..470c4ceaa8 100644 --- a/src/analyses/threadReturn.ml +++ b/src/analyses/threadReturn.ml @@ -1,4 +1,4 @@ -(** Thread returning analysis. *) +(** Thread returning analysis which abstracts a thread's call stack by a boolean, indicating whether it is at the topmost call stack frame or not ([threadreturn]). *) open GoblintCil open Analyses diff --git a/src/analyses/tutorials/constants.ml b/src/analyses/tutorials/constants.ml index 6ffeaaa874..e1d341e993 100644 --- a/src/analyses/tutorials/constants.ml +++ b/src/analyses/tutorials/constants.ml @@ -1,3 +1,4 @@ +(** Simple intraprocedural integer constants analysis example ([constants]). *) open GoblintCil open Analyses diff --git a/src/analyses/tutorials/signs.ml b/src/analyses/tutorials/signs.ml index ddbb3b035e..31168df86a 100644 --- a/src/analyses/tutorials/signs.ml +++ b/src/analyses/tutorials/signs.ml @@ -1,4 +1,6 @@ -(** An analysis specification for didactic purposes. *) +(** Simple intraprocedural integer signs analysis template ([signs]). + + @see *) open GoblintCil open Analyses diff --git a/src/analyses/tutorials/taint.ml b/src/analyses/tutorials/taint.ml index f01c2bdd70..217125c8bd 100644 --- a/src/analyses/tutorials/taint.ml +++ b/src/analyses/tutorials/taint.ml @@ -1,3 +1,5 @@ +(** Simple interprocedural taint analysis template ([taint]). *) + (** An analysis specification for didactic purposes. *) (* Helpful link on CIL: https://goblint.in.tum.de/assets/goblint-cil/ *) (* Goblint documentation: https://goblint.readthedocs.io/en/latest/ *) diff --git a/src/analyses/tutorials/unitAnalysis.ml b/src/analyses/tutorials/unitAnalysis.ml index 0a72cb1c89..d3b8c69bfd 100644 --- a/src/analyses/tutorials/unitAnalysis.ml +++ b/src/analyses/tutorials/unitAnalysis.ml @@ -1,4 +1,4 @@ -(** An analysis specification for didactic purposes. *) +(** Simplest possible analysis with unit domain ([unit]). *) open GoblintCil open Analyses diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml index 72cc1b78ce..4a02b41451 100644 --- a/src/analyses/unassumeAnalysis.ml +++ b/src/analyses/unassumeAnalysis.ml @@ -1,6 +1,7 @@ -(** Unassume analysis. +(** Unassume analysis ([unassume]). Emits unassume events for other analyses based on YAML witness invariants. *) + open Analyses module Cil = GoblintCil.Cil diff --git a/src/analyses/uninit.ml b/src/analyses/uninit.ml index cdb3124c87..9501c4a166 100644 --- a/src/analyses/uninit.ml +++ b/src/analyses/uninit.ml @@ -1,4 +1,4 @@ -(** Local variable initialization analysis. *) +(** Analysis of initialized local variables ([uninit]). *) module M = Messages module AD = ValueDomain.AD diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml index ad49a0d93d..7e310d9784 100644 --- a/src/analyses/varEq.ml +++ b/src/analyses/varEq.ml @@ -1,4 +1,4 @@ -(** Variable equalities necessary for per-element patterns. *) +(** Symbolic expression equalities analysis ([var_eq]). *) module Addr = ValueDomain.Addr module Offs = ValueDomain.Offs diff --git a/src/analyses/vla.ml b/src/analyses/vla.ml index 1b738d040f..865f22b20a 100644 --- a/src/analyses/vla.ml +++ b/src/analyses/vla.ml @@ -1,4 +1,4 @@ -(** An analysis to detect if an invocation is in the scope of a variably modified variable. *) +(** Analysis of variable-length arrays (VLAs) in scope ([vla]). *) open GoblintCil open Analyses diff --git a/src/autoTune.ml b/src/autoTune.ml index 79d85d8009..8ad5f8d655 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -1,3 +1,5 @@ +(** Autotuning of the configuration based on syntactic heuristics. *) + open GobConfig open GoblintCil open AutoTune0 diff --git a/src/cdomains/addressDomain.ml b/src/cdomains/addressDomain.ml index 1be584c2a5..02a52d00c2 100644 --- a/src/cdomains/addressDomain.ml +++ b/src/cdomains/addressDomain.ml @@ -1,3 +1,5 @@ +(** Domains for addresses/pointers. *) + open GoblintCil open IntOps diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index 72448c7415..6c24a46c6e 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -1,3 +1,7 @@ +(** OCaml implementation of the affine equalities domain. + + @see Karr, M. Affine relationships among variables of a program. *) + (** Abstract states in the newly added domain are represented by structs containing a matrix and an apron environment. Matrices are modeled as proposed by Karr: Each variable is assigned to a column and each row represents a linear affine relationship that must hold at the corresponding program point. The apron environment is hereby used to organize the order of columns and variables. *) diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml index eee8d50b60..d9928df597 100644 --- a/src/cdomains/apron/apronDomain.apron.ml +++ b/src/cdomains/apron/apronDomain.apron.ml @@ -1,3 +1,5 @@ +(** {!Apron} domains. *) + open Batteries open GoblintCil open Pretty diff --git a/src/cdomains/apron/relationDomain.apron.ml b/src/cdomains/apron/relationDomain.apron.ml index c13b44b075..c5b6a0a89b 100644 --- a/src/cdomains/apron/relationDomain.apron.ml +++ b/src/cdomains/apron/relationDomain.apron.ml @@ -1,4 +1,6 @@ -(** Interfaces/implementations that generalize the apronDomain and affineEqualityDomain. *) +(** Signatures for relational value domains. + + See {!ApronDomain} and {!AffineEqualityDomain}. *) open Batteries open GoblintCil diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index 9545c51a12..059a7f8264 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -1,4 +1,4 @@ -(** Functions and modules that are shared among the original apronDomain and the new affineEqualityDomain. *) +(** Relational value domain utilities. *) open GoblintCil open Batteries diff --git a/src/cdomains/arrayDomain.mli b/src/cdomains/arrayDomain.mli index 91e526235d..ebf265ac0b 100644 --- a/src/cdomains/arrayDomain.mli +++ b/src/cdomains/arrayDomain.mli @@ -1,3 +1,5 @@ +(** Abstract domains for C arrays. *) + open IntOps open GoblintCil module VDQ = ValueDomainQueries diff --git a/src/cdomains/baseDomain.ml b/src/cdomains/baseDomain.ml index 00c7e0a7c2..242d83e708 100644 --- a/src/cdomains/baseDomain.ml +++ b/src/cdomains/baseDomain.ml @@ -1,4 +1,4 @@ -(** domain of the base analysis *) +(** Full domain of {!Base} analysis. *) open GoblintCil module VD = ValueDomain.Compound diff --git a/src/cdomains/basetype.ml b/src/cdomains/basetype.ml index e241141a75..d576b803b6 100644 --- a/src/cdomains/basetype.ml +++ b/src/cdomains/basetype.ml @@ -1,3 +1,5 @@ +(** Printables and domains for some common types. *) + open GoblintCil diff --git a/src/cdomains/cilLval.ml b/src/cdomains/cilLval.ml index 74118785ef..9a86a3b083 100644 --- a/src/cdomains/cilLval.ml +++ b/src/cdomains/cilLval.ml @@ -1 +1,3 @@ +(** Domains for {!GoblintCil.lval}. *) + module Set = SetDomain.ToppedSet (CilType.Lval) (struct let topname = "All" end) diff --git a/src/cdomains/concDomain.ml b/src/cdomains/concDomain.ml index 94df15cb7a..b16cdf1d9f 100644 --- a/src/cdomains/concDomain.ml +++ b/src/cdomains/concDomain.ml @@ -1,3 +1,5 @@ +(** Domains for thread sets and their uniqueness. *) + module ThreadSet = SetDomain.ToppedSet (ThreadIdDomain.Thread) (struct let topname = "All Threads" end) module MustThreadSet = SetDomain.Reverse(ThreadSet) diff --git a/src/cdomains/deadlockDomain.ml b/src/cdomains/deadlockDomain.ml index 06fc16600c..1e62a48933 100644 --- a/src/cdomains/deadlockDomain.ml +++ b/src/cdomains/deadlockDomain.ml @@ -1,3 +1,5 @@ +(** Deadlock domain. *) + module Lock = LockDomain.Addr module LockEvent = Printable.Prod3 (Lock) (Node) (MCPAccess.A) diff --git a/src/cdomains/escapeDomain.ml b/src/cdomains/escapeDomain.ml index 4c2331d9ab..1e2769dcd7 100644 --- a/src/cdomains/escapeDomain.ml +++ b/src/cdomains/escapeDomain.ml @@ -1,3 +1,5 @@ +(** Domain for escaped thread-local variables. *) + module EscapedVars = struct include SetDomain.ToppedSet (Basetype.Variables) (struct let topname = "All Variables" end) diff --git a/src/cdomains/fileDomain.ml b/src/cdomains/fileDomain.ml index 775587da68..3a10d7f8b7 100644 --- a/src/cdomains/fileDomain.ml +++ b/src/cdomains/fileDomain.ml @@ -1,3 +1,5 @@ +(** Domains for file handles. *) + open Batteries module D = LvalMapDomain diff --git a/src/cdomains/flagModeDomain.ml b/src/cdomains/flagModeDomain.ml index 6d290fbf29..70ee6d0015 100644 --- a/src/cdomains/flagModeDomain.ml +++ b/src/cdomains/flagModeDomain.ml @@ -1,3 +1,5 @@ +(* TODO: unused *) + module Eq = IntDomain.MakeBooleans (struct let truename="==" let falsename="!=" end) module Method = IntDomain.MakeBooleans (struct let truename="guard" let falsename="assign" end) diff --git a/src/cdomains/floatDomain.mli b/src/cdomains/floatDomain.mli index 8be4304c5e..13df16aba6 100644 --- a/src/cdomains/floatDomain.mli +++ b/src/cdomains/floatDomain.mli @@ -1,5 +1,5 @@ -(** Abstract Domains for floats. These are domains that support the C - * operations on double/float values. *) +(** Abstract domains for C floating-point numbers. *) + open GoblintCil exception ArithmeticOnFloatBot of string @@ -9,67 +9,94 @@ module type FloatArith = sig val neg : t -> t (** Negating a float value: [-x] *) + val add : t -> t -> t (** Addition: [x + y] *) + val sub : t -> t -> t (** Subtraction: [x - y] *) + val mul : t -> t -> t (** Multiplication: [x * y] *) + val div : t -> t -> t (** Division: [x / y] *) + val fmax : t -> t -> t (** Maximum *) + val fmin : t -> t -> t (** Minimum *) - (** {unary functions} *) + (** {b Unary functions} *) + val ceil: t -> t - (* ceil(x) *) + (** ceil(x) *) + val floor: t -> t - (* floor(x) *) + (** floor(x) *) + val fabs : t -> t (** fabs(x) *) + val acos : t -> t (** acos(x) *) + val asin : t -> t (** asin(x) *) + val atan : t -> t (** atan(x) *) + val cos : t -> t (** cos(x) *) + val sin : t -> t (** sin(x) *) + val tan : t -> t (** tan(x) *) (** {b Comparison operators} *) + val lt : t -> t -> IntDomain.IntDomTuple.t (** Less than: [x < y] *) + val gt : t -> t -> IntDomain.IntDomTuple.t (** Greater than: [x > y] *) + val le : t -> t -> IntDomain.IntDomTuple.t (** Less than or equal: [x <= y] *) + val ge : t -> t -> IntDomain.IntDomTuple.t (** Greater than or equal: [x >= y] *) + val eq : t -> t -> IntDomain.IntDomTuple.t (** Equal to: [x == y] *) + val ne : t -> t -> IntDomain.IntDomTuple.t (** Not equal to: [x != y] *) + val unordered: t -> t -> IntDomain.IntDomTuple.t (** Unordered *) - (** {unary functions returning int} *) + (** {b Unary functions returning [int]} *) + val isfinite : t -> IntDomain.IntDomTuple.t - (** __builtin_isfinite(x) *) + (** [__builtin_isfinite(x)] *) + val isinf : t -> IntDomain.IntDomTuple.t - (** __builtin_isinf(x) *) + (** [__builtin_isinf(x)] *) + val isnan : t -> IntDomain.IntDomTuple.t - (** __builtin_isnan(x) *) + (** [__builtin_isnan(x)] *) + val isnormal : t -> IntDomain.IntDomTuple.t - (** __builtin_isnormal(x) *) + (** [__builtin_isnormal(x)] *) + val signbit : t -> IntDomain.IntDomTuple.t - (** __builtin_signbit(x) *) + (** [__builtin_signbit(x)] *) end module type FloatDomainBase = sig diff --git a/src/cdomains/floatOps/floatOps.mli b/src/cdomains/floatOps/floatOps.mli index 1bfd04fca3..05bf363872 100644 --- a/src/cdomains/floatOps/floatOps.mli +++ b/src/cdomains/floatOps/floatOps.mli @@ -1,3 +1,5 @@ +(** Unified interface for floating-point types. *) + type round_mode = | Nearest | ToZero diff --git a/src/cdomains/intDomain.mli b/src/cdomains/intDomain.mli index 4671fb3013..a853c8acca 100644 --- a/src/cdomains/intDomain.mli +++ b/src/cdomains/intDomain.mli @@ -1,5 +1,5 @@ -(** Abstract Domains for integers. These are domains that support the C - * operations on integer values. *) +(** Abstract domains for C integers. *) + open GoblintCil val should_wrap: Cil.ikind -> bool diff --git a/src/cdomains/jmpBufDomain.ml b/src/cdomains/jmpBufDomain.ml index 4188ff55a6..3c94fa8f47 100644 --- a/src/cdomains/jmpBufDomain.ml +++ b/src/cdomains/jmpBufDomain.ml @@ -1,3 +1,5 @@ +(** Domains for [setjmp] and [longjmp] analyses, and [setjmp] buffers. *) + module BufferEntry = Printable.ProdSimple(Node)(ControlSpecC) module BufferEntryOrTop = struct diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml index 0ebcf4a8a5..6a4649b002 100644 --- a/src/cdomains/lockDomain.ml +++ b/src/cdomains/lockDomain.ml @@ -1,3 +1,5 @@ +(** Lockset domains. *) + module Addr = ValueDomain.Addr module Offs = ValueDomain.Offs module Equ = MusteqDomain.Equ diff --git a/src/cdomains/lval.ml b/src/cdomains/lval.ml index e6143e0de9..ea4acac920 100644 --- a/src/cdomains/lval.ml +++ b/src/cdomains/lval.ml @@ -1,3 +1,5 @@ +(** Domains for offsets and lvalues. *) + open GoblintCil open Pretty diff --git a/src/cdomains/lvalMapDomain.ml b/src/cdomains/lvalMapDomain.ml index 4b35ecdd8b..5a8f31764a 100644 --- a/src/cdomains/lvalMapDomain.ml +++ b/src/cdomains/lvalMapDomain.ml @@ -1,3 +1,5 @@ +(** Domains for lvalue maps. *) + open Batteries open GoblintCil diff --git a/src/cdomains/mHP.ml b/src/cdomains/mHP.ml index 9bcd9d739f..8037cfa21d 100644 --- a/src/cdomains/mHP.ml +++ b/src/cdomains/mHP.ml @@ -1,3 +1,5 @@ +(** May-happen-in-parallel (MHP) domain. *) + include Printable.Std let name () = "mhp" diff --git a/src/cdomains/musteqDomain.ml b/src/cdomains/musteqDomain.ml index bf3d694c23..13acbca5fe 100644 --- a/src/cdomains/musteqDomain.ml +++ b/src/cdomains/musteqDomain.ml @@ -1,3 +1,5 @@ +(** Symbolic lvalue equalities domain. *) + open GoblintCil open Pretty diff --git a/src/cdomains/pthreadDomain.ml b/src/cdomains/pthreadDomain.ml index f16bf29722..8cef57bdbd 100644 --- a/src/cdomains/pthreadDomain.ml +++ b/src/cdomains/pthreadDomain.ml @@ -1,3 +1,5 @@ +(** Domains for extraction of Pthread programs. *) + open Batteries (** Thread ID *) diff --git a/src/cdomains/regionDomain.ml b/src/cdomains/regionDomain.ml index 672aa90c82..9788beec61 100644 --- a/src/cdomains/regionDomain.ml +++ b/src/cdomains/regionDomain.ml @@ -1,3 +1,5 @@ +(** Domains for disjoint heap regions. *) + open GoblintCil open GobConfig diff --git a/src/cdomains/specDomain.ml b/src/cdomains/specDomain.ml index 7194b83071..364657d2f7 100644 --- a/src/cdomains/specDomain.ml +++ b/src/cdomains/specDomain.ml @@ -1,3 +1,5 @@ +(** Domains for finite automaton specification file analysis. *) + open Batteries module D = LvalMapDomain diff --git a/src/cdomains/stackDomain.ml b/src/cdomains/stackDomain.ml index 98e46b1571..3a83c78503 100644 --- a/src/cdomains/stackDomain.ml +++ b/src/cdomains/stackDomain.ml @@ -1,3 +1,5 @@ +(** Call stack domains. *) + module type S = sig include Lattice.S diff --git a/src/cdomains/structDomain.mli b/src/cdomains/structDomain.mli index d83d807096..15b75c6d41 100644 --- a/src/cdomains/structDomain.mli +++ b/src/cdomains/structDomain.mli @@ -1,4 +1,4 @@ -(** Abstract domains representing structs. *) +(** Abstract domains for C structs. *) open GoblintCil diff --git a/src/cdomains/symbLocksDomain.ml b/src/cdomains/symbLocksDomain.ml index 20c5a5a86d..e67be76ea5 100644 --- a/src/cdomains/symbLocksDomain.ml +++ b/src/cdomains/symbLocksDomain.ml @@ -1,3 +1,5 @@ +(** Symbolic lockset domain. *) + open GoblintCil module M = Messages diff --git a/src/cdomains/threadFlagDomain.ml b/src/cdomains/threadFlagDomain.ml index 09d19d9e74..80ba9b7a52 100644 --- a/src/cdomains/threadFlagDomain.ml +++ b/src/cdomains/threadFlagDomain.ml @@ -1,3 +1,5 @@ +(** Multi-threadedness flag domains. *) + module type S = sig include Lattice.S diff --git a/src/cdomains/threadIdDomain.ml b/src/cdomains/threadIdDomain.ml index 57e8b443dc..b81a86811a 100644 --- a/src/cdomains/threadIdDomain.ml +++ b/src/cdomains/threadIdDomain.ml @@ -1,3 +1,5 @@ +(** Thread ID domains. *) + open GoblintCil open FlagHelper diff --git a/src/cdomains/unionDomain.ml b/src/cdomains/unionDomain.ml index d2657621e7..08efecf421 100644 --- a/src/cdomains/unionDomain.ml +++ b/src/cdomains/unionDomain.ml @@ -1,3 +1,5 @@ +(** Abstract domains for C unions. *) + open GoblintCil module type Arg = diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml index 6d5b06bcec..544ac9f27a 100644 --- a/src/cdomains/valueDomain.ml +++ b/src/cdomains/valueDomain.ml @@ -1,3 +1,5 @@ +(** Domain for a single {!Base} analysis value. *) + open GoblintCil open Pretty open PrecisionUtil diff --git a/src/cdomains/vectorMatrix.ml b/src/cdomains/vectorMatrix.ml index a1e554d131..d652145032 100644 --- a/src/cdomains/vectorMatrix.ml +++ b/src/cdomains/vectorMatrix.ml @@ -1,3 +1,5 @@ +(** OCaml implementations of vectors and matrices. *) + open Batteries module Array = Batteries.Array module M = Messages diff --git a/src/domains/abstractionDomainProperties.ml b/src/domains/abstractionDomainProperties.ml index 208e433e86..1772af0b6b 100644 --- a/src/domains/abstractionDomainProperties.ml +++ b/src/domains/abstractionDomainProperties.ml @@ -1,3 +1,5 @@ +(** QCheck properties for abstract operations. *) + module type AbstractFunction = sig type c diff --git a/src/domains/access.ml b/src/domains/access.ml index 8d9d585015..c40e6f136c 100644 --- a/src/domains/access.ml +++ b/src/domains/access.ml @@ -1,3 +1,5 @@ +(** Memory accesses and their manipulation. *) + open Batteries open GoblintCil open Pretty diff --git a/src/domains/accessDomain.ml b/src/domains/accessDomain.ml index 3c4813299e..5884214976 100644 --- a/src/domains/accessDomain.ml +++ b/src/domains/accessDomain.ml @@ -1,3 +1,5 @@ +(** Domain for memory accesses. *) + open GoblintCil.Pretty module Event = diff --git a/src/domains/accessKind.ml b/src/domains/accessKind.ml index dbaeec0f2f..576581af02 100644 --- a/src/domains/accessKind.ml +++ b/src/domains/accessKind.ml @@ -1,3 +1,5 @@ +(** Kinds of memory accesses. *) + type t = | Write (** argument may be read or written to *) | Read (** argument may be read *) diff --git a/src/domains/boolDomain.ml b/src/domains/boolDomain.ml index 4fe060a961..e088c3605c 100644 --- a/src/domains/boolDomain.ml +++ b/src/domains/boolDomain.ml @@ -1,3 +1,5 @@ +(** Boolean domains. *) + module Bool = struct include Basetype.RawBools diff --git a/src/domains/domainProperties.ml b/src/domains/domainProperties.ml index 38f32ea059..b2f0f7671a 100644 --- a/src/domains/domainProperties.ml +++ b/src/domains/domainProperties.ml @@ -1,3 +1,5 @@ +(** QCheck properties for lattice properties. *) + open QCheck module DomainTest (D: Lattice.S) = diff --git a/src/domains/events.ml b/src/domains/events.ml index 07cce9feab..2141ad17dd 100644 --- a/src/domains/events.ml +++ b/src/domains/events.ml @@ -1,3 +1,5 @@ +(** Events. *) + open GoblintCil open Pretty diff --git a/src/domains/flagHelper.ml b/src/domains/flagHelper.ml index 7ddf493048..933d371f48 100644 --- a/src/domains/flagHelper.ml +++ b/src/domains/flagHelper.ml @@ -1,3 +1,5 @@ +(** Domain alternatives chosen by a runtime flag. *) + module type FlagError = sig val msg: string val name: string diff --git a/src/domains/intDomainProperties.ml b/src/domains/intDomainProperties.ml index a40862b446..9dcb867efc 100644 --- a/src/domains/intDomainProperties.ml +++ b/src/domains/intDomainProperties.ml @@ -1,3 +1,5 @@ +(** QCheck properties for {!IntDomain}. *) + open GoblintCil module BI = IntOps.BigIntOps diff --git a/src/domains/invariant.ml b/src/domains/invariant.ml index ff50aa801e..042554c4e3 100644 --- a/src/domains/invariant.ml +++ b/src/domains/invariant.ml @@ -1,3 +1,5 @@ +(** Invariants for witnesses. *) + open GoblintCil (** Symbolic (and fully syntactic) expression "lattice". *) diff --git a/src/domains/invariantCil.ml b/src/domains/invariantCil.ml index 2e647f6920..8a1d8f0745 100644 --- a/src/domains/invariantCil.ml +++ b/src/domains/invariantCil.ml @@ -1,3 +1,5 @@ +(** Invariant manipulation related to CIL transformations. *) + open GoblintCil diff --git a/src/domains/lattice.ml b/src/domains/lattice.ml index f1657b32ca..14422c1431 100644 --- a/src/domains/lattice.ml +++ b/src/domains/lattice.ml @@ -1,4 +1,5 @@ -(** The lattice signature and simple functors for building lattices. *) +(** Signature for lattices. + Functors for common lattices. *) module Pretty = GoblintCil.Pretty diff --git a/src/domains/mapDomain.ml b/src/domains/mapDomain.ml index 9051074230..3dcb4f8d17 100644 --- a/src/domains/mapDomain.ml +++ b/src/domains/mapDomain.ml @@ -1,4 +1,4 @@ -(** Specification and functors for maps. *) +(** Map domains. *) module Pretty = GoblintCil.Pretty open Pretty diff --git a/src/domains/myCheck.ml b/src/domains/myCheck.ml index cc5782997e..98583cd2c3 100644 --- a/src/domains/myCheck.ml +++ b/src/domains/myCheck.ml @@ -1,3 +1,5 @@ +(** {!QCheck} extensions. *) + open QCheck let shrink arb = BatOption.default Shrink.nil arb.shrink diff --git a/src/domains/printable.ml b/src/domains/printable.ml index 4f68bc29a5..495d294e6e 100644 --- a/src/domains/printable.ml +++ b/src/domains/printable.ml @@ -1,4 +1,5 @@ -(** Some things are not quite lattices ... *) +(** Signature for comparable and outputtable elements. + Functors for common printables. *) module Pretty = GoblintCil.Pretty open Pretty diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 171eaaf083..2d1b25eca9 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -1,4 +1,4 @@ -(** Structures for the querying subsystem. *) +(** Queries and their result lattices. *) open GoblintCil diff --git a/src/domains/setDomain.ml b/src/domains/setDomain.ml index 69196fb8df..1b5239de80 100644 --- a/src/domains/setDomain.ml +++ b/src/domains/setDomain.ml @@ -1,4 +1,5 @@ -(** Abstract domains representing sets. *) +(** Set domains. *) + module Pretty = GoblintCil.Pretty open Pretty diff --git a/src/domains/valueDomainQueries.ml b/src/domains/valueDomainQueries.ml index 5f95320cfe..c89e491e58 100644 --- a/src/domains/valueDomainQueries.ml +++ b/src/domains/valueDomainQueries.ml @@ -1,3 +1,5 @@ +(** Queries within {!ValueDomain}. *) + open GoblintCil open BoolDomain diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index f7c4253b76..30486825df 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -1,4 +1,4 @@ -(** Signatures for analyzers, analysis specifications, and result output. *) +(** {{!Spec} Analysis specification} and {{!MonSystem} constraint system} signatures. *) open Batteries open GoblintCil diff --git a/src/framework/analysisState.ml b/src/framework/analysisState.ml index b57d2bc341..0f3a9f55bc 100644 --- a/src/framework/analysisState.ml +++ b/src/framework/analysisState.ml @@ -1,3 +1,5 @@ +(** Global flags for analysis state. *) + (** If this is true we output messages and collect accesses. This is set to true in control.ml before we verify the result (or already before solving if warn = 'early') *) let should_warn = ref false diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml index 626758a994..e61a208bc3 100644 --- a/src/framework/cfgTools.ml +++ b/src/framework/cfgTools.ml @@ -1,3 +1,5 @@ +(** Construction and output of CFGs. *) + open MyCFG open GoblintCil open Pretty diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index d00a530e07..69a820e67e 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -1,4 +1,5 @@ -(** How to generate constraints for a solver using specifications described in [Analyses]. *) +(** Construction of a {{!Analyses.MonSystem} constraint system} from an {{!Analyses.Spec} analysis specification} and {{!MyCFG.CfgBackward} CFGs}. + Transformatons of analysis specifications as functors. *) open Batteries open GoblintCil diff --git a/src/framework/control.ml b/src/framework/control.ml index 5de5b6f692..35cadfc12d 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -1,3 +1,5 @@ +(** Main internal functionality: analysis of the program by abstract interpretation via constraint solving. *) + (** An analyzer that takes the CFG from [MyCFG], a solver from [Selector], constraints from [Constraints] (using the specification from [MCP]) *) open Batteries diff --git a/src/framework/controlSpecC.mli b/src/framework/controlSpecC.mli index 47f37b5c88..330fd4bf73 100644 --- a/src/framework/controlSpecC.mli +++ b/src/framework/controlSpecC.mli @@ -1,3 +1,5 @@ +(** {{!Analyses.Spec.C} Context module} for the dynamically composed analysis. *) + (** Top-level Control Spec context as static module, which delegates to {!control_spec_c}. This allows using top-level context values inside individual analyses. *) include Printable.S diff --git a/src/framework/edge.ml b/src/framework/edge.ml index 87b9c45a3f..e6f214a4c8 100644 --- a/src/framework/edge.ml +++ b/src/framework/edge.ml @@ -1,3 +1,6 @@ +(** CFG edge. + Corresponds to a (primitive) program statement between program points (and their states). *) + open GoblintCil open Pretty diff --git a/src/framework/myCFG.ml b/src/framework/myCFG.ml index 1b5ffba98b..76675f3c88 100644 --- a/src/framework/myCFG.ml +++ b/src/framework/myCFG.ml @@ -1,4 +1,6 @@ -(** Our Control-flow graph implementation. *) +(** Control-flow graph. + + Distinct from CIL's CFG. *) open GoblintCil diff --git a/src/framework/node.ml b/src/framework/node.ml index e3493e5a6e..906f9e1d77 100644 --- a/src/framework/node.ml +++ b/src/framework/node.ml @@ -1,3 +1,6 @@ +(** CFG node. + Corresponds to a program point between program statements. *) + open GoblintCil open Pretty diff --git a/src/framework/refinement.ml b/src/framework/refinement.ml index e23aea0095..8c6181b9d6 100644 --- a/src/framework/refinement.ml +++ b/src/framework/refinement.ml @@ -1,3 +1,5 @@ +(** Experimental analysis refinement. *) + (** Restarts the analysis from scratch in Control. Its raiser is expected to have modified modified some global state to do a more precise analysis next time. diff --git a/src/framework/resultQuery.ml b/src/framework/resultQuery.ml index 63b0765fdb..ce5839ef30 100644 --- a/src/framework/resultQuery.ml +++ b/src/framework/resultQuery.ml @@ -1,3 +1,5 @@ +(** Perform {{!Queries.t} queries} on the constraint system solution. *) + open Analyses module Query (SpecSys: SpecSys) = diff --git a/src/framework/varQuery.mli b/src/framework/varQuery.mli index 77894b62ef..86abc389fc 100644 --- a/src/framework/varQuery.mli +++ b/src/framework/varQuery.mli @@ -1,3 +1,5 @@ +(** Queries for constraint variables related to semantic elements. *) + open GoblintCil type t = diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml new file mode 100644 index 0000000000..ea0d0420a1 --- /dev/null +++ b/src/goblint_lib.ml @@ -0,0 +1,471 @@ + +(** {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 Constraints = Constraints +module AnalysisState = AnalysisState +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 ResultQuery = ResultQuery +module VarQuery = VarQuery + +(** {2 Configuration} + + Runtime configuration is represented as JSON. + Options are specified and documented by the JSON schema [src/util/options.schema.json]. *) + +module GobConfig = GobConfig +module AfterConfig = AfterConfig + +module AutoTune = AutoTune + +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 VarEq = VarEq +module CondVars = CondVars + +(** {2 Heap} + + Analyses related to the heap. *) + +module MallocWrapperAnalysis = MallocWrapperAnalysis +module Region = Region +module MallocFresh = MallocFresh +module Malloc_null = Malloc_null + +(** {2 Concurrency} + + Analyses related to concurrency. *) + +(** {3 Locks} + + Analyses related to locking. *) + +module MutexEventsAnalysis = MutexEventsAnalysis +module LocksetAnalysis = LocksetAnalysis +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 ModifiedSinceLongjmp = ModifiedSinceLongjmp +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 FileUse = FileUse +module Uninit = Uninit +module Termination = Termination +module Expsplit = Expsplit +module StackTrace = StackTrace +module Spec = Spec + +(** {2 Helper} + + Analyses which only support other analyses. *) + +module AccessAnalysis = AccessAnalysis +module TaintPartialContexts = TaintPartialContexts +module UnassumeAnalysis = UnassumeAnalysis +module ExpRelation = ExpRelation +module AbortUnless = AbortUnless + + +(** {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 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. *) + +module BaseDomain = BaseDomain +module ValueDomain = ValueDomain +module IntDomain = IntDomain +module FloatDomain = FloatDomain +module AddressDomain = AddressDomain +module StructDomain = StructDomain +module UnionDomain = UnionDomain +module ArrayDomain = ArrayDomain +module JmpBufDomain = JmpBufDomain +module ValueDomainQueries = ValueDomainQueries + +(** {4 Relational} + + Domains for {!RelationAnalysis}. *) + +module RelationDomain = RelationDomain +module ApronDomain = ApronDomain +module AffineEqualityDomain = AffineEqualityDomain + +(** {3 Concurrency} *) + +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 CilLval = CilLval +module Access = Access +module AccessDomain = AccessDomain + +module MusteqDomain = MusteqDomain +module RegionDomain = RegionDomain +module FileDomain = FileDomain +module StackDomain = StackDomain + +module LvalMapDomain = LvalMapDomain +module SpecDomain = SpecDomain + +(** {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 Solvers} + + Generic solvers are used to solve {{!Analyses.MonSystem} (side-effecting) constraint systems}. *) + +(** {2 Top-down} + + The top-down solver family. *) + +module Td3 = Td3 +module TopDown = TopDown +module TopDown_term = TopDown_term +module TopDown_space_cache_term = TopDown_space_cache_term +module TopDown_deprecated = TopDown_deprecated + +(** {2 SLR} + + The SLR solver family. *) + +module SLRphased = SLRphased +module SLRterm = SLRterm +module SLR = SLR + +(** {2 Other} *) + +module EffectWConEq = EffectWConEq +module Worklist = Worklist +module Generic = Generic +module Selector = Selector + +module PostSolver = PostSolver +module LocalFixpoint = LocalFixpoint +module SolverStats = SolverStats +module SolverBox = SolverBox + + +(** {1 I/O} + + Various input/output interfaces and formats. *) + +module Messages = Messages +module Tracing = Tracing + +(** {2 Front-end} + + The following modules handle program input. *) + +module Preprocessor = Preprocessor +module CompilationDatabase = CompilationDatabase +module MakefileUtil = MakefileUtil + +(** {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 WitnessConstraints = WitnessConstraints +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 +module WideningTokens = WideningTokens + +(** {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 XmlUtil = XmlUtil + +(** {2 CIL} *) + +module CilType = CilType +module Cilfacade = Cilfacade +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 BaseInvariant = BaseInvariant +module CommonPriv = CommonPriv +module WideningThresholds = WideningThresholds + +module VectorMatrix = VectorMatrix +module SharedFunctions = SharedFunctions + +(** {2 Precision comparison} *) + +module PrecCompare = PrecCompare +module PrecCompareUtil = PrecCompareUtil +module PrivPrecCompareUtil = PrivPrecCompareUtil +module RelationPrecCompareUtil = RelationPrecCompareUtil +module ApronPrecCompareUtil = ApronPrecCompareUtil + +(** {2 Build info} *) + +(** OCaml compiler info. *) +module ConfigOcaml = ConfigOcaml + +(** Dune profile info. *) +module ConfigProfile = ConfigProfile + +(** Goblint version info. *) +module Version = Version + +(** Goblint git version info. *) +module ConfigVersion = ConfigVersion + + +(** {1 Library extensions} + + OCaml library extensions which are completely independent of Goblint. *) + +(** {2 Standard library} + + OCaml standard library extensions which are not provided by {!Batteries}. *) + +module GobFormat = GobFormat +module GobGc = GobGc +module GobHashtbl = GobHashtbl +module GobList = GobList +module GobRef = GobRef +module GobResult = GobResult +module GobOption = GobOption +module GobSys = GobSys +module GobUnix = GobUnix + +(** {2 Other libraries} + + External library extensions. *) + +module GobFpath = GobFpath +module GobPretty = GobPretty +module GobYaml = GobYaml +module GobYojson = GobYojson +module GobZ = GobZ +module MyCheck = MyCheck diff --git a/src/incremental/compareAST.ml b/src/incremental/compareAST.ml index ce71b43392..28dce7a8c6 100644 --- a/src/incremental/compareAST.ml +++ b/src/incremental/compareAST.ml @@ -1,3 +1,5 @@ +(** Comparison of CIL ASTs. *) + open GoblintCil open CilMaps diff --git a/src/incremental/compareCFG.ml b/src/incremental/compareCFG.ml index 93bb855606..e822166d38 100644 --- a/src/incremental/compareCFG.ml +++ b/src/incremental/compareCFG.ml @@ -1,3 +1,5 @@ +(** Comparison of CFGs. *) + open MyCFG open Queue open GoblintCil diff --git a/src/incremental/compareCIL.ml b/src/incremental/compareCIL.ml index b218cb18e0..1a83048b6c 100644 --- a/src/incremental/compareCIL.ml +++ b/src/incremental/compareCIL.ml @@ -1,3 +1,5 @@ +(** Comparison of CIL files. *) + open GoblintCil open MyCFG open CilMaps diff --git a/src/incremental/makefileUtil.ml b/src/incremental/makefileUtil.ml index 6893b8aecf..843981ee38 100644 --- a/src/incremental/makefileUtil.ml +++ b/src/incremental/makefileUtil.ml @@ -1,3 +1,5 @@ +(** Input program from a real-world project using a Makefile. *) + open Unix let buff_size = 1024 diff --git a/src/incremental/maxIdUtil.ml b/src/incremental/maxIdUtil.ml index 7854fd8a59..a5c4fdda61 100644 --- a/src/incremental/maxIdUtil.ml +++ b/src/incremental/maxIdUtil.ml @@ -1,3 +1,5 @@ +(** Tracking of maximum CIL IDs in use. *) + open GoblintCil type max_ids = { diff --git a/src/incremental/serialize.ml b/src/incremental/serialize.ml index 63e94e730d..bddf3aa383 100644 --- a/src/incremental/serialize.ml +++ b/src/incremental/serialize.ml @@ -1,3 +1,5 @@ +(** Serialization/deserialization of incremental analysis data. *) + open Batteries (* TODO: GoblintDir *) diff --git a/src/incremental/updateCil.ml b/src/incremental/updateCil.ml index 2f9628b4c1..60a3379ec1 100644 --- a/src/incremental/updateCil.ml +++ b/src/incremental/updateCil.ml @@ -1,3 +1,5 @@ +(** Combination of CIL files using comparison results. *) + open GoblintCil open CompareCIL open MaxIdUtil diff --git a/src/maingoblint.ml b/src/maingoblint.ml index a32cdaa015..8944d87ea0 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -1,4 +1,4 @@ -(** This is the main program! *) +(** Main external executable functionality: command-line, front-end and analysis execution. *) open Batteries open GobConfig diff --git a/src/solvers/effectWConEq.ml b/src/solvers/effectWConEq.ml index f0bea7ba11..c6dcf8f0e9 100644 --- a/src/solvers/effectWConEq.ml +++ b/src/solvers/effectWConEq.ml @@ -1,3 +1,5 @@ +(** ([effectWConEq]). *) + open Batteries open Analyses open Constraints diff --git a/src/solvers/generic.ml b/src/solvers/generic.ml index e29fc60c27..2569341dd1 100644 --- a/src/solvers/generic.ml +++ b/src/solvers/generic.ml @@ -1,3 +1,5 @@ +(** Various simple/old solvers and solver utilities. *) + open Batteries open GobConfig open Analyses diff --git a/src/solvers/postSolver.ml b/src/solvers/postSolver.ml index 55da3fcab3..346ce312b1 100644 --- a/src/solvers/postSolver.ml +++ b/src/solvers/postSolver.ml @@ -1,3 +1,5 @@ +(** Extra constraint system evaluation pass for warning generation, verification, pruning, etc. *) + open Batteries open Analyses open GobConfig diff --git a/src/solvers/sLR.ml b/src/solvers/sLR.ml index fed09d84ab..4904731b61 100644 --- a/src/solvers/sLR.ml +++ b/src/solvers/sLR.ml @@ -1,4 +1,6 @@ -(** The 'slr*' solvers. *) +(** Various SLR solvers. + + @see Apinis, K. Frameworks for analyzing multi-threaded C. *) open Batteries open Analyses diff --git a/src/solvers/sLRphased.ml b/src/solvers/sLRphased.ml index e3803c1764..f4c3389f1d 100644 --- a/src/solvers/sLRphased.ml +++ b/src/solvers/sLRphased.ml @@ -1,3 +1,5 @@ +(** Two-phased terminating SLR3 solver ([slr3tp]). *) + open Batteries open Analyses open Constraints diff --git a/src/solvers/sLRterm.ml b/src/solvers/sLRterm.ml index deb18ccd73..d4f4671c46 100644 --- a/src/solvers/sLRterm.ml +++ b/src/solvers/sLRterm.ml @@ -1,3 +1,6 @@ +(** Terminating SLR3 solver ([slr3t]). + Simpler version of {!SLRphased} without phases. *) + open Batteries open Analyses open Constraints diff --git a/src/solvers/selector.ml b/src/solvers/selector.ml index 5d15c5d9f9..664cbe0513 100644 --- a/src/solvers/selector.ml +++ b/src/solvers/selector.ml @@ -1,3 +1,5 @@ +(** Solver, which delegates at runtime to the configured solver. *) + open Batteries open Analyses open GobConfig diff --git a/src/solvers/solverBox.ml b/src/solvers/solverBox.ml index a261570e74..6472dd7870 100644 --- a/src/solvers/solverBox.ml +++ b/src/solvers/solverBox.ml @@ -1,3 +1,5 @@ +(** Box operator for warrowing solvers. *) + module type S = functor (D: Lattice.S) -> sig diff --git a/src/solvers/solverStats.ml b/src/solvers/solverStats.ml index 4f8cc3b22b..f8429f0868 100644 --- a/src/solvers/solverStats.ml +++ b/src/solvers/solverStats.ml @@ -1,3 +1,4 @@ +(** Statistics for solvers. *) let vars = ref 0 let evals = ref 0 diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 36f43693af..f0a728f73b 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -1,3 +1,8 @@ +(** Incremental/interactive terminating top-down solver, which supports space-efficiency and caching ([td3]). + + @see Seidl, H., Vogler, R. Three improvements to the top-down solver. + @see Interactive Abstract Interpretation: Reanalyzing Whole Programs for Cheap. *) + (** Incremental terminating top down solver that optionally only keeps values at widening points and restores other values afterwards. *) (* Incremental: see paper 'Incremental Abstract Interpretation' https://link.springer.com/chapter/10.1007/978-3-030-41103-9_5 *) (* TD3: see paper 'Three Improvements to the Top-Down Solver' https://dl.acm.org/doi/10.1145/3236950.3236967 diff --git a/src/solvers/topDown.ml b/src/solvers/topDown.ml index d1cf99199d..c6b20d28db 100644 --- a/src/solvers/topDown.ml +++ b/src/solvers/topDown.ml @@ -1,4 +1,5 @@ -(** Top down solver using box/warrow. This is superseded by td3 but kept as a simple version without term & space (& incremental). *) +(** Warrowing top-down solver ([topdown]). + Simpler version of {!Td3} without terminating, space-efficiency and incremental. *) open Batteries open Analyses diff --git a/src/solvers/topDown_deprecated.ml b/src/solvers/topDown_deprecated.ml index 2e7e276128..1f51244458 100644 --- a/src/solvers/topDown_deprecated.ml +++ b/src/solvers/topDown_deprecated.ml @@ -1,3 +1,5 @@ +(** Deprecated top-down solver ([topdown_deprecated]). *) + open Batteries open Analyses open Constraints diff --git a/src/solvers/topDown_space_cache_term.ml b/src/solvers/topDown_space_cache_term.ml index 0074401989..a78d90559d 100644 --- a/src/solvers/topDown_space_cache_term.ml +++ b/src/solvers/topDown_space_cache_term.ml @@ -1,5 +1,5 @@ -(** Terminating top down solver that only keeps values at widening points and restores other values afterwards. *) -(* This is superseded by td3 but kept as a simpler version without the incremental parts. *) +(** Terminating top-down solver, which supports space-efficiency and caching ([topdown_space_cache_term]). + Simpler version of {!Td3} without incremental. *) open Batteries open Analyses diff --git a/src/solvers/topDown_term.ml b/src/solvers/topDown_term.ml index 577e7ea814..ec07995586 100644 --- a/src/solvers/topDown_term.ml +++ b/src/solvers/topDown_term.ml @@ -1,4 +1,5 @@ -(** Top down solver. *) +(** Terminating top-down solver ([topdown_term]). + Simpler version of {!Td3} without space-efficiency and incremental. *) open Batteries open Analyses diff --git a/src/solvers/worklist.ml b/src/solvers/worklist.ml index 138024f137..b525764c74 100644 --- a/src/solvers/worklist.ml +++ b/src/solvers/worklist.ml @@ -1,3 +1,5 @@ +(** Worklist solver ([WL]). *) + open Batteries open Analyses open Constraints diff --git a/src/transform/deadCode.ml b/src/transform/deadCode.ml index cc6c1d928d..1b9db8d06a 100644 --- a/src/transform/deadCode.ml +++ b/src/transform/deadCode.ml @@ -1,3 +1,5 @@ +(** Dead code elimination transformation ([remove_dead_code]). *) + open Batteries open GoblintCil open GobConfig diff --git a/src/transform/evalAssert.ml b/src/transform/evalAssert.ml index 4ebb4190bf..fbfbce68d9 100644 --- a/src/transform/evalAssert.ml +++ b/src/transform/evalAssert.ml @@ -1,3 +1,5 @@ +(** Transformation for instrumenting the program with computed invariants as assertions ([assert]). *) + open GoblintCil open Formatcil diff --git a/src/transform/expressionEvaluation.ml b/src/transform/expressionEvaluation.ml index 397206a873..815e5742f6 100644 --- a/src/transform/expressionEvaluation.ml +++ b/src/transform/expressionEvaluation.ml @@ -1,3 +1,6 @@ +(** Transformation for evaluating expressions on the analysis results ([expeval]). + {e Hack for Gobview}. *) + open Batteries open GoblintCil open Syntacticsearch diff --git a/src/transform/transform.ml b/src/transform/transform.ml index c508da703d..fe3abb6f08 100644 --- a/src/transform/transform.ml +++ b/src/transform/transform.ml @@ -1,3 +1,5 @@ +(** Signatures and registry for transformations. *) + open GoblintCil module M = Messages diff --git a/src/util/afterConfig.ml b/src/util/afterConfig.ml index a49e4f31cc..ddc544ef0b 100644 --- a/src/util/afterConfig.ml +++ b/src/util/afterConfig.ml @@ -1,3 +1,5 @@ +(** Hooks which run after the runtime configuration is fully loaded. *) + let callbacks = ref [] let register callback = diff --git a/src/util/apron/apronPrecCompareUtil.apron.ml b/src/util/apron/apronPrecCompareUtil.apron.ml index 046b9126ff..b276e0953b 100644 --- a/src/util/apron/apronPrecCompareUtil.apron.ml +++ b/src/util/apron/apronPrecCompareUtil.apron.ml @@ -1,3 +1,5 @@ +(** {!ApronDomain} precision comparison. *) + open PrecCompareUtil open ApronDomain diff --git a/src/util/apron/relationPrecCompareUtil.apron.ml b/src/util/apron/relationPrecCompareUtil.apron.ml index 7e4c60f4d3..15b59c2e22 100644 --- a/src/util/apron/relationPrecCompareUtil.apron.ml +++ b/src/util/apron/relationPrecCompareUtil.apron.ml @@ -1,3 +1,5 @@ +(** {!RelationPriv} precison comparison. *) + open PrecCompareUtil module MyNode = diff --git a/src/util/cilCfg.ml b/src/util/cilCfg.ml index 84b4797c53..2c8ec646c3 100644 --- a/src/util/cilCfg.ml +++ b/src/util/cilCfg.ml @@ -1,3 +1,5 @@ +(** Creation of CIL CFGs. *) + open GobConfig open GoblintCil @@ -30,9 +32,9 @@ class countLoopsVisitor(count) = object | Loop _ -> count := !count + 1; DoChildren | _ -> DoChildren -end +end -let loopCount file = +let loopCount file = let count = ref 0 in let visitor = new countLoopsVisitor(count) in ignore (visitCilFileSameGlobals visitor file); diff --git a/src/util/cilMaps.ml b/src/util/cilMaps.ml index 9b3b91f5c6..8f961a09e0 100644 --- a/src/util/cilMaps.ml +++ b/src/util/cilMaps.ml @@ -1,3 +1,5 @@ +(** Special maps used for incremental comparison. *) + open GoblintCil module VarinfoOrdered = struct diff --git a/src/util/cilType.ml b/src/util/cilType.ml index 547188c72c..87b78e60e9 100644 --- a/src/util/cilType.ml +++ b/src/util/cilType.ml @@ -1,3 +1,5 @@ +(** Printables for CIL types. *) + open GoblintCil open Pretty diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml index 3c61e5db88..18ff9bf234 100644 --- a/src/util/cilfacade.ml +++ b/src/util/cilfacade.ml @@ -1,4 +1,4 @@ -(** Helpful functions for dealing with [Cil]. *) +(** {!GoblintCil} utilities. *) open GobConfig open GoblintCil diff --git a/src/util/compilationDatabase.ml b/src/util/compilationDatabase.ml index 2c84e4c168..2443b8d3ab 100644 --- a/src/util/compilationDatabase.ml +++ b/src/util/compilationDatabase.ml @@ -1,3 +1,5 @@ +(** Input program from a real-world project using a compilation database. *) + open Batteries let basename = "compile_commands.json" diff --git a/src/util/contextUtil.ml b/src/util/contextUtil.ml index e079835da6..fc70e50dda 100644 --- a/src/util/contextUtil.ml +++ b/src/util/contextUtil.ml @@ -1,3 +1,5 @@ +(** Goblint-specific C attribute handling. *) + open GoblintCil (** Definition of Goblint specific user defined C attributes and their alternatives via options **) diff --git a/src/util/gobConfig.ml b/src/util/gobConfig.ml index 3cab128b29..c517ba150d 100644 --- a/src/util/gobConfig.ml +++ b/src/util/gobConfig.ml @@ -1,3 +1,5 @@ +(** Configuration access. *) + (** New, untyped, path-based configuration subsystem. diff --git a/src/util/goblintDir.ml b/src/util/goblintDir.ml index f5d616e058..41f1ef76a3 100644 --- a/src/util/goblintDir.ml +++ b/src/util/goblintDir.ml @@ -1,3 +1,5 @@ +(** Intermediate data directory. *) + open GobConfig let root () = Fpath.v (get_string "goblint-dir") diff --git a/src/util/intOps.ml b/src/util/intOps.ml index 153bb0a251..7c8e5d31e1 100644 --- a/src/util/intOps.ml +++ b/src/util/intOps.ml @@ -1,6 +1,4 @@ -(* -------------------------------------------------------------- - * IntOps Basics - * -------------------------------------------------------------- *) +(** Unified interface for integer types. *) open Batteries diff --git a/src/util/jsonSchema.ml b/src/util/jsonSchema.ml index 9accd2a270..701c948f3a 100644 --- a/src/util/jsonSchema.ml +++ b/src/util/jsonSchema.ml @@ -1,3 +1,5 @@ +(** JSON schema validation. *) + module JS = Json_schema.Make (Json_repr.Yojson) module JE = Json_encoding.Make (Json_repr.Yojson) module JQ = Json_query.Make (Json_repr.Yojson) diff --git a/src/util/lazyEval.ml b/src/util/lazyEval.ml index e6c85cf9b2..e49a5f4693 100644 --- a/src/util/lazyEval.ml +++ b/src/util/lazyEval.ml @@ -1,3 +1,6 @@ +(** Lazy evaluation with a fixed function. + Allows marshaling. *) + (* Lazy eval extracted here to avoid dependency cycle: Node -> CilType -> Printable -> Goblintutil -> GobConfig -> Tracing -> Node *) diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index b62dec9440..62d0f662f3 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -1,3 +1,5 @@ +(** Syntactic loop unrolling. *) + open GobConfig open GoblintCil diff --git a/src/util/messageUtil.ml b/src/util/messageUtil.ml index e1edc2d5be..17651fb05f 100644 --- a/src/util/messageUtil.ml +++ b/src/util/messageUtil.ml @@ -1,3 +1,5 @@ +(** Terminal color utilities. *) + open GobConfig let ansi_color_table = diff --git a/src/util/messages.ml b/src/util/messages.ml index 5c30344940..8aa1f2678f 100644 --- a/src/util/messages.ml +++ b/src/util/messages.ml @@ -1,3 +1,5 @@ +(** Messages (e.g. warnings) from the analysis. *) + module Pretty = GoblintCil.Pretty open GobConfig diff --git a/src/util/options.ml b/src/util/options.ml index 7fb6cabae9..d352c86465 100644 --- a/src/util/options.ml +++ b/src/util/options.ml @@ -1,3 +1,5 @@ +(** [src/util/options.schema.json] low-level access. *) + open Json_schema let schema = diff --git a/src/util/precCompare.ml b/src/util/precCompare.ml index 15543d80ab..45b3e32ed8 100644 --- a/src/util/precCompare.ml +++ b/src/util/precCompare.ml @@ -1,3 +1,5 @@ +(** Precison comparison. *) + open Batteries module Pretty = GoblintCil.Pretty open Pretty diff --git a/src/util/precCompareUtil.ml b/src/util/precCompareUtil.ml index d8ea4842e9..e00447fd60 100644 --- a/src/util/precCompareUtil.ml +++ b/src/util/precCompareUtil.ml @@ -1,3 +1,5 @@ +(** Signatures for precision comparison. *) + open Batteries (** A printable, where each element is related to one location. diff --git a/src/util/precisionUtil.ml b/src/util/precisionUtil.ml index 06bf08aa3c..047043b4aa 100644 --- a/src/util/precisionUtil.ml +++ b/src/util/precisionUtil.ml @@ -1,3 +1,5 @@ +(** Integer and floating-point option and attribute handling. *) + (* We define precision by the number of IntDomains activated. * We currently have 5 types: DefExc, Interval, Enums, Congruence, IntervalSet *) type int_precision = (bool * bool * bool * bool * bool) diff --git a/src/util/preprocessor.ml b/src/util/preprocessor.ml index 0b54fb88e8..1da3aa25ce 100644 --- a/src/util/preprocessor.ml +++ b/src/util/preprocessor.ml @@ -1,3 +1,5 @@ +(** Detection of suitable C preprocessor. *) + open Batteries let bad_cpp_version_regexp = Str.regexp_case_fold "clang\\|apple\\|darwin" diff --git a/src/util/privPrecCompareUtil.ml b/src/util/privPrecCompareUtil.ml index 367f01e8a7..8f0a24db3b 100644 --- a/src/util/privPrecCompareUtil.ml +++ b/src/util/privPrecCompareUtil.ml @@ -1,3 +1,5 @@ +(** {!BasePriv} precison comparison. *) + open GoblintCil open PrecCompareUtil diff --git a/src/util/processPool.ml b/src/util/processPool.ml index e93aa10548..89228fd6ac 100644 --- a/src/util/processPool.ml +++ b/src/util/processPool.ml @@ -1,3 +1,5 @@ +(** Process pool for running processes in parallel. *) + type task = { command: string; cwd: Fpath.t option; diff --git a/src/util/resettableLazy.mli b/src/util/resettableLazy.mli index f4103a86dd..5b0db478bb 100644 --- a/src/util/resettableLazy.mli +++ b/src/util/resettableLazy.mli @@ -1,3 +1,5 @@ +(** Lazy type which can be reset to a closure. *) + type 'a t val from_fun: (unit -> 'a) -> 'a t diff --git a/src/util/richVarinfo.mli b/src/util/richVarinfo.mli index fffccf8c5d..4e682734ee 100644 --- a/src/util/richVarinfo.mli +++ b/src/util/richVarinfo.mli @@ -1,3 +1,5 @@ +(** Custom {!GoblintCil.varinfo} management. *) + open GoblintCil val single: name:string -> (unit -> varinfo) diff --git a/src/util/sarif.ml b/src/util/sarif.ml index 216060c9e9..9fa428ff46 100644 --- a/src/util/sarif.ml +++ b/src/util/sarif.ml @@ -1,3 +1,5 @@ +(** SARIF output of {!Messages}. *) + (** The Sarif format is a standardised output format for static analysis tools. https://docs.oasis-open.org/sarif/sarif/v2.1.0/sarif-v2.1.0.html *) open Batteries diff --git a/src/util/sarifRules.ml b/src/util/sarifRules.ml index 17f4f5f263..feeeae10bc 100644 --- a/src/util/sarifRules.ml +++ b/src/util/sarifRules.ml @@ -1,3 +1,4 @@ +(** SARIF rule definitions for Goblint. *) type categoryInformation = { name:string; diff --git a/src/util/sarifType.ml b/src/util/sarifType.ml index 47b7261e7d..793ba24d01 100644 --- a/src/util/sarifType.ml +++ b/src/util/sarifType.ml @@ -1,3 +1,4 @@ +(** SARIF format types. *) module Invocation = struct diff --git a/src/util/server.ml b/src/util/server.ml index ace218ad06..bb6263d36e 100644 --- a/src/util/server.ml +++ b/src/util/server.ml @@ -1,3 +1,5 @@ +(** Interactive server mode using JSON-RPC. *) + open Batteries open Jsonrpc open GoblintCil diff --git a/src/util/timeout.ml b/src/util/timeout.ml index c60bbb32bb..ce1352ef67 100644 --- a/src/util/timeout.ml +++ b/src/util/timeout.ml @@ -1,3 +1,5 @@ +(** Timeout utilities. *) + module Unix = struct let timeout f arg tsecs timeout_fn = let oldsig = Sys.signal Sys.sigprof (Sys.Signal_handle (fun _ -> timeout_fn ())) in diff --git a/src/util/timing.ml b/src/util/timing.ml index d276a6f2f0..d5db4664aa 100644 --- a/src/util/timing.ml +++ b/src/util/timing.ml @@ -1,3 +1,5 @@ +(** Time measurement of computations. *) + module Default = Goblint_timing.Make (struct let name = "Default" end) module Program = Goblint_timing.Make (struct let name = "Program" end) diff --git a/src/util/tracing.ml b/src/util/tracing.ml index e3bcdc6126..f9dff2c2cf 100644 --- a/src/util/tracing.ml +++ b/src/util/tracing.ml @@ -1,3 +1,5 @@ +(** Nested tracing system for debugging. *) + (* TRACING STUFF. A rewrite of Cil's tracing framework which is too slow for the * large domains we output. The original code generated the document object * even when the subsystem is not activated. *) diff --git a/src/util/wideningThresholds.mli b/src/util/wideningThresholds.mli index df58fed65b..69e48695dd 100644 --- a/src/util/wideningThresholds.mli +++ b/src/util/wideningThresholds.mli @@ -1,3 +1,5 @@ +(** Widening threshold utilities. *) + val thresholds : unit -> Z.t list val thresholds_incl_mul2 : unit -> Z.t list val exps: GoblintCil.exp list ResettableLazy.t diff --git a/src/util/wideningTokens.ml b/src/util/wideningTokens.ml index a563d3cc79..fa0f1a33d4 100644 --- a/src/util/wideningTokens.ml +++ b/src/util/wideningTokens.ml @@ -1,4 +1,5 @@ (** Widening tokens are a generic and dynamic mechanism for delaying widening. + All abstract elements carry a set of tokens, which analyses can add into. Lifted abstract elements are only widened if the token set does not increase, i.e. adding a widening token delays a widening. diff --git a/src/util/xmlUtil.ml b/src/util/xmlUtil.ml index a0cc4bc982..e33be1b215 100644 --- a/src/util/xmlUtil.ml +++ b/src/util/xmlUtil.ml @@ -1,3 +1,5 @@ +(** XML utilities. *) + (* XML escape extracted here to avoid dependency cycle: CilType -> Goblintutil -> GobConfig -> Tracing -> Node -> CilType *) diff --git a/src/witness/argTools.ml b/src/witness/argTools.ml index d323b938b1..2d65911a5f 100644 --- a/src/witness/argTools.ml +++ b/src/witness/argTools.ml @@ -1,3 +1,5 @@ +(** Construction of {{!MyARG} ARGs} from constraint system solutions. *) + open MyCFG module M = Messages diff --git a/src/witness/graphml.ml b/src/witness/graphml.ml index 1282a6e3c3..022cbee8ef 100644 --- a/src/witness/graphml.ml +++ b/src/witness/graphml.ml @@ -1,3 +1,5 @@ +(** Streaming GraphML output. *) + module type GraphMlWriter = sig type t diff --git a/src/witness/myARG.ml b/src/witness/myARG.ml index 8a848898a1..62c705f5b1 100644 --- a/src/witness/myARG.ml +++ b/src/witness/myARG.ml @@ -1,3 +1,5 @@ +(** Abstract reachability graph. *) + open MyCFG open GoblintCil diff --git a/src/witness/observerAnalysis.ml b/src/witness/observerAnalysis.ml index 62bfd1fcc6..ec2ad670f8 100644 --- a/src/witness/observerAnalysis.ml +++ b/src/witness/observerAnalysis.ml @@ -1,3 +1,5 @@ +(** Path-sensitive analysis using an {!ObserverAutomaton}. *) + open GoblintCil open Analyses open MyCFG diff --git a/src/witness/observerAutomaton.ml b/src/witness/observerAutomaton.ml index 9b16cd511a..a5205b2b98 100644 --- a/src/witness/observerAutomaton.ml +++ b/src/witness/observerAutomaton.ml @@ -1,3 +1,5 @@ +(** Finite automaton for matching an infeasible ARG path. *) + module type S = sig type q diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml index d5fdac4859..a5a572d1c2 100644 --- a/src/witness/svcomp.ml +++ b/src/witness/svcomp.ml @@ -1,3 +1,5 @@ +(** SV-COMP tasks and results. *) + open GoblintCil open Batteries diff --git a/src/witness/svcompSpec.ml b/src/witness/svcompSpec.ml index 4f846f282d..464c170251 100644 --- a/src/witness/svcompSpec.ml +++ b/src/witness/svcompSpec.ml @@ -1,3 +1,5 @@ +(** SV-COMP specification strings and files. *) + open Batteries type t = diff --git a/src/witness/timeUtil.ml b/src/witness/timeUtil.ml index 291e2e8fc2..e1736f4fca 100644 --- a/src/witness/timeUtil.ml +++ b/src/witness/timeUtil.ml @@ -1,3 +1,5 @@ +(** Date and time utilities. *) + open Unix let iso8601_of_tm {tm_year; tm_mon; tm_mday; tm_hour; tm_min; tm_sec; _} = diff --git a/src/witness/violation.ml b/src/witness/violation.ml index 9b85f854ff..d48005a988 100644 --- a/src/witness/violation.ml +++ b/src/witness/violation.ml @@ -1,3 +1,5 @@ +(** Violation checking in an ARG. *) + module type ViolationArg = sig include MyARG.S with module Edge = MyARG.InlineEdge diff --git a/src/witness/witness.ml b/src/witness/witness.ml index 08eafbb6a8..aff9a01383 100644 --- a/src/witness/witness.ml +++ b/src/witness/witness.ml @@ -1,3 +1,5 @@ +(** Output of ARG as GraphML. *) + open MyCFG open Graphml open Svcomp diff --git a/src/witness/witnessConstraints.ml b/src/witness/witnessConstraints.ml index 7849718be9..66136f07b6 100644 --- a/src/witness/witnessConstraints.ml +++ b/src/witness/witnessConstraints.ml @@ -1,4 +1,4 @@ -(** An analysis specification for witnesses. *) +(** Analysis specification transformation for ARG construction. *) open Batteries open Analyses diff --git a/src/witness/witnessUtil.ml b/src/witness/witnessUtil.ml index 91a021c32b..12bc598be5 100644 --- a/src/witness/witnessUtil.ml +++ b/src/witness/witnessUtil.ml @@ -1,3 +1,5 @@ +(** Utilities for witness generation and witness invariants. *) + open MyCFG open GoblintCil diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 8c2bae6352..31fd4dccc2 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -1,3 +1,5 @@ +(** YAML witness generation and validation. *) + open Analyses open GoblintCil diff --git a/src/witness/yamlWitnessType.ml b/src/witness/yamlWitnessType.ml index ae30828a55..3390c1e3ab 100644 --- a/src/witness/yamlWitnessType.ml +++ b/src/witness/yamlWitnessType.ml @@ -1,3 +1,5 @@ +(** YAML witness format types. *) + module Producer = struct type t = { diff --git a/src/witness/z3/violationZ3.no-z3.ml b/src/witness/z3/violationZ3.no-z3.ml index 0c61eb3b29..0771f6862d 100644 --- a/src/witness/z3/violationZ3.no-z3.ml +++ b/src/witness/z3/violationZ3.no-z3.ml @@ -1 +1,3 @@ +(** ARG path feasibility checking using weakest precondition and {!Z3} ({b not installed!}). *) + module WP = Violation.UnknownFeasibility (* default to always unknown if no Z3 installed *) diff --git a/src/witness/z3/violationZ3.z3.ml b/src/witness/z3/violationZ3.z3.ml index bebd367157..a93684bdb3 100644 --- a/src/witness/z3/violationZ3.z3.ml +++ b/src/witness/z3/violationZ3.z3.ml @@ -1,3 +1,5 @@ +(** ARG path feasibility checking using weakest precondition and {!Z3}. *) + open Violation module WP (Node: MyARG.Node): Feasibility with module Node = Node =