diff --git a/.clang-format b/.clang-format new file mode 100644 index 00000000..10b62638 --- /dev/null +++ b/.clang-format @@ -0,0 +1,16 @@ +--- +BasedOnStyle: Google +--- +Language: Cpp +SpacesInAngles: true +AccessModifierOffset: -2 +DerivePointerAlignment: false +AllowShortIfStatementsOnASingleLine: false +AllowShortLoopsOnASingleLine: false +AllowShortFunctionsOnASingleLine: Inline +BinPackParameters: false +BinPackArguments: false +PenaltyBreakBeforeFirstCallParameter: 5000 +PenaltyReturnTypeOnItsOwnLine: 500 +SpacesBeforeTrailingComments: 1 +--- diff --git a/.gitignore b/.gitignore new file mode 100644 index 00000000..6b65b5a5 --- /dev/null +++ b/.gitignore @@ -0,0 +1,38 @@ +build + +# Editors +*.swp +*~ +.ycm_extra_conf.py + +# Python +*.pyc +__pycache__ + +# Object files +*.o +*.ko +*.obj +*.elf + +# Libraries +*.lib +*.a + +# Shared objects (inc. Windows DLLs) +*.dll +*.so +*.so.* +*.dylib + +# Executables +*.exe +*.out +*.app +*.i*86 +*.x86_64 +*.hex + +# IKOS +*.ar +*.db diff --git a/CMakeLists.txt b/CMakeLists.txt new file mode 100644 index 00000000..10c1f9d5 --- /dev/null +++ b/CMakeLists.txt @@ -0,0 +1,95 @@ +#******************************************************************************* +# +# Author: Maxime Arthaud +# +# Contact: ikos@lists.nasa.gov +# +# Notices: +# +# Copyright (c) 2011-2017 United States Government as represented by the +# Administrator of the National Aeronautics and Space Administration. +# All Rights Reserved. +# +# Disclaimers: +# +# No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF +# ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT LIMITED +# TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO SPECIFICATIONS, +# ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE, +# OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL BE +# ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF PROVIDED, WILL CONFORM TO +# THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN ANY MANNER, CONSTITUTE AN +# ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR RECIPIENT OF ANY RESULTS, +# RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR ANY OTHER APPLICATIONS +# RESULTING FROM USE OF THE SUBJECT SOFTWARE. FURTHER, GOVERNMENT AGENCY +# DISCLAIMS ALL WARRANTIES AND LIABILITIES REGARDING THIRD-PARTY SOFTWARE, +# IF PRESENT IN THE ORIGINAL SOFTWARE, AND DISTRIBUTES IT "AS IS." +# +# Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST +# THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL +# AS ANY PRIOR RECIPIENT. IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS +# IN ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH +# USE, INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, +# RECIPIENT'S USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD +# HARMLESS THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, +# AS WELL AS ANY PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW. +# RECIPIENT'S SOLE REMEDY FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, +# UNILATERAL TERMINATION OF THIS AGREEMENT. +# +#*****************************************************************************/ + +cmake_minimum_required(VERSION 2.8.12.2 FATAL_ERROR) + +project(ikos) +set(PACKAGE_VERSION "1.3") + +# +# Build settings +# + +if (CMAKE_SOURCE_DIR STREQUAL CMAKE_BINARY_DIR) + message (FATAL_ERROR + "In-source builds are not allowed. Please clean your source tree and try again.") +endif() + +if (NOT CMAKE_BUILD_TYPE) + set(CMAKE_BUILD_TYPE "Release" CACHE STRING "Choose the type of build." FORCE) +endif() + +if (CMAKE_INSTALL_PREFIX_INITIALIZED_TO_DEFAULT) + set(CMAKE_INSTALL_PREFIX "${CMAKE_SOURCE_DIR}/install" CACHE STRING "Install directory." FORCE) +endif() +message(STATUS "All libraries and binaries will be installed in ${CMAKE_INSTALL_PREFIX}") + +# Do not build anything when running make install +set(CMAKE_SKIP_INSTALL_ALL_DEPENDENCY TRUE) + +# Add path for custom modules +set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_CURRENT_SOURCE_DIR}/cmake") + +# Enable tests +include(CTest) +enable_testing() + +# Add abstract-representation +add_subdirectory(abs-repr) + +set(ARBOS_FOUND "ON") +set(ARBOS_INCLUDE_DIR "${CMAKE_SOURCE_DIR}/abs-repr/include") +set(ARBOS_LIB arbos-api) +set(ARBOS_BIN "") + +# LLVM frontend +add_subdirectory(frontends/llvm) + +# IKOS core +add_subdirectory(core) + +set(IKOS_FOUND "ON") +set(IKOS_INCLUDE_DIR "${CMAKE_SOURCE_DIR}/core/include") + +# Analyzer +add_subdirectory(analyzer) + +# Doxygen +add_custom_target(docs DEPENDS doxygen-arbos doxygen-ikos doxygen-analyzer) diff --git a/LICENSE.pdf b/LICENSE.pdf new file mode 100644 index 00000000..84a8f011 Binary files /dev/null and b/LICENSE.pdf differ diff --git a/README.md b/README.md new file mode 100644 index 00000000..7b310d01 --- /dev/null +++ b/README.md @@ -0,0 +1,281 @@ +IKOS 1.3 +======== + +IKOS (Inference Kernel for Open Static Analyzers) is a static analyzer for C/C++ based on the theory of Abstract Interpretation. + +Introduction +------------ + +IKOS started as a C++ library designed to facilitate the development of sound static analyzers based on [Abstract Interpretation](https://www.di.ens.fr/~cousot/AI/IntroAbsInt.html). Specialization of a static analyzer for an application or family of applications is critical for achieving both precision and scalability. Developing such an analyzer is arduous and requires significant expertise in Abstract Interpretation. + +IKOS provides a generic and efficient implementation of state-of-the-art Abstract Interpretation data structures and algorithms, such as control-flow graphs, fixpoint iterators, numerical abstract domains, etc. IKOS is independent of a particular programming language. + +IKOS now also provides a C/C++ analyzer based on [LLVM](https://llvm.org/). It implements scalable analyses for detecting buffer-overflows, divisions by zero, null pointer dereferences, uninitialized variables and unaligned pointer dereferences in C and C++ programs. + +License +------- + +IKOS has been released under the NASA Open Source Agreement version 1.3, see [LICENSE.pdf](LICENSE.pdf) + +Contact +------- + +ikos@lists.nasa.gov + +Release notes +------------- + +See [RELEASE_NOTES.md](RELEASE_NOTES.md) + +Troubleshooting +--------------- + +See [TROUBLESHOOTING.md](TROUBLESHOOTING.md) + +Build and Install +----------------- + +IKOS analyzes programs transformed into the Abstract Representation (AR), an intermediate representation that represents the control-flow graph of the program. The IKOS distribution provides a compiler frontend that transforms C/C++ programs into the AR using the LLVM compiler framework. + +The next section illustrates how to install the required dependencies. + +### Dependencies + +To build and run the analyzer, you will need the following dependencies: + +* CMake >= 2.8.12.2 +* GMP >= 4.3.1 +* Boost >= 1.55 +* Python 2 >= 2.7.3 or Python 3 >= 3.3 +* SQLite >= 3.6.20 +* LLVM and Clang 4.0.x +* A C++ compiler that supports C++14 (gcc >= 4.9.2 or clang >= 3.4) + +Note: You will need CMake >= 3.4.3 if you build LLVM from source + +Most of them can be installed using your package manager. + +Installation instructions for Archlinux, CentOS, Debian, Fedora, Mac OS X, Red Hat and Ubuntu are available in the [docs](docs) directory. These instructions assume you have sudo or root access. If you don't, please follow the instructions in [docs/INSTALL_ROOTLESS.md](docs/INSTALL_ROOTLESS.md). + +Once you have all the required dependencies, move to the next section. + +### Build and Install IKOS + +Now that you have all the dependencies on your system, you can build and install IKOS. + +As you open the IKOS distribution, you shall see the following content: + +``` +. +├── CMakeLists.txt +├── LICENSE.pdf +├── README.md +├── RELEASE_NOTES.md +├── TROUBLESHOOTING.md +├── abs-repr +├── analyzer +├── cmake +├── core +├── docs +├── frontends +└── scripts +``` + +We use CMake to build IKOS. You will need to specify an installation directory that will contain all the binaries, libraries and headers after installation. If you do not specify this directory, CMake will install everything under `install` in the root directory of the distribution. In the following steps, we will install IKOS under `/path/to/ikos-install-directory`. After installation, it will contain the following structure: + +``` +. +├── include +├── bin +└── lib +``` + +Here are the steps to build and install IKOS: + +``` +$ mkdir build +$ cd build +$ cmake -DCMAKE_INSTALL_PREFIX=/path/to/ikos-install-directory .. +$ make +$ make install +``` + +### Running the tests + +To run the tests, we will need the full installation of IKOS. In addition, we will also need to build and install the verifier passes: + +``` +$ make verifier-passes +$ make install +``` + +Now, you can run the tests: + +``` +$ PATH=/path/to/ikos-install-directory/bin:$PATH +$ make test +``` + +How to run IKOS +--------------- + +Suppose we want to analyze the following C program in a file, called *loop.c*: + +```c + 1: #include + 2: int a[10]; + 3: int main(int argc, char *argv[]) { + 4: size_t i = 0; + 5: for (;i < 10; i++) { + 6: a[i] = i; + 7: } + 8: a[i] = i; + 9: printf("%i", a[i]); +10: } +``` + +Using the following commands, you can run IKOS to detect buffer overflow defects directly against the C program: + +``` +$ PATH=/path/to/ikos-install-directory/bin:$PATH +$ ikos loop.c --export +``` + +Then you shall see the following output. IKOS reports two occurrences of buffer overflow at line 8 and 9. + +``` +dlopen successful on /path/to/ikos-install-directory/lib/libpointer-shift-opt.dylib +Loaded ARBOS pass: ps-opt - Optimize pointer shift statements +dlopen successful on /path/to/ikos-install-directory/lib/libbranching-opt.dylib +Loaded ARBOS pass: branching-opt - Optimize the Control Flow Graph +dlopen successful on /path/to/ikos-install-directory/lib/libinline-init-gv.dylib +Loaded ARBOS pass: inline-init-gv - Inline initialization of global variables in main +dlopen successful on /path/to/ikos-install-directory/lib/libunify-exit-nodes.dylib +Loaded ARBOS pass: unify-exit-nodes - Unify exit nodes +dlopen successful on /path/to/ikos-install-directory/lib/libanalyzer.dylib +Loaded ARBOS pass: analyzer - Analyzer pass +5 pass(es) registered. +Executing pass - ps-opt Optimize pointer shift statements +Executing pass - branching-opt Optimize the Control Flow Graph +Executing pass - inline-init-gv Inline initialization of global variables in main +Executing pass - unify-exit-nodes Unify exit nodes +Executing pass - analyzer Analyzer pass +Running liveness variable analysis ... +Running function pointer analysis ... +** Generating pointer constraints ... +** Solving pointer constraints ... +Running pointer analysis ... +** Computing intra-procedural numerical invariants ... +** Generating pointer constraints ... +** Solving pointer constraints ... +Running value analysis ... +*** Analyzing entry point: main +*** Analyzing function: __ikos_init_globals +*** Writing results for entry point: main + +# Time stats: +arbos : 0.117 sec +clang : 0.023 sec +ikos-pp : 0.006 sec +llvm-to-ar: 0.017 sec + +# Summary: +Total number of checks : 30 +Total number of unreachable checks : 0 +Total number of safe checks : 28 +Total number of definite unsafe checks: 2 +Total number of warnings : 0 + +The program is definitely UNSAFE + +# Results +loop.c: In function 'main': +loop.c:8:10: error: buffer overflow, trying to access index 10 + a[i] = i; + ^ +loop.c: In function 'main': +loop.c:9:18: error: buffer overflow, trying to access index 10 + printf("%i", a[i]); + ^ +``` + +The ikos command takes a source file (`.c`, `.cpp`) or a LLVM bitcode file (`.bc`) as input, analyzes it to find undefined behaviors (such as buffer overflows), creates a result database `output.db` in the current working directory, prints a summary and exits. + +To see the analysis report within your terminal, you shall use the `--export` option. This argument generates a report using the result database, and prints it in a specific format (by default, a gcc-style format). + +You can either provide the `--export` option directly in the ikos command, or as a second step using the ikos-render command, taking the result database: + +``` +$ ikos-render output.db --export +``` + +To analyze a large program, you shall run the `ikos` command first to create the result database `output.db` and then generate a report using the `ikos-render` command. This way, you can generate reports in different formats and adjust the verbosity to your needs, without running the analysis again. + +Further information: +* [Analyses options](analyzer/README.md#analyses-options) +* [Export options](analyzer/README.md#export-options) +* [Export formats](analyzer/README.md#export-formats) +* [Running IKOS on a whole C/C++ project](analyzer/README.md#running-ikos-on-a-whole-cc-project) + +Current and Past contributors +----------------------------- + +* Maxime Arthaud +* Guillaume Brat +* Clément Decoodt +* Jorge Navas +* Nija Shi +* Sarah Thompson +* Arnaud Venet +* Alexandre Wimmers + +Publications +------------ + +* Guillaume Brat, Jorge Navas, Nija Shi and Arnaud Venet. **IKOS: a Framework for Static Analysis based on Abstract Interpretation.** In _Proceedings of the International Conference on Software Engineering and Formal Methods (SEFM 2014)_, Grenoble, France ([PDF](http://ti.arc.nasa.gov/publications/16610/download/)). + +* Arnaud Venet. **The Gauge Domain: Scalable Analysis of Linear Inequality Invariants.** In _Proceedings of Computer Aided Verification (CAV 2012)_, Berkeley, California, USA 2012. Lecture Notes in Computer Science, pages 139-154, volume 7358, Springer 2012 ([PDF](http://ti.arc.nasa.gov/publications/4767/download/)). + +Overview of the source code +--------------------------- + +The following illustrates the content of the root directory: + +``` +. +├── CMakeLists.txt +├── LICENSE.pdf +├── README.md +├── RELEASE_NOTES.md +├── TROUBLESHOOTING.md +├── abs-repr +├── analyzer +├── cmake +├── core +├── docs +├── frontends +└── scripts +``` + + +* [CMakeLists.txt](CMakeLists.txt) is the root CMake file. + +* [LICENSE.pdf](LICENSE.pdf) contains the NOSA 1.3 license + +* [RELEASE_NOTES.md](RELEASE_NOTES.md) contains the release notes for the latest versions. + +* [TROUBLESHOOTING.md](TROUBLESHOOTING.md) contains solution for common issues with IKOS. + +* [cmake](cmake) contains CMake files to search for related software libraries. + +* [core](core) contains the implementation of the theory of Abstract Interpretation, which includes the abstract domains, the fixpoint iterator, and various algorithms that support the implementation. More information can be found at [core/README.md](core/README.md). + +* [abs-repr](abs-repr) contains the implementation of the ARBOS, a plugin framework that parses the AR and executes AR passes that perform various analysis. More information can be found at [abs-repr/README.md](abs-repr/README.md). + +* [analyzer](analyzer) contains the implementation of various analyses for specific defect detections. These analyses are implemented as AR passes and use the fixpoint iterator and abstract domains to perform analysis. More information can be found at [analyzer/README.md](analyzer/README.md). + +* [frontends](frontends) contains implementation of various frontend compilers to translate programs into AR. Currently we only support the LLVM frontend. More information can be found at [frontends/llvm/README.md](frontends/llvm/README.md). + +* [scripts](scripts) contains the [bootstrap](scripts/bootstrap) script for a rootless installation. + +* [docs](docs) contains installation instructions for specific operating systems. diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md new file mode 100644 index 00000000..b21c1cd9 --- /dev/null +++ b/RELEASE_NOTES.md @@ -0,0 +1,184 @@ +IKOS version 1.3 release notes +============================== + +Release date +------------ + +October 2017 + +List of changes +--------------- + +### IKOS Core changes + +* Added an implementation of the Gauge domain. +* Combined the memory domain and the pointer domain, improving the precision for arrays of pointers and virtual tables. +* Improved the documentation + +### Analyzer changes + +* Added a report generator. The analyzer can now export the results in a gcc-style format, json or csv. +* Added an analysis of unaligned pointers. +* Improved the analysis performance by keeping previous fixpoints of called functions in memory. +* Added the intrinsic function `__ikos_debug()`, that dumps the current invariant. +* Added support for analyzing variable argument functions (`va_start`, `va_arg`, `va_end` and `va_copy`). +* Added support for analyzing structures in register (`insertelement` and `extractelement` in LLVM). +* Fixed an unsoundness in the exception analysis. +* Added a `settings` and `times` table in the result database, allowing a user to query the analysis options and timing results. +* Added special checks that warn about dangerous code patterns (such as casts from integers to pointers). +* Fixed and improved the analysis of bitwise and conversion operators. +* Moved all global variable initializations into the internal function `__ikos_init_globals`, also fixing the initialization of global objects in C++. + +### ARBOS changes + +* Added support for C variable-length arrays (VLA). + +### LLVM frontend changes + +* Upgraded to LLVM 4.0.x + + +IKOS version 1.2 release notes +============================== + +Release date +------------ + +October 2016 + +List of changes +--------------- + +### IKOS Core changes + +* Added an abstract domain to handle C++ exceptions. + +### Analyzer changes + +* Implemented a proper C++ exception propagation handling using abstract interpretation. IKOS correctly handles C++ code with exceptions. +* Improved the analysis of string-related functions (such as strlen, strcpy and strcat). +* Fixed the precision of the null dereference analysis. + +### ARBOS changes + +* Removed AR_Unwind as it is no longer generated by LLVM since LLVM 3.1 +* Added APIs to set and retrieve the "resume" basic block in an AR_Code. + + +IKOS version 1.1.2 release notes +================================ + +Release date +------------ + +September 2016 + +List of changes +--------------- + +### IKOS Core changes + +* Added interfaces for abstract domains, nullity domains, uninitialized variables domains, pointer domains and memory domains. +* Moved the pointer domain, the value domain and the summary domain under IKOS core. + +### Analyzer changes + +* Added a pass to unify exit nodes. + +### ARBOS changes + +* Added APIs to set and retrieve "unreachable" and "unwind" basic blocks in an AR_Code + + +IKOS version 1.1.1 release notes +================================ + +Release date +------------ + +August 2016 + +List of changes +--------------- + +### Analyzer changes + +* Added a pass `branching-opt` to optimize all Control Flow Graphs of the AR, before the analysis. The pass detects unreachable paths in the graphs and removes them. + +### IKOS Core changes + +* Improved the precision of the interval domain on most binary operators. +* Added a wrapper for APRON. + +### Other changes + +* Improved the bootstrap script. It is now able to build and install zlib, ncurses, libedit, GMP, SQLite and Python. +* Added installation instructions for Archlinux, CentOS, Debian, Fedora, Mac OS X, Red Hat and Ubuntu. +* Added support for gcc 4.9.2 and boost 1.55.0. + + +IKOS version 1.1.0 release notes +================================ + +Release date +------------ + +June 2016 + +List of changes +--------------- + +### Analyzer changes + +* Added the ability to demangle C++ function names. +* We now handle `calloc()` correctly. In IKOS 1.0.0, the function call was just ignored. +* Added the runtime options `--display-invariants` and `--display-checks`. +* Added a column called `column` to the result tables in the output database, containing the column number in the source code. +* Added a column called `stmt_uid` to the result tables in the output database, containing the UID of the checked statement. +* Performance improvement (the analysis is 70% faster in average). +* Bug fixes. + +### LLVM Frontend changes + +The LLVM frontend now supports both LLVM 3.7 and 3.8. + +### ARBOS changes + +ARBOS now gives the column number in addition to the line number in `AR_Source_Location`. + + +IKOS version 1.0.0 release notes +================================ + +Release date +------------ + +May 2016 + +List of changes +--------------- + +### LLVM Frontend changes + +In this release we upgraded our LLVM frontend from version 2.9 to 3.7. + +To have a C/C++ program fully represented in AR, there are several code transformation we had to handle with the frontend's intermediate representation. When using the LLVM framework as the frontend, we transform the following LLVM instructions so they can be expressed in AR: + +* `phi` instruction +* `getelementptr` instruction +* `insertvalue` and `extractvalue` instructions +* `i/fcmp` and `select` instructions +* removed `br` +* `constantexpr` and its subclasses +* translation of intrinsic calls to AR-supported intrinsic calls. We currently support `memset`, `memcpy`, `memmove`, `vastart`, `vaend`, `va_arg`, and `vacopy`. + +In the previous release v0.0.1 we handled all transformation in **ARBOS**. The previous tool chain architecture defined another intermediate representation, called **AIR**, that served as a direct translation from the LLVM bitcode to an S-expression format that was fed into **ARBOS**. **ARBOS** then parsed and transformed **AIR** to **AR** in memory. + +This release removes **AIR** entirely. All transformation are done in **LLVMAR**, while **ABROS** only parses the AR and makes it available in memory for ARBOS analysis plugins to traverse and perform analysis on it. + +### ARBOS API changes + +* Each `AR_Global_Variable` may contain an initializer represented as `AR_Code`. In the previous release we dedicated an initializer function for each global variable. These initializer functions were individually invoked in `main()`. In this release, analyzers need to dive into the initializer of an `AR_Global_Variable` to analyze the initializer code. +* Differentiates between store vs. real sizes of an `AR_Type`. +* Supports `varags` intrinsic calls in the AR. This was not supported in the previous release. +* Function pointers are now available in the AR model; they were misinterpreted and were not available in the previous release. diff --git a/TROUBLESHOOTING.md b/TROUBLESHOOTING.md new file mode 100644 index 00000000..4d813f3c --- /dev/null +++ b/TROUBLESHOOTING.md @@ -0,0 +1,78 @@ +Troubleshooting +=============== + +This document covers some common issues with IKOS, and how to solve them. + +Contact +------- + +ikos@lists.nasa.gov + +Installation issues +------------------- + +### "Could NOT find LLVM" while running cmake + +CMake could not find LLVM. + +First, install LLVM 4.0.x. This can usually be done with your package manager. + +If this message still shows up, it means cmake cannot find the `llvm-config` command. + +You can either add the LLVM binary directory in your PATH, or give cmake the full path to llvm-config, using `-DLLVM_CONFIG_EXECUTABLE=/path/to/llvm-config` + +For instance, if you installed LLVM using Homebrew on Mac OS X, you can add LLVM in your path using: + +``` +$ PATH="$(brew --prefix)/opt/llvm@4/bin:$PATH" +``` + +### "Could not find ikos python module" while running ikos + +The ikos command could not import the ikos python module. + +The module should be under `/path/to/ikos-install/lib/python*/site-packages` + +If the ikos python module is in another directory, make sure it is in your PYTHONPATH: + +``` +export PYTHONPATH=/path/to/ikos-python-module +``` + +### "Could not find clang" while running ikos + +IKOS is expecting clang to be in the LLVM binary directory, i.e. in the directory given by `ikos-config --llvm-bindir`. + +If clang is installed in another directory, you can hard-code its path in settings.py under `/path/to/ikos-install/lib/python*/site-packages/ikos/settings/__init__.py` + +### "Could not find ikos-view" while running ikos + +ikos-view is currently not open source, sorry. + +Analysis issues +--------------- + +### Exited with signal 9 + +IKOS probably ran out of memory. + +We are currently working on this issue. + +As a short-term solution, you could run IKOS on a machine with more memory. + +Known issues +------------ + +### Source Code Fortification + +Source code fortification aims at making your source code more robust. It replaces regular `memset()`, `memcpy()` and `memmove()` calls to `__memset_chk()`, `__memcpy_chk()` and `__memmove_chk()`. According to Linux Standard Base Core Specification 4.1, the interfaces `__memset_chk()`, `__memcpy_chk()` and `__memmove_chk()` shall function in the same way as the interface `memset()`, `memcpy()` and `memmove()`, respectively, except that `__memset_chk()`, `__memcpy_chk()` and `__memmove_chk()` shall check for buffer overflow before computing a result. If an overflow is anticipated, the function shall abort and the program calling it shall exit. + +The Buffer Overflow Analysis (BOA) in IKOS handles `__memset_chk()`, `__memcpy_chk()` and `__memmove_chk()` as unknown library functions, and won't report any warning. Consider using `-D_FORTIFY_SOURCE=0` when you compile your source code to LLVM bitcode manually. + +### Handling Global Variables + +Prior to performing any analysis, the initialization code of the global variables in the AR program model are inlined in function `main()` if available. This transformation of the AR program model is implemented as an AR pass located at `analyzer/src/ar-passes/inline-init-gv.cpp`. + +### Octagon Abstract Domain + +The octagon abstract domain has some implementation issues. Do not use it. diff --git a/abs-repr/CMakeLists.txt b/abs-repr/CMakeLists.txt new file mode 100644 index 00000000..23905af7 --- /dev/null +++ b/abs-repr/CMakeLists.txt @@ -0,0 +1,211 @@ +#******************************************************************************* +# +# Author: Maxime Arthaud +# +# Contact: ikos@lists.nasa.gov +# +# Notices: +# +# Copyright (c) 2011-2017 United States Government as represented by the +# Administrator of the National Aeronautics and Space Administration. +# All Rights Reserved. +# +# Disclaimers: +# +# No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF +# ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT LIMITED +# TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO SPECIFICATIONS, +# ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE, +# OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL BE +# ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF PROVIDED, WILL CONFORM TO +# THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN ANY MANNER, CONSTITUTE AN +# ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR RECIPIENT OF ANY RESULTS, +# RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR ANY OTHER APPLICATIONS +# RESULTING FROM USE OF THE SUBJECT SOFTWARE. FURTHER, GOVERNMENT AGENCY +# DISCLAIMS ALL WARRANTIES AND LIABILITIES REGARDING THIRD-PARTY SOFTWARE, +# IF PRESENT IN THE ORIGINAL SOFTWARE, AND DISTRIBUTES IT "AS IS." +# +# Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST +# THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL +# AS ANY PRIOR RECIPIENT. IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS +# IN ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH +# USE, INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, +# RECIPIENT'S USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD +# HARMLESS THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, +# AS WELL AS ANY PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW. +# RECIPIENT'S SOLE REMEDY FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, +# UNILATERAL TERMINATION OF THIS AGREEMENT. +# +#*****************************************************************************/ + +cmake_minimum_required(VERSION 2.8.12.2 FATAL_ERROR) + +project(abstract-representation) + +# +# Build settings +# + +if (CMAKE_SOURCE_DIR STREQUAL CMAKE_BINARY_DIR) + message (FATAL_ERROR + "In-source builds are not allowed. Please clean your source tree and try again.") +endif() + +if (NOT CMAKE_BUILD_TYPE) + set(CMAKE_BUILD_TYPE "Release" CACHE STRING "Choose the type of build." FORCE) +endif() + +if (CMAKE_INSTALL_PREFIX_INITIALIZED_TO_DEFAULT) + set(CMAKE_INSTALL_PREFIX "${CMAKE_SOURCE_DIR}/install" CACHE STRING "Install directory." FORCE) +endif() +message(STATUS "All libraries and binaries will be installed in ${CMAKE_INSTALL_PREFIX}") + +# +# CMake policy +# + +# Use @rpath on Mac OS X (requires MAC OS X >= 10.5) +if (POLICY CMP0042) + cmake_policy(SET CMP0042 NEW) +else () + set(CMAKE_MACOSX_RPATH ON) +endif() + +# For add_cxx_flag +if (POLICY CMP0054) + cmake_policy(SET CMP0054 OLD) +endif() + +# Do not build anything when running make install +set(CMAKE_SKIP_INSTALL_ALL_DEPENDENCY TRUE) + +# +# CMake utils +# + +include(CheckCXXCompilerFlag) + +macro(add_cxx_flag flag name) + CHECK_CXX_COMPILER_FLAG(${flag} "CXX-SUPPORTS-${name}") + if("CXX-SUPPORTS-${name}") + add_definitions(${flag}) + else() + message(FATAL_ERROR "${flag} flag is not supported by ${CMAKE_CXX_COMPILER}") + endif() +endmacro() + +# +# Dependency checks +# + +# Add path for custom modules +set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_CURRENT_SOURCE_DIR}/../cmake") + +set(CUSTOM_BOOST_ROOT "" CACHE PATH "Path to custom boost installation.") +if (CUSTOM_BOOST_ROOT) + set(BOOST_ROOT "${CUSTOM_BOOST_ROOT}") + set(Boost_NO_SYSTEM_PATHS "ON") +endif() + +find_package(Boost 1.55.0 REQUIRED + COMPONENTS program_options) +include_directories(${Boost_INCLUDE_DIRS}) + +find_package(GMP REQUIRED) +include_directories(${GMP_INCLUDE_DIR}) +include_directories(${GMPXX_INCLUDE_DIR}) + +find_package(RT) +if (NOT RT_FOUND) + set(RT_LIB "") +endif() + +# +# Compiler flags +# + +add_cxx_flag("-std=c++1y" "CXX14") +add_cxx_flag("-Wall" "WALL") +# warning flags from -Wextra +add_cxx_flag("-Wempty-body" "WEMPTY_BODY") +add_cxx_flag("-Wmissing-field-initializers" "WMISSING_FIELD_INITIALIZERS") +add_cxx_flag("-Wsign-compare" "WSIGN_COMPARE") +add_cxx_flag("-Wtype-limits" "WTYPE_LIMITS") +add_cxx_flag("-Wuninitialized" "WUNINITIALIZED") + +# +# Targets +# + +include_directories(include) + +# arbos +add_library(arbos-api SHARED + src/arbos/api/ar.cpp + src/arbos/api/ar_factory.cpp + src/arbos/api/ar_visitor.cpp +) +target_link_libraries(arbos-api ${Boost_LIBRARIES} ${GMP_LIB} ${GMPXX_LIB}) +install(TARGETS arbos-api LIBRARY DESTINATION lib OPTIONAL) + +add_executable(arbos src/arbos/arbos.cpp) +target_link_libraries(arbos arbos-api ${CMAKE_DL_LIBS} ${RT_LIB} pthread) +install(TARGETS arbos RUNTIME DESTINATION bin OPTIONAL) +set_target_properties(arbos PROPERTIES + INSTALL_RPATH "${CMAKE_INSTALL_PREFIX}/lib") + +# install headers +install(DIRECTORY include/ + DESTINATION include + FILES_MATCHING + PATTERN "*.hpp" +) + +# passes +add_library(print SHARED src/passes/dumps/print.cpp) +target_link_libraries(print arbos-api) +install(TARGETS print DESTINATION lib OPTIONAL) + +# example passes +add_subdirectory(src/passes/examples EXCLUDE_FROM_ALL) + +# Hack so that "make install" also tries to install example passes +install(SCRIPT "${CMAKE_CURRENT_BINARY_DIR}/src/passes/examples/cmake_install.cmake") + +# +# Regression tests +# + +include(CTest) +enable_testing() + +add_subdirectory(tests/regression/tests) +add_subdirectory(tests/regression/verifier-passes EXCLUDE_FROM_ALL) + +# Hack so that "make install" also tries to install verifier passes +install(SCRIPT "${CMAKE_CURRENT_BINARY_DIR}/tests/regression/verifier-passes/cmake_install.cmake") + +# +# Doxygen +# + +find_package(Doxygen) +if (DOXYGEN_FOUND) + configure_file(docs/doxygen/Doxyfile.in docs/Doxyfile @ONLY) + configure_file(docs/doxygen/customdoxygen.css docs/customdoxygen.css @ONLY) + configure_file(docs/doxygen/DoxygenLayout.xml docs/DoxygenLayout.xml @ONLY) + add_custom_target(doxygen-arbos + ${DOXYGEN_EXECUTABLE} "${CMAKE_CURRENT_BINARY_DIR}/docs/Doxyfile" + WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}" + COMMENT "Generating ARBOS API documentation with Doxygen" VERBATIM + ) + install(DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/docs/html" DESTINATION docs/arbos OPTIONAL) +endif() + +# +# If it's the top level CMakeLists.txt, we add some aliases +# + +if (CMAKE_SOURCE_DIR STREQUAL CMAKE_CURRENT_SOURCE_DIR) + add_custom_target(docs DEPENDS doxygen-arbos) +endif() diff --git a/abs-repr/README.md b/abs-repr/README.md new file mode 100644 index 00000000..abdf04f6 --- /dev/null +++ b/abs-repr/README.md @@ -0,0 +1,234 @@ +Abstract Representation +======================= + +This folder contains the implementation of the ARBOS tool. + +Introduction +------------ + +The ARBOS tool produces a program model from an _AR file_. An _AR file_ is a text file that represents the program model in S-expressions using the Abstract Representation (AR) specification. An _AR file_ is produced by the tools under [../frontends](../frontends). + +ARBOS is a plugin framework that reads an _AR file_ and creates the AR program model in memory for registered ARBOS passes to traverse and perform analysis on it. + +Related documents include: + +* [docs/AR_SPEC.md](docs/AR_SPEC.md) documents the AR specification + +Build and Install +----------------- + +The ARBOS tool can be independently built. The source project uses cmake to generate build files needed by your build tool. + +To build arbos, run the following commands within the abs-repr directory: + +``` +$ mkdir build +$ cd build +$ cmake -DCMAKE_INSTALL_PREFIX= .. +$ make +$ make install +``` + +### Example passes + +We provide example passes to illustrate how to extend ARBOS by integrating your own passes. The source code of these passes are located under [src/passes/examples](src/passes/examples). To build these example passes, you can simply run the following command in the same `build` directory: + +``` +$ make example-passes +``` + +And use the following command to install the example passes: + +``` +$ make install +``` + +### Documentation + +To build and install our doxygen documentation, run the following command under the same `build` directory: + +``` +$ make docs +``` + +and use the following command to instal the documentation: + +``` +$ make install +``` + +### Running the regression tests + +The regression tests are verified by verifiers implemented as ARBOS passes. These passes are located under [tests/regr-tests/verifier-passes](tests/regr-tests/verifier-passes) and must be built before we can run the regression tests. + +To build and install the verifier passes, run the following command under the same `build` directory: + +``` +$ make verifier-passes +$ make install +``` + +To run the regression tests, please make sure to add IKOS to your path: + +``` +$ PATH=/path/to/ikos-install-directory/bin:$PATH +``` + +Now, simply run: + +``` +$ make test +``` + +How to run ARBOS +---------------- + +The **arbos** command requires users to specify a list of ARBOS passes to run on the AR provided by the input AR file. Suppose we want to run the **Hello World** ARBOS pass on an AR file `file.ar`, then we use the following command under the directory where you've generated `file.ar`: + +``` +$ arbos -load=/path/to/libhello.dylib -hello < file.ar +``` + +You should obtain the following output: + +``` +dlopen successful on libhello.dylib +Loaded ARBOS pass: hello - Demo pass that prints Hello World! +1 pass(es) registered. +Executing pass - hello Demo pass that prints Hello World! +Hello World! +``` + +What you have done is to execute the **Hello World** ARBOS pass on the AR generated from `file.ar`. This pass simply prints "Hello World!" in the console. + +Writing an ARBOS pass +--------------------- + +The ARBOS example passes are located under [src/passes/examples](src/passes/examples). + +If you want to create a new pass, the easiest way is to create it out of a template. The `hello` pass is an obvious choice. Suppose you want to create a pass named `mypass`. Below shows the implementation of the pass: + +```c++ +#include + +#include "arbos/semantics/ar.hpp" + +using namespace arbos; + +namespace { + +class MyPass : public Pass { +public: + MyPass() : Pass("mypass", "My ARBOS pass.") {}; + virtual ~MyPass() {} + virtual void execute(AR_Node_Ref< AR_Bundle > bundle) { + std::cout << "This is the entry point for the pass" << std::endl; + } +}; + +} + +extern "C" Pass* init() { + return new MyPass(); +} +``` + +Then go under the [examples](abs-repr/src/passes/examples) directory and edit the [CMakeLists.txt](abs-repr/src/passes/examples/CMakeLists.txt) file. Add the following line at the beginning of the file: + +``` +add_library(mypass SHARED mypass.cpp) +target_link_libraries(mypass arbos-api) +install(TARGETS mypass DESTINATION lib OPTIONAL) +``` + +And append `mypass` in the list of arguments in `add_custom_target`: + +``` +add_custom_target(example-passes DEPENDS hello options visitor mypass) +``` + +Now you can build and installed the example passes using the following command: + +``` +$ make example-passes +$ make install +``` + +`mypass` is now built. To try it out, please go under the directory where `file.ar` is located and type: + +``` +$ arbos -load=libmypass.dylib -mypass < file.ar +``` + +You should obtain the following output: + +``` +dlopen successful on libmypass.dylib +Loaded ARBOS pass: mypass - My ARBOS pass. +1 pass(es) registered. +Executing pass - mypass My ARBOS pass. +This is the entry point for the pass +``` + +Overview of the source code +--------------------------- + +``` +. +├── CMakeLists.txt +├── README.md +├── docs +│ ├── AR_SPEC.md +│ └── doxygen +│ ├── Doxyfile.in +│ ├── DoxygenLayout.xml +│ └── customdoxygen.css +├── include +│ └── arbos +│ ├── common +│ ├── io +│ └── semantics +├── src +│ ├── arbos +│ │ ├── api +│ │ └── arbos.cpp +│ └── passes +│ ├── dumps +│ └── examples +└── tests + └── regression + ├── CMakeLists.txt + ├── tests + ├── utils + └── verifier-passes +``` + +#### docs/ + +* [docs/AR_SPEC.md](docs/AR_SPEC.md) documents the AR specification. + +* [docs/doxygen](docs/doxygen) contains Doxygen files. + +#### include/ + +* [include/arbos/common](include/arbos/common) contains all basic data structures used across the infrastructure. For example, FP representation, big integers, etc. + +* [include/arbos/io](include/arbos/io) contains interfaces and adapters for various exchange formats for AR. For example, importing and exporting AR from and to S-expressions. + +* [include/arbos/semantics](include/arbos/semantics) contains data structures for defining semantics for the CFG. + +#### src/ + +* [src/arbos/api](src/arbos/api) contains implementation of ARBOS API. + +* [src/arbos/arbos.cpp](src/arbos/arbos.cpp) implements the driver of the plugin framework. + +* [src/passes/examples](src/passes/examples) contains sample ARBOS passes. + +#### tests/ + +* [tests/regression/tests](tests/regression/tests) contains test programs in C/C++ for verifying the generated AR program models. + +* [tests/regression/utils](tests/regression/utils) contains scripts that support the execution of the regression tests. + +* [tests/regression/verifier-passes](tests/regression/verifier-passes) contains ARBOS passes that verify the generated AR program models. diff --git a/abs-repr/docs/AR_SPEC.md b/abs-repr/docs/AR_SPEC.md new file mode 100644 index 00000000..e7b833fe --- /dev/null +++ b/abs-repr/docs/AR_SPEC.md @@ -0,0 +1,526 @@ +# AR Specification + +## Introduction + +This document illustrates the Abstract Representation (AR) in S-expressions. + +## AR Specification +Serialized versions of the AR are encoded in an extended S-expression-like format that permits preservation of sharing and recursion. It is strictly more expressive than XML (i.e., its underlying topology is that of a directed graph rather than a tree). + +### Atoms + +#### Strings + +All strings are prefixed by $. Punctuation and white space must be escaped by being prefixed with '\', e.g.: + +``` +$fred +$this\ has\ spaces\ in\ it +$Hello\,\ World\! +$yada\09\20\23\24\25\24\24\5E\25\5E\24\5E\25\5E\26\25\2A\26\20yada\0A for "yada\t #$%$$^%^$^%^&%*& yada\n" +``` + +#### Integers + +Integers are prefixed with #, e.g. + +``` +#1 +#-345 +``` + +#### Floating point + +``` +^0.88 +``` + +#### Q numbers + +Q numbers are prefixed with %, e.g. + +``` +%-4/7 +``` + +#### UIDs + +Each AR node has an unique identification represented as unsigned 64bit integer. UIDs are prefixed with !, e.g. + +``` +!33 +``` + +### S-expressions + +#### Types + +The AR output lists all the types referenced in the entire program prior to the function definitions. Each type is associated with a UID. The following illustrates the general s-expression format for types. + +``` +(![uid] ($type ($[type_name]) ([...]))) +``` + +##### Integer type + +``` +($int (#8) ($realsize (#8)) ($storesize (#1))) +``` + +represents an integer type of size 8 bits. + +##### Floating point type + +``` +($float ($double) ($realsize (#64)) ($storesize (#8))) +``` + +##### Array type + +``` +($array ($len (#10)) ($ty (!4)))))), where #10 represents the length of the array; ($ty (!4)) represents the cell type. +``` + +##### Pointer type + +``` +($ptr ($ty (!18)) ($realsize (#64)) ($storesize (#8))), where ($ty (!18)) represents the referenced type +``` + +##### Struct type + +The struct type includes information of the struct layout, alignment, and the total padded size in bits. The format of the layout specifies a sequence of (#padded_offset (!type-uid-ref)) for each field of the struct. + +``` +($struct ($layout (#0 (!16))) ($align (#64)) ($realsize (#128)) ($storesize (#16))) +``` + +##### Function type + +``` +($function ($return_ty (!34)) ($params_ty (!48) (!25)) ($isVarArg ($False))) +``` + +##### Void type + +``` +($void ($realsize (#0)) ($storesize (#0))) +``` + +#### Constants + +The following illustrates the general s-expression format for constants. + +``` +($cst ($[constant-type]) ([...])) +``` + +##### Integer constant + +``` +($constantint ($val (#0)) ($ty (!2))) +``` + +##### Floating point constant + +``` +($constantfp ($val (^0.88)) ($ty (!4))) +``` + +##### Null constant + +``` +($constantpointernull ($ty (!22))) +``` + +##### Undefined + +``` +(!23 ($def ($undefined) (!11))) +``` + +##### Range + +``` +($range + ($values + ($value (#0) ($cst ($constantfp ($val (^0x0p0)) ($ty (!4))))) + ($value (#64) ($cst ($constantfp ($val (^0x0p0)) ($ty (!4))))) + ($value (#128) ($cst ($constantfp ($val (^0x0p0)) ($ty (!4))))) + ($value (#192) ($cst ($constantfp ($val (^0x0p0)) ($ty (!4))))) + ($value (#256) ($cst ($constantfp ($val (^0x0p0)) ($ty (!4))))) + ($value (#320) ($cst ($constantfp ($val (^0x0p0)) ($ty (!4))))) + ($value (#384) ($cst ($constantfp ($val (^0x0p0)) ($ty (!4))))) + ($value (#448) ($cst ($constantfp ($val (^0x0p0)) ($ty (!4))))) + ($value (#512) ($cst ($constantfp ($val (^0x0p0)) ($ty (!4))))) + ($value (#576) ($cst ($constantfp ($val (^0x0p0)) ($ty (!4))))) + ($ty (!7)))) +``` + +##### Variable Address + +``` +($globalvariableref ($name ($a)) ($gv (!2)) ($ty (!7))), or +($localvariableref ($name ($a)) ($ty (!11))) +``` + +#### Variables + +##### Global variable + +``` +($gv ($name ($)) ($ty (!)) ($align (#)) ($code) ($debug ($srcloc))) +``` + +##### Global variable reference + +``` +($globalvariableref ($name ($a)) ($gv (!2)) ($ty (!7))) +``` + +##### Local variable + +``` +($local_var ($var ($name ($str)) ($ty (!2)) ($align (#4) ))) +``` + +##### Local variable reference + +``` +($localvariableref ($name ($a)) ($ty (!7))) +``` + +##### Internal variable + +``` +($var ($name ($tmp)) ($ty (!11))) +``` + + +#### Operands + +##### Variable operand + +``` +($var ($name ($i.0)) ($ty (!2)))), where ($i\2E0) (that is "i.0") is the name of the variable and (!2) is the reference uid of its type. +``` + + +##### Constant operand + +``` +($cst ($constantint ($val (#9)) ($ty (!9))) +``` + + +#### Statements + +##### Assignment + +``` +($assign ($lhs ($var ($name ($i.o)) ($ty (!7)))) ($rhs ($var ($name ($tmp5)) ($ty (!7)))) ($debug ($srcloc))), where \ + ($lhs ($var ($name ($i.0)) ($ty (!7)))) is the result, while ($rhs ($var ($name ($tmp5)) ($ty (!7)))) \ + is the operand of the right-hand-side. +``` + +##### Asssertion + +``` +($assert ($kind ($i)) + ($cmp ($cond ($true)) ($pred ($eq)) + ($ops ($var ($name ($eh_select)) ($ty (!24))) ($var ($name ($eh_typeid)) ($ty (!24))))) + ($debug ($srcloc ($line (#48)) ($file (!27))))) +``` + +##### Arithmic operation + +``` +($mul + ($lhs ($var ($name ($__v:43)) ($ty (!16)))) + ($rhs ($cst ($constantint ($val (#3)) ($ty (!16)))) + ($cst ($constantint ($val (#0)) ($ty (!16))))) + ($debug ($srcloc ($line (#-1)) ($file (!17))))), where + ($var ($name ($__v:43)) ($ty (!16))) is the result, while \ + ($cst ($constantint ($val (#3)) ($ty (!16)))) and \ + ($cst ($constantint ($val (#0)) ($ty (!16)))) are operands on the right-hand-side. +``` + +##### AR_FP_Op + +``` +($fmul + ($lhs ($var ($name ($tmp3)) ($ty (!4)))) + ($rhs ($var ($name ($tmp1)) ($ty (!4))) ($var ($name ($tmp2)) ($ty (!4)))) + ($debug ($srcloc ($line (#9)) ($file (!6))))) +``` + +##### AR_Bitwise_Op + +``` +($or + ($lhs ($var ($name ($tmp)) ($ty (!2)))) + ($rhs ($cst ($constantint ($val (#4)) ($ty (!2)))) ($cst ($constantint ($val (#5)) ($ty (!2))))) + ($debug ($srcloc ($line (#3)) ($file (!6))))) +``` + +##### AR_Conv_Op + +``` +($sitofp + ($lhs ($var ($name ($tmp1)) ($ty (!4)))) + ($rhs ($var ($name ($tmp)) ($ty (!11)))) + ($debug ($srcloc ($line (#9)) ($file (!6))))) +``` + +##### AR_Integer_Comparison + +``` +($cmp ($cond ($true)) ($pred ($sle)) ($ops ($var ($name ($i\2E0)) ($ty (!11))) ($cst ($constantint ($val (#22)) ($ty (!11)))))) +``` + +##### AR_FP_Comparison + +``` +($cmp ($cond ($true)) ($pred ($sle)) ($ops ($var ($name ($i\2E0)) ($ty (!11))) ($cst ($constantint ($val (#22)) ($ty (!11)))))) +``` + +##### AR_MemSet + +``` + ($memset + ($ret ($var ($name ($\5C5Fv)) ($ty (!12)))) + ($dest ($var ($name ($\5C5F\5C5Fv)) ($ty (!9)))) + ($val ($cst ($constantint ($val (#13)) ($ty (!10))))) + ($len ($cst ($constantint ($val (#14)) ($ty (!15))))) + ($align (#16)) + ($isvolatile ($cst ($constantint ($val (#17)) ($ty (!18))))) + ($debug ($srcloc ($line (#7)) ($file (!6))))) +``` + +##### AR_MemCpy +``` + ($memcpy + ($ret ()) + ($dest ()) + ($src ()) + ($len ()) + ($align (#16)) + ($isvolatile ($cst ($constantint ($val (#17)) ($ty (!18))))) + ($debug ($srcloc ($line (#7)) ($file (!6))))) +``` + +##### AR_MemMove +``` + ($memmove + ($ret ()) + ($dest ()) + ($src ()) + ($len ()) + ($align (#16)) + ($isvolatile ($cst ($constantint ($val (#17)) ($ty (!18))))) + ($debug ($srcloc ($line (#7)) ($file (!6))))) +``` + +##### AR_VA_Start + +``` +($va_start ($var ($name ($vl12)) ($ty (!6))) ($debug ($srcloc ($line (#14)) ($file (!14))))) +``` + +##### AR_VA_Copy + +``` +($va_copy ($dest ($var ($name ($vl_count35)) ($ty (!6)))) ($src ($var ($name ($vl46)) ($ty (!6)))) ($debug ($srcloc ($line (#17)) ($file (!14))))) +``` + +##### AR_VA_End + +``` +($va_end ($var ($name ($vl_count1213)) ($ty (!6))) ($debug ($srcloc ($line (#22)) ($file (!14))))) +``` + +##### AR_VA_Arg + +``` +($va_arg ($ret) ($ptr) ($debug)) +``` + +##### AR_Pointer_Shift + +``` +($ptrshift + ($lhs ($var ($name ($__v:1)) ($ty (!19)))) + ($rhs ($cst ($globalvariableref ($name ($_ZTI1A)) ($gv (!3)) ($ty (!14)))) + ($cst ($constantint ($val (#0)) ($ty (!20))))) + ($debug ($srcloc ($line (#-1)) ($file (!13))))) +``` + +##### AR_Allocate + +``` +($allocate + ($dest ($cst ($localvariableref ($name ($foo.vla)) ($ty (!13))))) + ($alloca_ty (!10)) + ($array_size ($var ($name ($foo._2)) ($ty (!7)))) + ($debug ($srcloc ($line (#3)) ($col (#5)) ($file (!11))))) +``` + +##### AR_Store + +``` +($store ($lhs ($var ($name ($d)) ($ty (!4)))) ($rhs ($constantfp ($val (^0x1.c28f5c28f5c29p-1)) ($ty (!4)))) ($align (#4)) ($debug ($srcloc ($line (#3)) ($file (!5))))) +``` + +##### AR_Load + +``` +($load ($lhs ($var ($name ($tmp2)) ($ty (!4)))) ($rhs ($cst ($constantint ($val (#17)) ($ty (!3))))) ($align (#4)) ($debug ($srcloc ($line (#9)) ($file (!6))))) +``` + +##### AR_Insert_Element + +``` +($insertelem + ($var ($name ($mrv4)) ($ty (!13))) // result + ($var ($name ($__v:51)) ($ty (!13))) // aggregate value + ($var ($name ($mrv)) ($ty (!14))) // element + ($var ($name ($__v:50)) ($ty (!20))) // offset + ($debug ($srcloc ($line (#15)) ($file (!15))))) +``` + +##### AR_Extract_Element + +``` +($extractelem + ($var ($name ($mrv_gr)) ($ty (!14))) // result + ($var ($name ($tmp)) ($ty (!13))) // aggregate value + ($var ($name ($__v:4)) ($ty (!20))) // offset + ($debug ($srcloc ($line (#20)) ($file (!15))))) +``` + +##### AR_Return_Value + +``` +($ret ($rhs ($cst ($constantint ($val (#0)) ($ty (!2))))) ($debug ($srcloc ($line (#9)) ($file (!8))))) +``` + +##### AR_Call + +``` +($call + ($ret ($var ($name ($main._4)) ($ty (!9)))) + ($callee ($var ($name ($__v:5)) ($ty (!12)))) + ($args ($a ($cst ($constantint ($val (#1)) ($ty (!9)))))) + ($inlineAsm ($true)) + ($debug ($srcloc ($line (#7)) ($file (!11))))) +``` + +##### AR_Invoke + +``` +($invoke + ($call ($ret ($var ($name ($__v:119)) ($ty (!34)))) + ($callee ($cst ($constantfunctionptr ($name ($_Z3runP1A)) ($ty (!53))))) + ($args ($a ($var ($name ($tmp)) ($ty (!35))))) + ($debug ($srcloc ($line (#45)) ($file (!13))))) + ($br ($normal ($invcont)) ($exception ($lpad))) + ($debug ($srcloc ($line (#45)) ($file (!13))))) +``` + +##### AR_Abstract_Memory + +``` +($abstractmemory + ($ptr ($cst ($globalvariableref ($name ($_ZTVN10__cxxabiv117__class_type_infoE)) ($gv (!4)) ($ty (!21))))) + ($len ($cst ($constantint ($val (#0)) ($ty (!20))))) + ($debug ($srcloc ($line (#-1)) ($file (!13))))) +``` + +##### AR_Abstract_Variable + +``` +($abstractvariable ($var ($name ($__v:63)) ($ty (!24))) ($debug ($srcloc ($line (#31)) ($file (!27))))) +``` + +##### AR_Landing_Pad + +``` +($def (!10 ($type ($ptr ($ty (!9)) ($realsize (#64)) ($storesize (#8)))))) + +($def (!18 ($type ($int ($realsize (#32)) ($storesize (#4)))))) + +($def (!42 ($type ($struct + ($layout (#0 (!10)) + (#8 (!18))) + ($align (#64)) + ($realsize (#128)) + ($storesize (#16)))))) + +($landingpad + ($exception + ($var + ($name ($main._invoke.cont.3)) ($ty (!42)))) + ($debug ($srcloc ($line (#27)) ($file (!34))))) +``` + +##### AR_Resume + +``` +($resume + ($exception + ($var ($name ($__v:173)) ($ty (!40)))) + ($debug ($srcloc ($line (#22)) ($file (!48))))) + +``` + +##### AR_Unreachable + +``` +($unreachable ($debug ($srcloc ($line (#48)) ($file (!27))))) +``` + +#### AR_Function + +``` +($function ($name ()) ($ty ()) ($params () ...) ($local_vars () ...) ($code ($basicblock) ...)) +``` + +#### AR_Code + +``` +($code + ($entry ($entry)) + ($exit ($return)) + ($unreachable ($if.then)) + ($ehresume ($eh.resume)) + ($basicblocks ($basicblock) ...) + ($trans ($edge () ()) ...)) +``` + +We support three different types of terminating blocks in AR_Code: `exit`, `unreachable`, and `ehresume`. In an `AR_Code`, we allow at most one basic block per type. Using the LLVM frontend, we transform the LLVM IR using the `UnifyFunctionExitNodes` pass to obtain the `exit` and `unreachable` blocks, where each represents the unified block for all returning and unreachable blocks, respectively. `ehresume` is already a unified block that contains the `resume` instruction to resume propagation of an exception whose unwinding was interrupted with the LLVM `landingpad` instruction. Note that ($exit), ($unreachable), and ($ehresume) may have zero arguments, which means these blocks may be absent in the function in the LLVM IR. If the exit block is missing, then this means the function does not terminate with a return block that ends with a return instruction. + +#### AR_Basic_Block + +``` +($basicblock ($name ()) ($instructions () ...) ... ) +``` + +### Metainfo provided by the LLVM frontend + +``` +($metainfo ($targettriple ($x86_64-apple-macosx10.11.0))) +($metainfo ($endianess ($LittleEndian))) +($metainfo ($sizeofptr (#64))) +``` + +### File + +``` +(!6 ($file) ($/path/to/some/directory/unitests/5/loop.c)) +``` + +### AR_Source_Location + +``` +($srcloc ($line (#4)) ($col (#3)) ($file (!9))) +``` diff --git a/abs-repr/docs/doxygen/Doxyfile.in b/abs-repr/docs/doxygen/Doxyfile.in new file mode 100644 index 00000000..08f48569 --- /dev/null +++ b/abs-repr/docs/doxygen/Doxyfile.in @@ -0,0 +1,2311 @@ +# Doxyfile 1.8.7 + +# This file describes the settings to be used by the documentation system +# doxygen (www.doxygen.org) for a project. +# +# All text after a double hash (##) is considered a comment and is placed in +# front of the TAG it is preceding. +# +# All text after a single hash (#) is considered a comment and will be ignored. +# The format is: +# TAG = value [value, ...] +# For lists, items can also be appended using: +# TAG += value [value, ...] +# Values that contain spaces should be placed between quotes (\" \"). + +#--------------------------------------------------------------------------- +# Project related configuration options +#--------------------------------------------------------------------------- + +# This tag specifies the encoding used for all characters in the config file +# that follow. The default is UTF-8 which is also the encoding used for all text +# before the first occurrence of this tag. Doxygen uses libiconv (or the iconv +# built into libc) for the transcoding. See http://www.gnu.org/software/libiconv +# for the list of possible encodings. +# The default value is: UTF-8. + +DOXYFILE_ENCODING = UTF-8 + +# The PROJECT_NAME tag is a single word (or a sequence of words surrounded by +# double-quotes, unless you are using Doxywizard) that should identify the +# project for which the documentation is generated. This name is used in the +# title of most generated pages and in a few other places. +# The default value is: My Project. + +PROJECT_NAME = "IKOS" + +# The PROJECT_NUMBER tag can be used to enter a project or revision number. This +# could be handy for archiving the generated documentation or if some version +# control system is used. + +PROJECT_NUMBER = + +# Using the PROJECT_BRIEF tag one can provide an optional one line description +# for a project that appears at the top of each page and should give viewer a +# quick idea about the purpose of the project. Keep the description short. + +PROJECT_BRIEF = "IKOS is a C++ library designed to facilitate the development of sound static analyzers based on Abstract Interpretation. Specialization of a static analyzer for an application or family of applications is critical for achieving both precision and scalability. Developing such an analyzer is arduous and requires significant expertise in Abstract Interpretation." + +# With the PROJECT_LOGO tag one can specify an logo or icon that is included in +# the documentation. The maximum height of the logo should not exceed 55 pixels +# and the maximum width should not exceed 200 pixels. Doxygen will copy the logo +# to the output directory. + +PROJECT_LOGO = + +# The OUTPUT_DIRECTORY tag is used to specify the (relative or absolute) path +# into which the generated documentation will be written. If a relative path is +# entered, it will be relative to the location where doxygen was started. If +# left blank the current directory will be used. + +OUTPUT_DIRECTORY = "@CMAKE_CURRENT_BINARY_DIR@/docs" + +# If the CREATE_SUBDIRS tag is set to YES, then doxygen will create 4096 sub- +# directories (in 2 levels) under the output directory of each output format and +# will distribute the generated files over these directories. Enabling this +# option can be useful when feeding doxygen a huge amount of source files, where +# putting all generated files in the same directory would otherwise causes +# performance problems for the file system. +# The default value is: NO. + +CREATE_SUBDIRS = NO + +# If the ALLOW_UNICODE_NAMES tag is set to YES, doxygen will allow non-ASCII +# characters to appear in the names of generated files. If set to NO, non-ASCII +# characters will be escaped, for example _xE3_x81_x84 will be used for Unicode +# U+3044. +# The default value is: NO. + +ALLOW_UNICODE_NAMES = NO + +# The OUTPUT_LANGUAGE tag is used to specify the language in which all +# documentation generated by doxygen is written. Doxygen will use this +# information to generate all constant output in the proper language. +# Possible values are: Afrikaans, Arabic, Armenian, Brazilian, Catalan, Chinese, +# Chinese-Traditional, Croatian, Czech, Danish, Dutch, English (United States), +# Esperanto, Farsi (Persian), Finnish, French, German, Greek, Hungarian, +# Indonesian, Italian, Japanese, Japanese-en (Japanese with English messages), +# Korean, Korean-en (Korean with English messages), Latvian, Lithuanian, +# Macedonian, Norwegian, Persian (Farsi), Polish, Portuguese, Romanian, Russian, +# Serbian, Serbian-Cyrillic, Slovak, Slovene, Spanish, Swedish, Turkish, +# Ukrainian and Vietnamese. +# The default value is: English. + +OUTPUT_LANGUAGE = English + +# If the BRIEF_MEMBER_DESC tag is set to YES doxygen will include brief member +# descriptions after the members that are listed in the file and class +# documentation (similar to Javadoc). Set to NO to disable this. +# The default value is: YES. + +BRIEF_MEMBER_DESC = YES + +# If the REPEAT_BRIEF tag is set to YES doxygen will prepend the brief +# description of a member or function before the detailed description +# +# Note: If both HIDE_UNDOC_MEMBERS and BRIEF_MEMBER_DESC are set to NO, the +# brief descriptions will be completely suppressed. +# The default value is: YES. + +REPEAT_BRIEF = YES + +# This tag implements a quasi-intelligent brief description abbreviator that is +# used to form the text in various listings. Each string in this list, if found +# as the leading text of the brief description, will be stripped from the text +# and the result, after processing the whole list, is used as the annotated +# text. Otherwise, the brief description is used as-is. If left blank, the +# following values are used ($name is automatically replaced with the name of +# the entity):The $name class, The $name widget, The $name file, is, provides, +# specifies, contains, represents, a, an and the. + +ABBREVIATE_BRIEF = + +# If the ALWAYS_DETAILED_SEC and REPEAT_BRIEF tags are both set to YES then +# doxygen will generate a detailed section even if there is only a brief +# description. +# The default value is: NO. + +ALWAYS_DETAILED_SEC = NO + +# If the INLINE_INHERITED_MEMB tag is set to YES, doxygen will show all +# inherited members of a class in the documentation of that class as if those +# members were ordinary class members. Constructors, destructors and assignment +# operators of the base classes will not be shown. +# The default value is: NO. + +INLINE_INHERITED_MEMB = NO + +# If the FULL_PATH_NAMES tag is set to YES doxygen will prepend the full path +# before files name in the file list and in the header files. If set to NO the +# shortest path that makes the file name unique will be used +# The default value is: YES. + +FULL_PATH_NAMES = YES + +# The STRIP_FROM_PATH tag can be used to strip a user-defined part of the path. +# Stripping is only done if one of the specified strings matches the left-hand +# part of the path. The tag can be used to show relative paths in the file list. +# If left blank the directory from which doxygen is run is used as the path to +# strip. +# +# Note that you can specify absolute paths here, but also relative paths, which +# will be relative from the directory where doxygen is started. +# This tag requires that the tag FULL_PATH_NAMES is set to YES. + +STRIP_FROM_PATH = + +# The STRIP_FROM_INC_PATH tag can be used to strip a user-defined part of the +# path mentioned in the documentation of a class, which tells the reader which +# header file to include in order to use a class. If left blank only the name of +# the header file containing the class definition is used. Otherwise one should +# specify the list of include paths that are normally passed to the compiler +# using the -I flag. + +STRIP_FROM_INC_PATH = + +# If the SHORT_NAMES tag is set to YES, doxygen will generate much shorter (but +# less readable) file names. This can be useful is your file systems doesn't +# support long names like on DOS, Mac, or CD-ROM. +# The default value is: NO. + +SHORT_NAMES = NO + +# If the JAVADOC_AUTOBRIEF tag is set to YES then doxygen will interpret the +# first line (until the first dot) of a Javadoc-style comment as the brief +# description. If set to NO, the Javadoc-style will behave just like regular Qt- +# style comments (thus requiring an explicit @brief command for a brief +# description.) +# The default value is: NO. + +JAVADOC_AUTOBRIEF = NO + +# If the QT_AUTOBRIEF tag is set to YES then doxygen will interpret the first +# line (until the first dot) of a Qt-style comment as the brief description. If +# set to NO, the Qt-style will behave just like regular Qt-style comments (thus +# requiring an explicit \brief command for a brief description.) +# The default value is: NO. + +QT_AUTOBRIEF = NO + +# The MULTILINE_CPP_IS_BRIEF tag can be set to YES to make doxygen treat a +# multi-line C++ special comment block (i.e. a block of //! or /// comments) as +# a brief description. This used to be the default behavior. The new default is +# to treat a multi-line C++ comment block as a detailed description. Set this +# tag to YES if you prefer the old behavior instead. +# +# Note that setting this tag to YES also means that rational rose comments are +# not recognized any more. +# The default value is: NO. + +MULTILINE_CPP_IS_BRIEF = NO + +# If the INHERIT_DOCS tag is set to YES then an undocumented member inherits the +# documentation from any documented member that it re-implements. +# The default value is: YES. + +INHERIT_DOCS = YES + +# If the SEPARATE_MEMBER_PAGES tag is set to YES, then doxygen will produce a +# new page for each member. If set to NO, the documentation of a member will be +# part of the file/class/namespace that contains it. +# The default value is: NO. + +SEPARATE_MEMBER_PAGES = NO + +# The TAB_SIZE tag can be used to set the number of spaces in a tab. Doxygen +# uses this value to replace tabs by spaces in code fragments. +# Minimum value: 1, maximum value: 16, default value: 4. + +TAB_SIZE = 4 + +# This tag can be used to specify a number of aliases that act as commands in +# the documentation. An alias has the form: +# name=value +# For example adding +# "sideeffect=@par Side Effects:\n" +# will allow you to put the command \sideeffect (or @sideeffect) in the +# documentation, which will result in a user-defined paragraph with heading +# "Side Effects:". You can put \n's in the value part of an alias to insert +# newlines. + +ALIASES = + +# This tag can be used to specify a number of word-keyword mappings (TCL only). +# A mapping has the form "name=value". For example adding "class=itcl::class" +# will allow you to use the command class in the itcl::class meaning. + +TCL_SUBST = + +# Set the OPTIMIZE_OUTPUT_FOR_C tag to YES if your project consists of C sources +# only. Doxygen will then generate output that is more tailored for C. For +# instance, some of the names that are used will be different. The list of all +# members will be omitted, etc. +# The default value is: NO. + +OPTIMIZE_OUTPUT_FOR_C = NO + +# Set the OPTIMIZE_OUTPUT_JAVA tag to YES if your project consists of Java or +# Python sources only. Doxygen will then generate output that is more tailored +# for that language. For instance, namespaces will be presented as packages, +# qualified scopes will look different, etc. +# The default value is: NO. + +OPTIMIZE_OUTPUT_JAVA = NO + +# Set the OPTIMIZE_FOR_FORTRAN tag to YES if your project consists of Fortran +# sources. Doxygen will then generate output that is tailored for Fortran. +# The default value is: NO. + +OPTIMIZE_FOR_FORTRAN = NO + +# Set the OPTIMIZE_OUTPUT_VHDL tag to YES if your project consists of VHDL +# sources. Doxygen will then generate output that is tailored for VHDL. +# The default value is: NO. + +OPTIMIZE_OUTPUT_VHDL = NO + +# Doxygen selects the parser to use depending on the extension of the files it +# parses. With this tag you can assign which parser to use for a given +# extension. Doxygen has a built-in mapping, but you can override or extend it +# using this tag. The format is ext=language, where ext is a file extension, and +# language is one of the parsers supported by doxygen: IDL, Java, Javascript, +# C#, C, C++, D, PHP, Objective-C, Python, Fortran (fixed format Fortran: +# FortranFixed, free formatted Fortran: FortranFree, unknown formatted Fortran: +# Fortran. In the later case the parser tries to guess whether the code is fixed +# or free formatted code, this is the default for Fortran type files), VHDL. For +# instance to make doxygen treat .inc files as Fortran files (default is PHP), +# and .f files as C (default is Fortran), use: inc=Fortran f=C. +# +# Note For files without extension you can use no_extension as a placeholder. +# +# Note that for custom extensions you also need to set FILE_PATTERNS otherwise +# the files are not read by doxygen. + +EXTENSION_MAPPING = + +# If the MARKDOWN_SUPPORT tag is enabled then doxygen pre-processes all comments +# according to the Markdown format, which allows for more readable +# documentation. See http://daringfireball.net/projects/markdown/ for details. +# The output of markdown processing is further processed by doxygen, so you can +# mix doxygen, HTML, and XML commands with Markdown formatting. Disable only in +# case of backward compatibilities issues. +# The default value is: YES. + +MARKDOWN_SUPPORT = YES + +# When enabled doxygen tries to link words that correspond to documented +# classes, or namespaces to their corresponding documentation. Such a link can +# be prevented in individual cases by by putting a % sign in front of the word +# or globally by setting AUTOLINK_SUPPORT to NO. +# The default value is: YES. + +AUTOLINK_SUPPORT = YES + +# If you use STL classes (i.e. std::string, std::vector, etc.) but do not want +# to include (a tag file for) the STL sources as input, then you should set this +# tag to YES in order to let doxygen match functions declarations and +# definitions whose arguments contain STL classes (e.g. func(std::string); +# versus func(std::string) {}). This also make the inheritance and collaboration +# diagrams that involve STL classes more complete and accurate. +# The default value is: NO. + +BUILTIN_STL_SUPPORT = NO + +# If you use Microsoft's C++/CLI language, you should set this option to YES to +# enable parsing support. +# The default value is: NO. + +CPP_CLI_SUPPORT = NO + +# Set the SIP_SUPPORT tag to YES if your project consists of sip (see: +# http://www.riverbankcomputing.co.uk/software/sip/intro) sources only. Doxygen +# will parse them like normal C++ but will assume all classes use public instead +# of private inheritance when no explicit protection keyword is present. +# The default value is: NO. + +SIP_SUPPORT = NO + +# For Microsoft's IDL there are propget and propput attributes to indicate +# getter and setter methods for a property. Setting this option to YES will make +# doxygen to replace the get and set methods by a property in the documentation. +# This will only work if the methods are indeed getting or setting a simple +# type. If this is not the case, or you want to show the methods anyway, you +# should set this option to NO. +# The default value is: YES. + +IDL_PROPERTY_SUPPORT = YES + +# If member grouping is used in the documentation and the DISTRIBUTE_GROUP_DOC +# tag is set to YES, then doxygen will reuse the documentation of the first +# member in the group (if any) for the other members of the group. By default +# all members of a group must be documented explicitly. +# The default value is: NO. + +DISTRIBUTE_GROUP_DOC = NO + +# Set the SUBGROUPING tag to YES to allow class member groups of the same type +# (for instance a group of public functions) to be put as a subgroup of that +# type (e.g. under the Public Functions section). Set it to NO to prevent +# subgrouping. Alternatively, this can be done per class using the +# \nosubgrouping command. +# The default value is: YES. + +SUBGROUPING = YES + +# When the INLINE_GROUPED_CLASSES tag is set to YES, classes, structs and unions +# are shown inside the group in which they are included (e.g. using \ingroup) +# instead of on a separate page (for HTML and Man pages) or section (for LaTeX +# and RTF). +# +# Note that this feature does not work in combination with +# SEPARATE_MEMBER_PAGES. +# The default value is: NO. + +INLINE_GROUPED_CLASSES = NO + +# When the INLINE_SIMPLE_STRUCTS tag is set to YES, structs, classes, and unions +# with only public data fields or simple typedef fields will be shown inline in +# the documentation of the scope in which they are defined (i.e. file, +# namespace, or group documentation), provided this scope is documented. If set +# to NO, structs, classes, and unions are shown on a separate page (for HTML and +# Man pages) or section (for LaTeX and RTF). +# The default value is: NO. + +INLINE_SIMPLE_STRUCTS = NO + +# When TYPEDEF_HIDES_STRUCT tag is enabled, a typedef of a struct, union, or +# enum is documented as struct, union, or enum with the name of the typedef. So +# typedef struct TypeS {} TypeT, will appear in the documentation as a struct +# with name TypeT. When disabled the typedef will appear as a member of a file, +# namespace, or class. And the struct will be named TypeS. This can typically be +# useful for C code in case the coding convention dictates that all compound +# types are typedef'ed and only the typedef is referenced, never the tag name. +# The default value is: NO. + +TYPEDEF_HIDES_STRUCT = NO + +# The size of the symbol lookup cache can be set using LOOKUP_CACHE_SIZE. This +# cache is used to resolve symbols given their name and scope. Since this can be +# an expensive process and often the same symbol appears multiple times in the +# code, doxygen keeps a cache of pre-resolved symbols. If the cache is too small +# doxygen will become slower. If the cache is too large, memory is wasted. The +# cache size is given by this formula: 2^(16+LOOKUP_CACHE_SIZE). The valid range +# is 0..9, the default is 0, corresponding to a cache size of 2^16=65536 +# symbols. At the end of a run doxygen will report the cache usage and suggest +# the optimal cache size from a speed point of view. +# Minimum value: 0, maximum value: 9, default value: 0. + +LOOKUP_CACHE_SIZE = 0 + +#--------------------------------------------------------------------------- +# Build related configuration options +#--------------------------------------------------------------------------- + +# If the EXTRACT_ALL tag is set to YES doxygen will assume all entities in +# documentation are documented, even if no documentation was available. Private +# class members and static file members will be hidden unless the +# EXTRACT_PRIVATE respectively EXTRACT_STATIC tags are set to YES. +# Note: This will also disable the warnings about undocumented members that are +# normally produced when WARNINGS is set to YES. +# The default value is: NO. + +EXTRACT_ALL = NO + +# If the EXTRACT_PRIVATE tag is set to YES all private members of a class will +# be included in the documentation. +# The default value is: NO. + +EXTRACT_PRIVATE = NO + +# If the EXTRACT_PACKAGE tag is set to YES all members with package or internal +# scope will be included in the documentation. +# The default value is: NO. + +EXTRACT_PACKAGE = NO + +# If the EXTRACT_STATIC tag is set to YES all static members of a file will be +# included in the documentation. +# The default value is: NO. + +EXTRACT_STATIC = NO + +# If the EXTRACT_LOCAL_CLASSES tag is set to YES classes (and structs) defined +# locally in source files will be included in the documentation. If set to NO +# only classes defined in header files are included. Does not have any effect +# for Java sources. +# The default value is: YES. + +EXTRACT_LOCAL_CLASSES = YES + +# This flag is only useful for Objective-C code. When set to YES local methods, +# which are defined in the implementation section but not in the interface are +# included in the documentation. If set to NO only methods in the interface are +# included. +# The default value is: NO. + +EXTRACT_LOCAL_METHODS = NO + +# If this flag is set to YES, the members of anonymous namespaces will be +# extracted and appear in the documentation as a namespace called +# 'anonymous_namespace{file}', where file will be replaced with the base name of +# the file that contains the anonymous namespace. By default anonymous namespace +# are hidden. +# The default value is: NO. + +EXTRACT_ANON_NSPACES = NO + +# If the HIDE_UNDOC_MEMBERS tag is set to YES, doxygen will hide all +# undocumented members inside documented classes or files. If set to NO these +# members will be included in the various overviews, but no documentation +# section is generated. This option has no effect if EXTRACT_ALL is enabled. +# The default value is: NO. + +HIDE_UNDOC_MEMBERS = NO + +# If the HIDE_UNDOC_CLASSES tag is set to YES, doxygen will hide all +# undocumented classes that are normally visible in the class hierarchy. If set +# to NO these classes will be included in the various overviews. This option has +# no effect if EXTRACT_ALL is enabled. +# The default value is: NO. + +HIDE_UNDOC_CLASSES = NO + +# If the HIDE_FRIEND_COMPOUNDS tag is set to YES, doxygen will hide all friend +# (class|struct|union) declarations. If set to NO these declarations will be +# included in the documentation. +# The default value is: NO. + +HIDE_FRIEND_COMPOUNDS = NO + +# If the HIDE_IN_BODY_DOCS tag is set to YES, doxygen will hide any +# documentation blocks found inside the body of a function. If set to NO these +# blocks will be appended to the function's detailed documentation block. +# The default value is: NO. + +HIDE_IN_BODY_DOCS = NO + +# The INTERNAL_DOCS tag determines if documentation that is typed after a +# \internal command is included. If the tag is set to NO then the documentation +# will be excluded. Set it to YES to include the internal documentation. +# The default value is: NO. + +INTERNAL_DOCS = NO + +# If the CASE_SENSE_NAMES tag is set to NO then doxygen will only generate file +# names in lower-case letters. If set to YES upper-case letters are also +# allowed. This is useful if you have classes or files whose names only differ +# in case and if your file system supports case sensitive file names. Windows +# and Mac users are advised to set this option to NO. +# The default value is: system dependent. + +CASE_SENSE_NAMES = NO + +# If the HIDE_SCOPE_NAMES tag is set to NO then doxygen will show members with +# their full class and namespace scopes in the documentation. If set to YES the +# scope will be hidden. +# The default value is: NO. + +HIDE_SCOPE_NAMES = NO + +# If the SHOW_INCLUDE_FILES tag is set to YES then doxygen will put a list of +# the files that are included by a file in the documentation of that file. +# The default value is: YES. + +SHOW_INCLUDE_FILES = YES + +# If the SHOW_GROUPED_MEMB_INC tag is set to YES then Doxygen will add for each +# grouped member an include statement to the documentation, telling the reader +# which file to include in order to use the member. +# The default value is: NO. + +SHOW_GROUPED_MEMB_INC = NO + +# If the FORCE_LOCAL_INCLUDES tag is set to YES then doxygen will list include +# files with double quotes in the documentation rather than with sharp brackets. +# The default value is: NO. + +FORCE_LOCAL_INCLUDES = NO + +# If the INLINE_INFO tag is set to YES then a tag [inline] is inserted in the +# documentation for inline members. +# The default value is: YES. + +INLINE_INFO = YES + +# If the SORT_MEMBER_DOCS tag is set to YES then doxygen will sort the +# (detailed) documentation of file and class members alphabetically by member +# name. If set to NO the members will appear in declaration order. +# The default value is: YES. + +SORT_MEMBER_DOCS = YES + +# If the SORT_BRIEF_DOCS tag is set to YES then doxygen will sort the brief +# descriptions of file, namespace and class members alphabetically by member +# name. If set to NO the members will appear in declaration order. Note that +# this will also influence the order of the classes in the class list. +# The default value is: NO. + +SORT_BRIEF_DOCS = NO + +# If the SORT_MEMBERS_CTORS_1ST tag is set to YES then doxygen will sort the +# (brief and detailed) documentation of class members so that constructors and +# destructors are listed first. If set to NO the constructors will appear in the +# respective orders defined by SORT_BRIEF_DOCS and SORT_MEMBER_DOCS. +# Note: If SORT_BRIEF_DOCS is set to NO this option is ignored for sorting brief +# member documentation. +# Note: If SORT_MEMBER_DOCS is set to NO this option is ignored for sorting +# detailed member documentation. +# The default value is: NO. + +SORT_MEMBERS_CTORS_1ST = NO + +# If the SORT_GROUP_NAMES tag is set to YES then doxygen will sort the hierarchy +# of group names into alphabetical order. If set to NO the group names will +# appear in their defined order. +# The default value is: NO. + +SORT_GROUP_NAMES = NO + +# If the SORT_BY_SCOPE_NAME tag is set to YES, the class list will be sorted by +# fully-qualified names, including namespaces. If set to NO, the class list will +# be sorted only by class name, not including the namespace part. +# Note: This option is not very useful if HIDE_SCOPE_NAMES is set to YES. +# Note: This option applies only to the class list, not to the alphabetical +# list. +# The default value is: NO. + +SORT_BY_SCOPE_NAME = NO + +# If the STRICT_PROTO_MATCHING option is enabled and doxygen fails to do proper +# type resolution of all parameters of a function it will reject a match between +# the prototype and the implementation of a member function even if there is +# only one candidate or it is obvious which candidate to choose by doing a +# simple string match. By disabling STRICT_PROTO_MATCHING doxygen will still +# accept a match between prototype and implementation in such cases. +# The default value is: NO. + +STRICT_PROTO_MATCHING = NO + +# The GENERATE_TODOLIST tag can be used to enable ( YES) or disable ( NO) the +# todo list. This list is created by putting \todo commands in the +# documentation. +# The default value is: YES. + +GENERATE_TODOLIST = YES + +# The GENERATE_TESTLIST tag can be used to enable ( YES) or disable ( NO) the +# test list. This list is created by putting \test commands in the +# documentation. +# The default value is: YES. + +GENERATE_TESTLIST = YES + +# The GENERATE_BUGLIST tag can be used to enable ( YES) or disable ( NO) the bug +# list. This list is created by putting \bug commands in the documentation. +# The default value is: YES. + +GENERATE_BUGLIST = YES + +# The GENERATE_DEPRECATEDLIST tag can be used to enable ( YES) or disable ( NO) +# the deprecated list. This list is created by putting \deprecated commands in +# the documentation. +# The default value is: YES. + +GENERATE_DEPRECATEDLIST= YES + +# The ENABLED_SECTIONS tag can be used to enable conditional documentation +# sections, marked by \if ... \endif and \cond +# ... \endcond blocks. + +ENABLED_SECTIONS = + +# The MAX_INITIALIZER_LINES tag determines the maximum number of lines that the +# initial value of a variable or macro / define can have for it to appear in the +# documentation. If the initializer consists of more lines than specified here +# it will be hidden. Use a value of 0 to hide initializers completely. The +# appearance of the value of individual variables and macros / defines can be +# controlled using \showinitializer or \hideinitializer command in the +# documentation regardless of this setting. +# Minimum value: 0, maximum value: 10000, default value: 30. + +MAX_INITIALIZER_LINES = 30 + +# Set the SHOW_USED_FILES tag to NO to disable the list of files generated at +# the bottom of the documentation of classes and structs. If set to YES the list +# will mention the files that were used to generate the documentation. +# The default value is: YES. + +SHOW_USED_FILES = YES + +# Set the SHOW_FILES tag to NO to disable the generation of the Files page. This +# will remove the Files entry from the Quick Index and from the Folder Tree View +# (if specified). +# The default value is: YES. + +SHOW_FILES = YES + +# Set the SHOW_NAMESPACES tag to NO to disable the generation of the Namespaces +# page. This will remove the Namespaces entry from the Quick Index and from the +# Folder Tree View (if specified). +# The default value is: YES. + +SHOW_NAMESPACES = YES + +# The FILE_VERSION_FILTER tag can be used to specify a program or script that +# doxygen should invoke to get the current version for each file (typically from +# the version control system). Doxygen will invoke the program by executing (via +# popen()) the command command input-file, where command is the value of the +# FILE_VERSION_FILTER tag, and input-file is the name of an input file provided +# by doxygen. Whatever the program writes to standard output is used as the file +# version. For an example see the documentation. + +FILE_VERSION_FILTER = + +# The LAYOUT_FILE tag can be used to specify a layout file which will be parsed +# by doxygen. The layout file controls the global structure of the generated +# output files in an output format independent way. To create the layout file +# that represents doxygen's defaults, run doxygen with the -l option. You can +# optionally specify a file name after the option, if omitted DoxygenLayout.xml +# will be used as the name of the layout file. +# +# Note that if you run doxygen from a directory containing a file called +# DoxygenLayout.xml, doxygen will parse it automatically even if the LAYOUT_FILE +# tag is left empty. + +LAYOUT_FILE = "@CMAKE_CURRENT_BINARY_DIR@/docs/DoxygenLayout.xml" + +# The CITE_BIB_FILES tag can be used to specify one or more bib files containing +# the reference definitions. This must be a list of .bib files. The .bib +# extension is automatically appended if omitted. This requires the bibtex tool +# to be installed. See also http://en.wikipedia.org/wiki/BibTeX for more info. +# For LaTeX the style of the bibliography can be controlled using +# LATEX_BIB_STYLE. To use this feature you need bibtex and perl available in the +# search path. Do not use file names with spaces, bibtex cannot handle them. See +# also \cite for info how to create references. + +CITE_BIB_FILES = + +#--------------------------------------------------------------------------- +# Configuration options related to warning and progress messages +#--------------------------------------------------------------------------- + +# The QUIET tag can be used to turn on/off the messages that are generated to +# standard output by doxygen. If QUIET is set to YES this implies that the +# messages are off. +# The default value is: NO. + +QUIET = NO + +# The WARNINGS tag can be used to turn on/off the warning messages that are +# generated to standard error ( stderr) by doxygen. If WARNINGS is set to YES +# this implies that the warnings are on. +# +# Tip: Turn warnings on while writing the documentation. +# The default value is: YES. + +WARNINGS = YES + +# If the WARN_IF_UNDOCUMENTED tag is set to YES, then doxygen will generate +# warnings for undocumented members. If EXTRACT_ALL is set to YES then this flag +# will automatically be disabled. +# The default value is: YES. + +WARN_IF_UNDOCUMENTED = YES + +# If the WARN_IF_DOC_ERROR tag is set to YES, doxygen will generate warnings for +# potential errors in the documentation, such as not documenting some parameters +# in a documented function, or documenting parameters that don't exist or using +# markup commands wrongly. +# The default value is: YES. + +WARN_IF_DOC_ERROR = YES + +# This WARN_NO_PARAMDOC option can be enabled to get warnings for functions that +# are documented, but have no documentation for their parameters or return +# value. If set to NO doxygen will only warn about wrong or incomplete parameter +# documentation, but not about the absence of documentation. +# The default value is: NO. + +WARN_NO_PARAMDOC = NO + +# The WARN_FORMAT tag determines the format of the warning messages that doxygen +# can produce. The string should contain the $file, $line, and $text tags, which +# will be replaced by the file and line number from which the warning originated +# and the warning text. Optionally the format may contain $version, which will +# be replaced by the version of the file (if it could be obtained via +# FILE_VERSION_FILTER) +# The default value is: $file:$line: $text. + +WARN_FORMAT = "$file:$line: $text" + +# The WARN_LOGFILE tag can be used to specify a file to which warning and error +# messages should be written. If left blank the output is written to standard +# error (stderr). + +WARN_LOGFILE = + +#--------------------------------------------------------------------------- +# Configuration options related to the input files +#--------------------------------------------------------------------------- + +# The INPUT tag is used to specify the files and/or directories that contain +# documented source files. You may enter file names like myfile.cpp or +# directories like /usr/src/myproject. Separate the files or directories with +# spaces. +# Note: If this tag is empty the current directory is searched. + +INPUT = "@CMAKE_CURRENT_SOURCE_DIR@/src" \ + "@CMAKE_CURRENT_SOURCE_DIR@/include" + +# This tag can be used to specify the character encoding of the source files +# that doxygen parses. Internally doxygen uses the UTF-8 encoding. Doxygen uses +# libiconv (or the iconv built into libc) for the transcoding. See the libiconv +# documentation (see: http://www.gnu.org/software/libiconv) for the list of +# possible encodings. +# The default value is: UTF-8. + +INPUT_ENCODING = UTF-8 + +# If the value of the INPUT tag contains directories, you can use the +# FILE_PATTERNS tag to specify one or more wildcard patterns (like *.cpp and +# *.h) to filter out the source-files in the directories. If left blank the +# following patterns are tested:*.c, *.cc, *.cxx, *.cpp, *.c++, *.java, *.ii, +# *.ixx, *.ipp, *.i++, *.inl, *.idl, *.ddl, *.odl, *.h, *.hh, *.hxx, *.hpp, +# *.h++, *.cs, *.d, *.php, *.php4, *.php5, *.phtml, *.inc, *.m, *.markdown, +# *.md, *.mm, *.dox, *.py, *.f90, *.f, *.for, *.tcl, *.vhd, *.vhdl, *.ucf, +# *.qsf, *.as and *.js. + +FILE_PATTERNS = + +# The RECURSIVE tag can be used to specify whether or not subdirectories should +# be searched for input files as well. +# The default value is: NO. + +RECURSIVE = YES + +# The EXCLUDE tag can be used to specify files and/or directories that should be +# excluded from the INPUT source files. This way you can easily exclude a +# subdirectory from a directory tree whose root is specified with the INPUT tag. +# +# Note that relative paths are relative to the directory from which doxygen is +# run. + +EXCLUDE = + +# The EXCLUDE_SYMLINKS tag can be used to select whether or not files or +# directories that are symbolic links (a Unix file system feature) are excluded +# from the input. +# The default value is: NO. + +EXCLUDE_SYMLINKS = NO + +# If the value of the INPUT tag contains directories, you can use the +# EXCLUDE_PATTERNS tag to specify one or more wildcard patterns to exclude +# certain files from those directories. +# +# Note that the wildcards are matched against the file with absolute path, so to +# exclude all test directories for example use the pattern */test/* + +EXCLUDE_PATTERNS = + +# The EXCLUDE_SYMBOLS tag can be used to specify one or more symbol names +# (namespaces, classes, functions, etc.) that should be excluded from the +# output. The symbol name can be a fully qualified name, a word, or if the +# wildcard * is used, a substring. Examples: ANamespace, AClass, +# AClass::ANamespace, ANamespace::*Test +# +# Note that the wildcards are matched against the file with absolute path, so to +# exclude all test directories use the pattern */test/* + +EXCLUDE_SYMBOLS = + +# The EXAMPLE_PATH tag can be used to specify one or more files or directories +# that contain example code fragments that are included (see the \include +# command). + +EXAMPLE_PATH = + +# If the value of the EXAMPLE_PATH tag contains directories, you can use the +# EXAMPLE_PATTERNS tag to specify one or more wildcard pattern (like *.cpp and +# *.h) to filter out the source-files in the directories. If left blank all +# files are included. + +EXAMPLE_PATTERNS = + +# If the EXAMPLE_RECURSIVE tag is set to YES then subdirectories will be +# searched for input files to be used with the \include or \dontinclude commands +# irrespective of the value of the RECURSIVE tag. +# The default value is: NO. + +EXAMPLE_RECURSIVE = NO + +# The IMAGE_PATH tag can be used to specify one or more files or directories +# that contain images that are to be included in the documentation (see the +# \image command). + +IMAGE_PATH = + +# The INPUT_FILTER tag can be used to specify a program that doxygen should +# invoke to filter for each input file. Doxygen will invoke the filter program +# by executing (via popen()) the command: +# +# +# +# where is the value of the INPUT_FILTER tag, and is the +# name of an input file. Doxygen will then use the output that the filter +# program writes to standard output. If FILTER_PATTERNS is specified, this tag +# will be ignored. +# +# Note that the filter must not add or remove lines; it is applied before the +# code is scanned, but not when the output code is generated. If lines are added +# or removed, the anchors will not be placed correctly. + +INPUT_FILTER = + +# The FILTER_PATTERNS tag can be used to specify filters on a per file pattern +# basis. Doxygen will compare the file name with each pattern and apply the +# filter if there is a match. The filters are a list of the form: pattern=filter +# (like *.cpp=my_cpp_filter). See INPUT_FILTER for further information on how +# filters are used. If the FILTER_PATTERNS tag is empty or if none of the +# patterns match the file name, INPUT_FILTER is applied. + +FILTER_PATTERNS = + +# If the FILTER_SOURCE_FILES tag is set to YES, the input filter (if set using +# INPUT_FILTER ) will also be used to filter the input files that are used for +# producing the source files to browse (i.e. when SOURCE_BROWSER is set to YES). +# The default value is: NO. + +FILTER_SOURCE_FILES = NO + +# The FILTER_SOURCE_PATTERNS tag can be used to specify source filters per file +# pattern. A pattern will override the setting for FILTER_PATTERN (if any) and +# it is also possible to disable source filtering for a specific pattern using +# *.ext= (so without naming a filter). +# This tag requires that the tag FILTER_SOURCE_FILES is set to YES. + +FILTER_SOURCE_PATTERNS = + +# If the USE_MDFILE_AS_MAINPAGE tag refers to the name of a markdown file that +# is part of the input, its contents will be placed on the main page +# (index.html). This can be useful if you have a project on for instance GitHub +# and want to reuse the introduction page also for the doxygen output. + +USE_MDFILE_AS_MAINPAGE = + +#--------------------------------------------------------------------------- +# Configuration options related to source browsing +#--------------------------------------------------------------------------- + +# If the SOURCE_BROWSER tag is set to YES then a list of source files will be +# generated. Documented entities will be cross-referenced with these sources. +# +# Note: To get rid of all source code in the generated output, make sure that +# also VERBATIM_HEADERS is set to NO. +# The default value is: NO. + +SOURCE_BROWSER = NO + +# Setting the INLINE_SOURCES tag to YES will include the body of functions, +# classes and enums directly into the documentation. +# The default value is: NO. + +INLINE_SOURCES = NO + +# Setting the STRIP_CODE_COMMENTS tag to YES will instruct doxygen to hide any +# special comment blocks from generated source code fragments. Normal C, C++ and +# Fortran comments will always remain visible. +# The default value is: YES. + +STRIP_CODE_COMMENTS = YES + +# If the REFERENCED_BY_RELATION tag is set to YES then for each documented +# function all documented functions referencing it will be listed. +# The default value is: NO. + +REFERENCED_BY_RELATION = NO + +# If the REFERENCES_RELATION tag is set to YES then for each documented function +# all documented entities called/used by that function will be listed. +# The default value is: NO. + +REFERENCES_RELATION = NO + +# If the REFERENCES_LINK_SOURCE tag is set to YES and SOURCE_BROWSER tag is set +# to YES, then the hyperlinks from functions in REFERENCES_RELATION and +# REFERENCED_BY_RELATION lists will link to the source code. Otherwise they will +# link to the documentation. +# The default value is: YES. + +REFERENCES_LINK_SOURCE = YES + +# If SOURCE_TOOLTIPS is enabled (the default) then hovering a hyperlink in the +# source code will show a tooltip with additional information such as prototype, +# brief description and links to the definition and documentation. Since this +# will make the HTML file larger and loading of large files a bit slower, you +# can opt to disable this feature. +# The default value is: YES. +# This tag requires that the tag SOURCE_BROWSER is set to YES. + +SOURCE_TOOLTIPS = YES + +# If the USE_HTAGS tag is set to YES then the references to source code will +# point to the HTML generated by the htags(1) tool instead of doxygen built-in +# source browser. The htags tool is part of GNU's global source tagging system +# (see http://www.gnu.org/software/global/global.html). You will need version +# 4.8.6 or higher. +# +# To use it do the following: +# - Install the latest version of global +# - Enable SOURCE_BROWSER and USE_HTAGS in the config file +# - Make sure the INPUT points to the root of the source tree +# - Run doxygen as normal +# +# Doxygen will invoke htags (and that will in turn invoke gtags), so these +# tools must be available from the command line (i.e. in the search path). +# +# The result: instead of the source browser generated by doxygen, the links to +# source code will now point to the output of htags. +# The default value is: NO. +# This tag requires that the tag SOURCE_BROWSER is set to YES. + +USE_HTAGS = NO + +# If the VERBATIM_HEADERS tag is set the YES then doxygen will generate a +# verbatim copy of the header file for each class for which an include is +# specified. Set to NO to disable this. +# See also: Section \class. +# The default value is: YES. + +VERBATIM_HEADERS = YES + +#--------------------------------------------------------------------------- +# Configuration options related to the alphabetical class index +#--------------------------------------------------------------------------- + +# If the ALPHABETICAL_INDEX tag is set to YES, an alphabetical index of all +# compounds will be generated. Enable this if the project contains a lot of +# classes, structs, unions or interfaces. +# The default value is: YES. + +ALPHABETICAL_INDEX = YES + +# The COLS_IN_ALPHA_INDEX tag can be used to specify the number of columns in +# which the alphabetical index list will be split. +# Minimum value: 1, maximum value: 20, default value: 5. +# This tag requires that the tag ALPHABETICAL_INDEX is set to YES. + +COLS_IN_ALPHA_INDEX = 5 + +# In case all classes in a project start with a common prefix, all classes will +# be put under the same header in the alphabetical index. The IGNORE_PREFIX tag +# can be used to specify a prefix (or a list of prefixes) that should be ignored +# while generating the index headers. +# This tag requires that the tag ALPHABETICAL_INDEX is set to YES. + +IGNORE_PREFIX = + +#--------------------------------------------------------------------------- +# Configuration options related to the HTML output +#--------------------------------------------------------------------------- + +# If the GENERATE_HTML tag is set to YES doxygen will generate HTML output +# The default value is: YES. + +GENERATE_HTML = YES + +# The HTML_OUTPUT tag is used to specify where the HTML docs will be put. If a +# relative path is entered the value of OUTPUT_DIRECTORY will be put in front of +# it. +# The default directory is: html. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_OUTPUT = html + +# The HTML_FILE_EXTENSION tag can be used to specify the file extension for each +# generated HTML page (for example: .htm, .php, .asp). +# The default value is: .html. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_FILE_EXTENSION = .html + +# The HTML_HEADER tag can be used to specify a user-defined HTML header file for +# each generated HTML page. If the tag is left blank doxygen will generate a +# standard header. +# +# To get valid HTML the header file that includes any scripts and style sheets +# that doxygen needs, which is dependent on the configuration options used (e.g. +# the setting GENERATE_TREEVIEW). It is highly recommended to start with a +# default header using +# doxygen -w html new_header.html new_footer.html new_stylesheet.css +# YourConfigFile +# and then modify the file new_header.html. See also section "Doxygen usage" +# for information on how to generate the default header that doxygen normally +# uses. +# Note: The header is subject to change so you typically have to regenerate the +# default header when upgrading to a newer version of doxygen. For a description +# of the possible markers and block names see the documentation. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_HEADER = + +# The HTML_FOOTER tag can be used to specify a user-defined HTML footer for each +# generated HTML page. If the tag is left blank doxygen will generate a standard +# footer. See HTML_HEADER for more information on how to generate a default +# footer and what special commands can be used inside the footer. See also +# section "Doxygen usage" for information on how to generate the default footer +# that doxygen normally uses. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_FOOTER = + +# The HTML_STYLESHEET tag can be used to specify a user-defined cascading style +# sheet that is used by each HTML page. It can be used to fine-tune the look of +# the HTML output. If left blank doxygen will generate a default style sheet. +# See also section "Doxygen usage" for information on how to generate the style +# sheet that doxygen normally uses. +# Note: It is recommended to use HTML_EXTRA_STYLESHEET instead of this tag, as +# it is more robust and this tag (HTML_STYLESHEET) will in the future become +# obsolete. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_STYLESHEET = + +# The HTML_EXTRA_STYLESHEET tag can be used to specify an additional user- +# defined cascading style sheet that is included after the standard style sheets +# created by doxygen. Using this option one can overrule certain style aspects. +# This is preferred over using HTML_STYLESHEET since it does not replace the +# standard style sheet and is therefor more robust against future updates. +# Doxygen will copy the style sheet file to the output directory. For an example +# see the documentation. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_EXTRA_STYLESHEET = "@CMAKE_CURRENT_BINARY_DIR@/docs/customdoxygen.css" + +# The HTML_EXTRA_FILES tag can be used to specify one or more extra images or +# other source files which should be copied to the HTML output directory. Note +# that these files will be copied to the base HTML output directory. Use the +# $relpath^ marker in the HTML_HEADER and/or HTML_FOOTER files to load these +# files. In the HTML_STYLESHEET file, use the file name only. Also note that the +# files will be copied as-is; there are no commands or markers available. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_EXTRA_FILES = + +# The HTML_COLORSTYLE_HUE tag controls the color of the HTML output. Doxygen +# will adjust the colors in the stylesheet and background images according to +# this color. Hue is specified as an angle on a colorwheel, see +# http://en.wikipedia.org/wiki/Hue for more information. For instance the value +# 0 represents red, 60 is yellow, 120 is green, 180 is cyan, 240 is blue, 300 +# purple, and 360 is red again. +# Minimum value: 0, maximum value: 359, default value: 220. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_COLORSTYLE_HUE = 220 + +# The HTML_COLORSTYLE_SAT tag controls the purity (or saturation) of the colors +# in the HTML output. For a value of 0 the output will use grayscales only. A +# value of 255 will produce the most vivid colors. +# Minimum value: 0, maximum value: 255, default value: 100. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_COLORSTYLE_SAT = 100 + +# The HTML_COLORSTYLE_GAMMA tag controls the gamma correction applied to the +# luminance component of the colors in the HTML output. Values below 100 +# gradually make the output lighter, whereas values above 100 make the output +# darker. The value divided by 100 is the actual gamma applied, so 80 represents +# a gamma of 0.8, The value 220 represents a gamma of 2.2, and 100 does not +# change the gamma. +# Minimum value: 40, maximum value: 240, default value: 80. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_COLORSTYLE_GAMMA = 80 + +# If the HTML_TIMESTAMP tag is set to YES then the footer of each generated HTML +# page will contain the date and time when the page was generated. Setting this +# to NO can help when comparing the output of multiple runs. +# The default value is: YES. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_TIMESTAMP = YES + +# If the HTML_DYNAMIC_SECTIONS tag is set to YES then the generated HTML +# documentation will contain sections that can be hidden and shown after the +# page has loaded. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_DYNAMIC_SECTIONS = NO + +# With HTML_INDEX_NUM_ENTRIES one can control the preferred number of entries +# shown in the various tree structured indices initially; the user can expand +# and collapse entries dynamically later on. Doxygen will expand the tree to +# such a level that at most the specified number of entries are visible (unless +# a fully collapsed tree already exceeds this amount). So setting the number of +# entries 1 will produce a full collapsed tree by default. 0 is a special value +# representing an infinite number of entries and will result in a full expanded +# tree by default. +# Minimum value: 0, maximum value: 9999, default value: 100. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_INDEX_NUM_ENTRIES = 100 + +# If the GENERATE_DOCSET tag is set to YES, additional index files will be +# generated that can be used as input for Apple's Xcode 3 integrated development +# environment (see: http://developer.apple.com/tools/xcode/), introduced with +# OSX 10.5 (Leopard). To create a documentation set, doxygen will generate a +# Makefile in the HTML output directory. Running make will produce the docset in +# that directory and running make install will install the docset in +# ~/Library/Developer/Shared/Documentation/DocSets so that Xcode will find it at +# startup. See http://developer.apple.com/tools/creatingdocsetswithdoxygen.html +# for more information. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +GENERATE_DOCSET = NO + +# This tag determines the name of the docset feed. A documentation feed provides +# an umbrella under which multiple documentation sets from a single provider +# (such as a company or product suite) can be grouped. +# The default value is: Doxygen generated docs. +# This tag requires that the tag GENERATE_DOCSET is set to YES. + +DOCSET_FEEDNAME = "Doxygen generated docs" + +# This tag specifies a string that should uniquely identify the documentation +# set bundle. This should be a reverse domain-name style string, e.g. +# com.mycompany.MyDocSet. Doxygen will append .docset to the name. +# The default value is: org.doxygen.Project. +# This tag requires that the tag GENERATE_DOCSET is set to YES. + +DOCSET_BUNDLE_ID = org.doxygen.Project + +# The DOCSET_PUBLISHER_ID tag specifies a string that should uniquely identify +# the documentation publisher. This should be a reverse domain-name style +# string, e.g. com.mycompany.MyDocSet.documentation. +# The default value is: org.doxygen.Publisher. +# This tag requires that the tag GENERATE_DOCSET is set to YES. + +DOCSET_PUBLISHER_ID = org.doxygen.Publisher + +# The DOCSET_PUBLISHER_NAME tag identifies the documentation publisher. +# The default value is: Publisher. +# This tag requires that the tag GENERATE_DOCSET is set to YES. + +DOCSET_PUBLISHER_NAME = Publisher + +# If the GENERATE_HTMLHELP tag is set to YES then doxygen generates three +# additional HTML index files: index.hhp, index.hhc, and index.hhk. The +# index.hhp is a project file that can be read by Microsoft's HTML Help Workshop +# (see: http://www.microsoft.com/en-us/download/details.aspx?id=21138) on +# Windows. +# +# The HTML Help Workshop contains a compiler that can convert all HTML output +# generated by doxygen into a single compiled HTML file (.chm). Compiled HTML +# files are now used as the Windows 98 help format, and will replace the old +# Windows help format (.hlp) on all Windows platforms in the future. Compressed +# HTML files also contain an index, a table of contents, and you can search for +# words in the documentation. The HTML workshop also contains a viewer for +# compressed HTML files. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +GENERATE_HTMLHELP = NO + +# The CHM_FILE tag can be used to specify the file name of the resulting .chm +# file. You can add a path in front of the file if the result should not be +# written to the html output directory. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. + +CHM_FILE = + +# The HHC_LOCATION tag can be used to specify the location (absolute path +# including file name) of the HTML help compiler ( hhc.exe). If non-empty +# doxygen will try to run the HTML help compiler on the generated index.hhp. +# The file has to be specified with full path. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. + +HHC_LOCATION = + +# The GENERATE_CHI flag controls if a separate .chi index file is generated ( +# YES) or that it should be included in the master .chm file ( NO). +# The default value is: NO. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. + +GENERATE_CHI = NO + +# The CHM_INDEX_ENCODING is used to encode HtmlHelp index ( hhk), content ( hhc) +# and project file content. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. + +CHM_INDEX_ENCODING = + +# The BINARY_TOC flag controls whether a binary table of contents is generated ( +# YES) or a normal table of contents ( NO) in the .chm file. Furthermore it +# enables the Previous and Next buttons. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. + +BINARY_TOC = NO + +# The TOC_EXPAND flag can be set to YES to add extra items for group members to +# the table of contents of the HTML help documentation and to the tree view. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. + +TOC_EXPAND = NO + +# If the GENERATE_QHP tag is set to YES and both QHP_NAMESPACE and +# QHP_VIRTUAL_FOLDER are set, an additional index file will be generated that +# can be used as input for Qt's qhelpgenerator to generate a Qt Compressed Help +# (.qch) of the generated HTML documentation. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +GENERATE_QHP = NO + +# If the QHG_LOCATION tag is specified, the QCH_FILE tag can be used to specify +# the file name of the resulting .qch file. The path specified is relative to +# the HTML output folder. +# This tag requires that the tag GENERATE_QHP is set to YES. + +QCH_FILE = + +# The QHP_NAMESPACE tag specifies the namespace to use when generating Qt Help +# Project output. For more information please see Qt Help Project / Namespace +# (see: http://qt-project.org/doc/qt-4.8/qthelpproject.html#namespace). +# The default value is: org.doxygen.Project. +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHP_NAMESPACE = org.doxygen.Project + +# The QHP_VIRTUAL_FOLDER tag specifies the namespace to use when generating Qt +# Help Project output. For more information please see Qt Help Project / Virtual +# Folders (see: http://qt-project.org/doc/qt-4.8/qthelpproject.html#virtual- +# folders). +# The default value is: doc. +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHP_VIRTUAL_FOLDER = doc + +# If the QHP_CUST_FILTER_NAME tag is set, it specifies the name of a custom +# filter to add. For more information please see Qt Help Project / Custom +# Filters (see: http://qt-project.org/doc/qt-4.8/qthelpproject.html#custom- +# filters). +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHP_CUST_FILTER_NAME = + +# The QHP_CUST_FILTER_ATTRS tag specifies the list of the attributes of the +# custom filter to add. For more information please see Qt Help Project / Custom +# Filters (see: http://qt-project.org/doc/qt-4.8/qthelpproject.html#custom- +# filters). +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHP_CUST_FILTER_ATTRS = + +# The QHP_SECT_FILTER_ATTRS tag specifies the list of the attributes this +# project's filter section matches. Qt Help Project / Filter Attributes (see: +# http://qt-project.org/doc/qt-4.8/qthelpproject.html#filter-attributes). +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHP_SECT_FILTER_ATTRS = + +# The QHG_LOCATION tag can be used to specify the location of Qt's +# qhelpgenerator. If non-empty doxygen will try to run qhelpgenerator on the +# generated .qhp file. +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHG_LOCATION = + +# If the GENERATE_ECLIPSEHELP tag is set to YES, additional index files will be +# generated, together with the HTML files, they form an Eclipse help plugin. To +# install this plugin and make it available under the help contents menu in +# Eclipse, the contents of the directory containing the HTML and XML files needs +# to be copied into the plugins directory of eclipse. The name of the directory +# within the plugins directory should be the same as the ECLIPSE_DOC_ID value. +# After copying Eclipse needs to be restarted before the help appears. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +GENERATE_ECLIPSEHELP = NO + +# A unique identifier for the Eclipse help plugin. When installing the plugin +# the directory name containing the HTML and XML files should also have this +# name. Each documentation set should have its own identifier. +# The default value is: org.doxygen.Project. +# This tag requires that the tag GENERATE_ECLIPSEHELP is set to YES. + +ECLIPSE_DOC_ID = org.doxygen.Project + +# If you want full control over the layout of the generated HTML pages it might +# be necessary to disable the index and replace it with your own. The +# DISABLE_INDEX tag can be used to turn on/off the condensed index (tabs) at top +# of each HTML page. A value of NO enables the index and the value YES disables +# it. Since the tabs in the index contain the same information as the navigation +# tree, you can set this option to YES if you also set GENERATE_TREEVIEW to YES. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +DISABLE_INDEX = NO + +# The GENERATE_TREEVIEW tag is used to specify whether a tree-like index +# structure should be generated to display hierarchical information. If the tag +# value is set to YES, a side panel will be generated containing a tree-like +# index structure (just like the one that is generated for HTML Help). For this +# to work a browser that supports JavaScript, DHTML, CSS and frames is required +# (i.e. any modern browser). Windows users are probably better off using the +# HTML help feature. Via custom stylesheets (see HTML_EXTRA_STYLESHEET) one can +# further fine-tune the look of the index. As an example, the default style +# sheet generated by doxygen has an example that shows how to put an image at +# the root of the tree instead of the PROJECT_NAME. Since the tree basically has +# the same information as the tab index, you could consider setting +# DISABLE_INDEX to YES when enabling this option. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +GENERATE_TREEVIEW = NO + +# The ENUM_VALUES_PER_LINE tag can be used to set the number of enum values that +# doxygen will group on one line in the generated HTML documentation. +# +# Note that a value of 0 will completely suppress the enum values from appearing +# in the overview section. +# Minimum value: 0, maximum value: 20, default value: 4. +# This tag requires that the tag GENERATE_HTML is set to YES. + +ENUM_VALUES_PER_LINE = 4 + +# If the treeview is enabled (see GENERATE_TREEVIEW) then this tag can be used +# to set the initial width (in pixels) of the frame in which the tree is shown. +# Minimum value: 0, maximum value: 1500, default value: 250. +# This tag requires that the tag GENERATE_HTML is set to YES. + +TREEVIEW_WIDTH = 250 + +# When the EXT_LINKS_IN_WINDOW option is set to YES doxygen will open links to +# external symbols imported via tag files in a separate window. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +EXT_LINKS_IN_WINDOW = NO + +# Use this tag to change the font size of LaTeX formulas included as images in +# the HTML documentation. When you change the font size after a successful +# doxygen run you need to manually remove any form_*.png images from the HTML +# output directory to force them to be regenerated. +# Minimum value: 8, maximum value: 50, default value: 10. +# This tag requires that the tag GENERATE_HTML is set to YES. + +FORMULA_FONTSIZE = 10 + +# Use the FORMULA_TRANPARENT tag to determine whether or not the images +# generated for formulas are transparent PNGs. Transparent PNGs are not +# supported properly for IE 6.0, but are supported on all modern browsers. +# +# Note that when changing this option you need to delete any form_*.png files in +# the HTML output directory before the changes have effect. +# The default value is: YES. +# This tag requires that the tag GENERATE_HTML is set to YES. + +FORMULA_TRANSPARENT = YES + +# Enable the USE_MATHJAX option to render LaTeX formulas using MathJax (see +# http://www.mathjax.org) which uses client side Javascript for the rendering +# instead of using prerendered bitmaps. Use this if you do not have LaTeX +# installed or if you want to formulas look prettier in the HTML output. When +# enabled you may also need to install MathJax separately and configure the path +# to it using the MATHJAX_RELPATH option. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +USE_MATHJAX = NO + +# When MathJax is enabled you can set the default output format to be used for +# the MathJax output. See the MathJax site (see: +# http://docs.mathjax.org/en/latest/output.html) for more details. +# Possible values are: HTML-CSS (which is slower, but has the best +# compatibility), NativeMML (i.e. MathML) and SVG. +# The default value is: HTML-CSS. +# This tag requires that the tag USE_MATHJAX is set to YES. + +MATHJAX_FORMAT = HTML-CSS + +# When MathJax is enabled you need to specify the location relative to the HTML +# output directory using the MATHJAX_RELPATH option. The destination directory +# should contain the MathJax.js script. For instance, if the mathjax directory +# is located at the same level as the HTML output directory, then +# MATHJAX_RELPATH should be ../mathjax. The default value points to the MathJax +# Content Delivery Network so you can quickly see the result without installing +# MathJax. However, it is strongly recommended to install a local copy of +# MathJax from http://www.mathjax.org before deployment. +# The default value is: http://cdn.mathjax.org/mathjax/latest. +# This tag requires that the tag USE_MATHJAX is set to YES. + +MATHJAX_RELPATH = http://cdn.mathjax.org/mathjax/latest + +# The MATHJAX_EXTENSIONS tag can be used to specify one or more MathJax +# extension names that should be enabled during MathJax rendering. For example +# MATHJAX_EXTENSIONS = TeX/AMSmath TeX/AMSsymbols +# This tag requires that the tag USE_MATHJAX is set to YES. + +MATHJAX_EXTENSIONS = + +# The MATHJAX_CODEFILE tag can be used to specify a file with javascript pieces +# of code that will be used on startup of the MathJax code. See the MathJax site +# (see: http://docs.mathjax.org/en/latest/output.html) for more details. For an +# example see the documentation. +# This tag requires that the tag USE_MATHJAX is set to YES. + +MATHJAX_CODEFILE = + +# When the SEARCHENGINE tag is enabled doxygen will generate a search box for +# the HTML output. The underlying search engine uses javascript and DHTML and +# should work on any modern browser. Note that when using HTML help +# (GENERATE_HTMLHELP), Qt help (GENERATE_QHP), or docsets (GENERATE_DOCSET) +# there is already a search function so this one should typically be disabled. +# For large projects the javascript based search engine can be slow, then +# enabling SERVER_BASED_SEARCH may provide a better solution. It is possible to +# search using the keyboard; to jump to the search box use + S +# (what the is depends on the OS and browser, but it is typically +# , /