diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore
index 8bc5e0b54ec5cfbcdd63e115855e21d315764ad2..5b0f4dc648d5958c0a12308cf867fdd1c53e1609 100644
--- a/src/plugins/e-acsl/.gitignore
+++ b/src/plugins/e-acsl/.gitignore
@@ -70,3 +70,6 @@ META.frama-c-e_acsl
Makefile.plugin.generated
E_ACSL.check_mli_exists
top/
+doc/doxygen/doxygen.cfg
+doc/doxygen/html
+doc/doxygen/warn.log
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 5fb3a337054828d22e0f41314548617a0ece2cab..b03cb56f0153a41874e8770f07eaf38e157b4dac 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -278,3 +278,16 @@ endif
$(E_ACSL_DIR)/Makefile: $(E_ACSL_DIR)/Makefile.in $(CONFIG_STATUS_DIR_DEP)
cd $(CONFIG_STATUS_DIR) && ./config.status
+
+#####################################
+# Doxygen #
+#####################################
+DOXYGEN = @DOXYGEN@
+doxygen:
+ if ! test $(DOXYGEN) = "no"; then \
+ $(DOXYGEN) doc/doxygen/doxygen.cfg ; \
+ else \
+ echo "Warning: Skip doxygen documentation: Doxygen executable not found."; \
+ fi
+
+doc:: doxygen
\ No newline at end of file
diff --git a/src/plugins/e-acsl/configure.ac b/src/plugins/e-acsl/configure.ac
index 7e158bf415c01661696a1364cf70dacbdce9faf2..504fb49bbd9e7440d6d0cb1e3a0abfd04181ce21 100644
--- a/src/plugins/e-acsl/configure.ac
+++ b/src/plugins/e-acsl/configure.ac
@@ -106,6 +106,12 @@ if test -z $HAVE_GMP; then
AC_MSG_WARN([GMP library missing: non-regression tests unavailable.])
fi
+# Doxygen
+#########
+AC_CHECK_PROG(DOXYGEN,doxygen,doxygen,no)
+AC_CHECK_PROG(HAVE_DOT,dot,YES,no)
+AC_OUTPUT([ doc/doxygen/doxygen.cfg ], [ ])
+
#######################
# Generating Makefile #
#######################
diff --git a/src/plugins/e-acsl/doc/doxygen/doxygen.cfg.in b/src/plugins/e-acsl/doc/doxygen/doxygen.cfg.in
new file mode 100644
index 0000000000000000000000000000000000000000..5d8a49c0b4e4c89582bfc092b04b6981d3bc8171
--- /dev/null
+++ b/src/plugins/e-acsl/doc/doxygen/doxygen.cfg.in
@@ -0,0 +1,1194 @@
+# Doxyfile 1.4.4
+
+# This file describes the settings to be used by the documentation system
+# doxygen (www.doxygen.org) for a project
+#
+# All text after a 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
+#---------------------------------------------------------------------------
+
+# The PROJECT_NAME tag is a single word (or a sequence of words surrounded
+# by quotes) that should identify the project.
+
+PROJECT_NAME = "E-ACSL Runtime Library"
+
+# 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 = 0.0.6
+
+# The OUTPUT_DIRECTORY tag is used to specify the (relative or absolute)
+# base path where the generated documentation will be put.
+# 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 = @abs_top_builddir@/doc/doxygen
+
+# 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 cause performance problems for the file system.
+
+CREATE_SUBDIRS = 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.
+# The default language is English, other supported languages are:
+# Brazilian, Catalan, Chinese, Chinese-Traditional, Croatian, Czech, Danish,
+# Dutch, Finnish, French, German, Greek, Hungarian, Italian, Japanese,
+# Japanese-en (Japanese with English messages), Korean, Korean-en, Norwegian,
+# Polish, Portuguese, Romanian, Russian, Serbian, Slovak, Slovene, Spanish,
+# Swedish, and Ukrainian.
+
+OUTPUT_LANGUAGE = English
+
+# If the BRIEF_MEMBER_DESC tag is set to YES (the default) 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.
+
+BRIEF_MEMBER_DESC = YES
+
+# If the REPEAT_BRIEF tag is set to YES (the default) 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.
+
+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" "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.
+
+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.
+
+INLINE_INHERITED_MEMB = NO
+
+# If the FULL_PATH_NAMES tag is set to YES then 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.
+
+FULL_PATH_NAMES = NO
+
+# If the FULL_PATH_NAMES tag is set to YES then 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.
+
+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 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.
+
+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
+# comments will behave just like the Qt-style comments (thus requiring an
+# explicit @brief command for a brief description.
+
+JAVADOC_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 behaviour.
+# 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 behaviour instead.
+
+MULTILINE_CPP_IS_BRIEF = NO
+
+# If the DETAILS_AT_TOP tag is set to YES then Doxygen
+# will output the detailed description near the top, like JavaDoc.
+# If set to NO, the detailed description appears after the member
+# documentation.
+
+INHERIT_DOCS = 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.
+
+DISTRIBUTE_GROUP_DOC = NO
+
+# 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.
+
+#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.
+
+TAB_SIZE = 4
+
+# This tag can be used to specify a number of aliases that acts
+# 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 =
+
+# 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.
+
+OPTIMIZE_OUTPUT_FOR_C = NO
+
+# Set the OPTIMIZE_OUTPUT_JAVA tag to YES if your project consists of Java sources
+# only. Doxygen will then generate output that is more tailored for Java.
+# For instance, namespaces will be presented as packages, qualified scopes
+# will look different, etc.
+
+OPTIMIZE_OUTPUT_JAVA = NO
+
+# Set the SUBGROUPING tag to YES (the default) 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.
+
+SUBGROUPING = YES
+
+#---------------------------------------------------------------------------
+# 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 and EXTRACT_STATIC tags are set to YES
+
+EXTRACT_ALL = YES
+
+# If the EXTRACT_PRIVATE tag is set to YES all private members of a class
+# will be included in the documentation.
+
+EXTRACT_PRIVATE = YES
+
+# If the EXTRACT_STATIC tag is set to YES all static members of a file
+# will be included in the documentation.
+
+EXTRACT_STATIC = YES
+
+# 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.
+
+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 (the default) only methods in the interface are included.
+
+EXTRACT_LOCAL_METHODS = NO
+
+# If the HIDE_UNDOC_MEMBERS tag is set to YES, Doxygen will hide all
+# undocumented members of documented classes, files or namespaces.
+# If set to NO (the default) 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.
+
+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 (the default) these classes will be included in the various
+# overviews. This option has no effect if EXTRACT_ALL is enabled.
+
+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 (the default) these declarations will be included in the
+# documentation.
+
+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 (the default) these blocks will be appended to the
+# function's detailed documentation block.
+
+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 (the default) then the documentation will be excluded.
+# Set it to YES to include the internal documentation.
+
+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.
+
+CASE_SENSE_NAMES = YES
+
+# If the HIDE_SCOPE_NAMES tag is set to NO (the default) then Doxygen
+# will show members with their full class and namespace scopes in the
+# documentation. If set to YES the scope will be hidden.
+
+HIDE_SCOPE_NAMES = NO
+
+# If the SHOW_INCLUDE_FILES tag is set to YES (the default) then Doxygen
+# will put a list of the files that are included by a file in the documentation
+# of that file.
+
+SHOW_INCLUDE_FILES = YES
+
+# If the INLINE_INFO tag is set to YES (the default) then a tag [inline]
+# is inserted in the documentation for inline members.
+
+INLINE_INFO = YES
+
+# If the SORT_MEMBER_DOCS tag is set to YES (the default) 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.
+
+SORT_MEMBER_DOCS = YES
+
+# If the SORT_BRIEF_DOCS tag is set to YES then doxygen will sort the
+# brief documentation of file, namespace and class members alphabetically
+# by member name. If set to NO (the default) the members will appear in
+# declaration order.
+
+SORT_BRIEF_DOCS = 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 default), 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.
+
+SORT_BY_SCOPE_NAME = 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.
+
+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.
+
+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.
+
+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.
+
+GENERATE_DEPRECATEDLIST= YES
+
+# The ENABLED_SECTIONS tag can be used to enable conditional
+# documentation sections, marked by \if sectionname ... \endif.
+
+ENABLED_SECTIONS =
+
+# The MAX_INITIALIZER_LINES tag determines the maximum number of lines
+# the initial value of a variable or define consists of 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 initializer of individual variables and defines in the
+# documentation can be controlled using \showinitializer or \hideinitializer
+# command in the documentation regardless of this setting.
+
+MAX_INITIALIZER_LINES = 0
+
+# 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.
+
+SHOW_USED_FILES = YES
+
+# If the sources in your project are distributed over multiple directories
+# then setting the SHOW_DIRECTORIES tag to YES will show the directory hierarchy
+# in the documentation. The default is YES.
+
+SHOW_DIRECTORIES = NO
+
+# 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 progam writes to standard output
+# is used as the file version. See the manual for examples.
+
+#FILE_VERSION_FILTER =
+
+#---------------------------------------------------------------------------
+# configuration options related to warning and progress messages
+#---------------------------------------------------------------------------
+
+# The QUIET tag can be used to turn on/off the messages that are generated
+# by doxygen. Possible values are YES and NO. If left blank NO is used.
+
+QUIET = NO
+
+# The WARNINGS tag can be used to turn on/off the warning messages that are
+# generated by doxygen. Possible values are YES and NO. If left blank
+# NO is used.
+
+WARNINGS = YES
+
+# If WARN_IF_UNDOCUMENTED 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.
+
+WARN_IF_UNDOCUMENTED = YES
+
+# If WARN_IF_DOC_ERROR 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.
+
+WARN_IF_DOC_ERROR = YES
+
+# This WARN_NO_PARAMDOC option can be abled to get warnings for
+# functions that are documented, but have no documentation for their parameters
+# or return value. If set to NO (the default) doxygen will only warn about
+# wrong or incomplete parameter documentation, but not about the absence of
+# documentation.
+
+#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)
+
+WARN_FORMAT =
+
+# 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 stderr.
+
+WARN_LOGFILE = @abs_top_srcdir@/doc/doxygen/warn.log
+
+#---------------------------------------------------------------------------
+# configuration options related to the input files
+#---------------------------------------------------------------------------
+
+# The INPUT tag can be 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.
+
+INPUT = @abs_top_srcdir@/share/e-acsl \
+ @abs_top_srcdir@/share/e-acsl/segment_model \
+ @abs_top_srcdir@/share/e-acsl/bittree_model
+
+# If the value of the INPUT tag contains directories, you can use the
+# FILE_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 the following patterns are tested:
+# *.c *.cc *.cxx *.cpp *.c++ *.java *.ii *.ixx *.ipp *.i++ *.inl *.h *.hh *.hxx
+# *.hpp *.h++ *.idl *.odl *.cs *.php *.php3 *.inc *.m *.mm
+
+FILE_PATTERNS = *.h *.c
+
+# The RECURSIVE tag can be used to turn specify whether or not subdirectories
+# should be searched for input files as well. Possible values are YES and NO.
+# If left blank NO is used.
+
+RECURSIVE = NO
+
+# The EXCLUDE tag can be used to specify files and/or directories that should
+# 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.
+
+EXCLUDE =
+
+
+# The EXCLUDE_SYMLINKS tag can be used select whether or not files or
+# directories that are symbolic links (a Unix filesystem feature) are excluded
+# from the input.
+
+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 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.
+# Possible values are YES and NO. If left blank NO is used.
+
+EXAMPLE_RECURSIVE = YES
+
+# The IMAGE_PATH tag can be used to specify one or more files or
+# directories that contain image that are 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 <filter> <input-file>, where <filter>
+# is the value of the INPUT_FILTER tag, and <input-file> 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.
+
+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
+# info on how filters are used. If FILTER_PATTERNS is empty, INPUT_FILTER
+# is applied to all files.
+
+FILTER_PATTERNS =
+
+# If the FILTER_SOURCE_FILES tag is set to YES, the input filter (if set using
+# INPUT_FILTER) will be used to filter the input files when producing source
+# files to browse (i.e. when SOURCE_BROWSER is set to YES).
+
+FILTER_SOURCE_FILES = NO
+
+#---------------------------------------------------------------------------
+# 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 also
+# VERBATIM_HEADERS is set to NO.
+
+SOURCE_BROWSER = YES
+
+# Setting the INLINE_SOURCES tag to YES will include the body
+# of functions and classes directly in the documentation.
+
+INLINE_SOURCES = NO
+
+# Setting the STRIP_CODE_COMMENTS tag to YES (the default) will instruct
+# doxygen to hide any special comment blocks from generated source code
+# fragments. Normal C and C++ comments will always remain visible.
+
+STRIP_CODE_COMMENTS = NO
+
+# If the REFERENCED_BY_RELATION tag is set to YES (the default)
+# then for each documented function all documented
+# functions referencing it will be listed.
+
+REFERENCED_BY_RELATION = YES
+
+# If the REFERENCES_RELATION tag is set to YES (the default)
+# then for each documented function all documented entities
+# called/used by that function will be listed.
+
+REFERENCES_RELATION = 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.
+
+#USE_HTAGS = NO
+
+# If the VERBATIM_HEADERS tag is set to YES (the default) 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.
+
+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.
+
+ALPHABETICAL_INDEX = YES
+
+# If the alphabetical index is enabled (see ALPHABETICAL_INDEX) then
+# the COLS_IN_ALPHA_INDEX tag can be used to specify the number of columns
+# in which this list will be split (can be a number in the range [1..20])
+
+COLS_IN_ALPHA_INDEX = 4
+
+# 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 one or more prefixes that
+# should be ignored while generating the index headers.
+
+IGNORE_PREFIX = clang::
+
+#---------------------------------------------------------------------------
+# configuration options related to the HTML output
+#---------------------------------------------------------------------------
+
+# If the GENERATE_HTML tag is set to YES (the default) Doxygen will
+# generate HTML output.
+
+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. If left blank `html' will be used as the default path.
+
+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). If it is left blank
+# doxygen will generate files with .html extension.
+
+HTML_FILE_EXTENSION = .html
+
+# The HTML_HEADER tag can be used to specify a personal HTML header for
+# each generated HTML page. If it is left blank doxygen will generate a
+# standard header.
+
+HTML_HEADER =
+
+# The HTML_FOOTER tag can be used to specify a personal HTML footer for
+# each generated HTML page. If it is left blank doxygen will generate a
+# standard footer.
+
+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 the tag is left blank doxygen
+# will generate a default style sheet. Note that doxygen will try to copy
+# the style sheet file to the HTML output directory, so don't put your own
+# stylesheet in the HTML output directory as well, or it will be erased!
+
+HTML_STYLESHEET =
+
+# If the HTML_ALIGN_MEMBERS tag is set to YES, the members of classes,
+# files or namespaces will be aligned in HTML using tables. If set to
+# NO a bullet list will be used.
+
+HTML_ALIGN_MEMBERS = YES
+
+# If the GENERATE_HTMLHELP tag is set to YES, additional index files
+# will be generated that can be used as input for tools like the
+# Microsoft HTML help workshop to generate a compressed HTML help file (.chm)
+# of the generated HTML documentation.
+
+GENERATE_HTMLHELP = NO
+
+# If the GENERATE_HTMLHELP tag is set to YES, 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.
+
+CHM_FILE =
+
+# If the GENERATE_HTMLHELP tag is set to YES, 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.
+
+HHC_LOCATION =
+
+# If the GENERATE_HTMLHELP tag is set to YES, 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).
+
+GENERATE_CHI = NO
+
+# If the GENERATE_HTMLHELP tag is set to YES, 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.
+
+BINARY_TOC = NO
+
+# The TOC_EXPAND flag can be set to YES to add extra items for group members
+# to the contents of the HTML help documentation and to the tree view.
+
+TOC_EXPAND = NO
+
+# The DISABLE_INDEX tag can be used to turn on/off the condensed index at
+# top of each HTML page. The value NO (the default) enables the index and
+# the value YES disables it.
+
+DISABLE_INDEX = NO
+
+# This tag can be used to set the number of enum values (range [1..20])
+# that doxygen will group on one line in the generated HTML documentation.
+
+ENUM_VALUES_PER_LINE = 4
+
+# If the GENERATE_TREEVIEW tag 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 (for instance Mozilla 1.0+,
+# Netscape 6.0+, Internet explorer 5.0+, or Konqueror). Windows users are
+# probably better off using the HTML help feature.
+
+GENERATE_TREEVIEW = NO
+
+# 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.
+
+TREEVIEW_WIDTH = 250
+
+#---------------------------------------------------------------------------
+# configuration options related to the LaTeX output
+#---------------------------------------------------------------------------
+
+# If the GENERATE_LATEX tag is set to YES (the default) Doxygen will
+# generate Latex output.
+
+GENERATE_LATEX = NO
+
+# The LATEX_OUTPUT tag is used to specify where the LaTeX docs will be put.
+# If a relative path is entered the value of OUTPUT_DIRECTORY will be
+# put in front of it. If left blank `latex' will be used as the default path.
+
+LATEX_OUTPUT =
+
+# The LATEX_CMD_NAME tag can be used to specify the LaTeX command name to be
+# invoked. If left blank `latex' will be used as the default command name.
+
+LATEX_CMD_NAME = latex
+
+# The MAKEINDEX_CMD_NAME tag can be used to specify the command name to
+# generate index for LaTeX. If left blank `makeindex' will be used as the
+# default command name.
+
+MAKEINDEX_CMD_NAME = makeindex
+
+# If the COMPACT_LATEX tag is set to YES Doxygen generates more compact
+# LaTeX documents. This may be useful for small projects and may help to
+# save some trees in general.
+
+COMPACT_LATEX = NO
+
+# The PAPER_TYPE tag can be used to set the paper type that is used
+# by the printer. Possible values are: a4, a4wide, letter, legal and
+# executive. If left blank a4wide will be used.
+
+PAPER_TYPE = letter
+
+# The EXTRA_PACKAGES tag can be to specify one or more names of LaTeX
+# packages that should be included in the LaTeX output.
+
+EXTRA_PACKAGES =
+
+# The LATEX_HEADER tag can be used to specify a personal LaTeX header for
+# the generated latex document. The header should contain everything until
+# the first chapter. If it is left blank doxygen will generate a
+# standard header. Notice: only use this tag if you know what you are doing!
+
+LATEX_HEADER =
+
+# If the PDF_HYPERLINKS tag is set to YES, the LaTeX that is generated
+# is prepared for conversion to pdf (using ps2pdf). The pdf file will
+# contain links (just like the HTML output) instead of page references
+# This makes the output suitable for online browsing using a pdf viewer.
+
+PDF_HYPERLINKS = NO
+
+# If the USE_PDFLATEX tag is set to YES, pdflatex will be used instead of
+# plain latex in the generated Makefile. Set this option to YES to get a
+# higher quality PDF documentation.
+
+USE_PDFLATEX = NO
+
+# If the LATEX_BATCHMODE tag is set to YES, doxygen will add the \\batchmode.
+# command to the generated LaTeX files. This will instruct LaTeX to keep
+# running if errors occur, instead of asking the user for help.
+# This option is also used when generating formulas in HTML.
+
+LATEX_BATCHMODE = NO
+
+# If LATEX_HIDE_INDICES is set to YES then doxygen will not
+# include the index chapters (such as File Index, Compound Index, etc.)
+# in the output.
+
+LATEX_HIDE_INDICES = NO
+
+#---------------------------------------------------------------------------
+# configuration options related to the RTF output
+#---------------------------------------------------------------------------
+
+# If the GENERATE_RTF tag is set to YES Doxygen will generate RTF output
+# The RTF output is optimized for Word 97 and may not look very pretty with
+# other RTF readers or editors.
+
+GENERATE_RTF = NO
+
+# The RTF_OUTPUT tag is used to specify where the RTF docs will be put.
+# If a relative path is entered the value of OUTPUT_DIRECTORY will be
+# put in front of it. If left blank `rtf' will be used as the default path.
+
+RTF_OUTPUT =
+
+# If the COMPACT_RTF tag is set to YES Doxygen generates more compact
+# RTF documents. This may be useful for small projects and may help to
+# save some trees in general.
+
+COMPACT_RTF = NO
+
+# If the RTF_HYPERLINKS tag is set to YES, the RTF that is generated
+# will contain hyperlink fields. The RTF file will
+# contain links (just like the HTML output) instead of page references.
+# This makes the output suitable for online browsing using WORD or other
+# programs which support those fields.
+# Note: wordpad (write) and others do not support links.
+
+RTF_HYPERLINKS = NO
+
+# Load stylesheet definitions from file. Syntax is similar to doxygen's
+# config file, i.e. a series of assignments. You only have to provide
+# replacements, missing definitions are set to their default value.
+
+RTF_STYLESHEET_FILE =
+
+# Set optional variables used in the generation of an rtf document.
+# Syntax is similar to doxygen's config file.
+
+RTF_EXTENSIONS_FILE =
+
+#---------------------------------------------------------------------------
+# configuration options related to the man page output
+#---------------------------------------------------------------------------
+
+# If the GENERATE_MAN tag is set to YES (the default) Doxygen will
+# generate man pages
+
+GENERATE_MAN = NO
+
+# The MAN_OUTPUT tag is used to specify where the man pages will be put.
+# If a relative path is entered the value of OUTPUT_DIRECTORY will be
+# put in front of it. If left blank `man' will be used as the default path.
+
+MAN_OUTPUT =
+
+# The MAN_EXTENSION tag determines the extension that is added to
+# the generated man pages (default is the subroutine's section .3)
+
+MAN_EXTENSION =
+
+# If the MAN_LINKS tag is set to YES and Doxygen generates man output,
+# then it will generate one additional man file for each entity
+# documented in the real man page(s). These additional files
+# only source the real man page, but without them the man command
+# would be unable to find the correct page. The default is NO.
+
+MAN_LINKS = NO
+
+#---------------------------------------------------------------------------
+# configuration options related to the XML output
+#---------------------------------------------------------------------------
+
+# If the GENERATE_XML tag is set to YES Doxygen will
+# generate an XML file that captures the structure of
+# the code including all documentation.
+
+GENERATE_XML = NO
+
+# The XML_OUTPUT tag is used to specify where the XML pages will be put.
+# If a relative path is entered the value of OUTPUT_DIRECTORY will be
+# put in front of it. If left blank `xml' will be used as the default path.
+
+XML_OUTPUT = xml
+
+# The XML_SCHEMA tag can be used to specify an XML schema,
+# which can be used by a validating XML parser to check the
+# syntax of the XML files.
+
+XML_SCHEMA =
+
+# The XML_DTD tag can be used to specify an XML DTD,
+# which can be used by a validating XML parser to check the
+# syntax of the XML files.
+
+XML_DTD =
+
+# If the XML_PROGRAMLISTING tag is set to YES Doxygen will
+# dump the program listings (including syntax highlighting
+# and cross-referencing information) to the XML output. Note that
+# enabling this will significantly increase the size of the XML output.
+
+XML_PROGRAMLISTING = YES
+
+#---------------------------------------------------------------------------
+# configuration options for the AutoGen Definitions output
+#---------------------------------------------------------------------------
+
+# If the GENERATE_AUTOGEN_DEF tag is set to YES Doxygen will
+# generate an AutoGen Definitions (see autogen.sf.net) file
+# that captures the structure of the code including all
+# documentation. Note that this feature is still experimental
+# and incomplete at the moment.
+
+GENERATE_AUTOGEN_DEF = NO
+
+#---------------------------------------------------------------------------
+# configuration options related to the Perl module output
+#---------------------------------------------------------------------------
+
+# If the GENERATE_PERLMOD tag is set to YES Doxygen will
+# generate a Perl module file that captures the structure of
+# the code including all documentation. Note that this
+# feature is still experimental and incomplete at the
+# moment.
+
+GENERATE_PERLMOD = NO
+
+# If the PERLMOD_LATEX tag is set to YES Doxygen will generate
+# the necessary Makefile rules, Perl scripts and LaTeX code to be able
+# to generate PDF and DVI output from the Perl module output.
+
+PERLMOD_LATEX = NO
+
+# If the PERLMOD_PRETTY tag is set to YES the Perl module output will be
+# nicely formatted so it can be parsed by a human reader. This is useful
+# if you want to understand what is going on. On the other hand, if this
+# tag is set to NO the size of the Perl module output will be much smaller
+# and Perl will parse it just the same.
+
+PERLMOD_PRETTY = YES
+
+# The names of the make variables in the generated doxyrules.make file
+# are prefixed with the string contained in PERLMOD_MAKEVAR_PREFIX.
+# This is useful so different doxyrules.make files included by the same
+# Makefile don't overwrite each other's variables.
+
+PERLMOD_MAKEVAR_PREFIX =
+
+#---------------------------------------------------------------------------
+# Configuration options related to the preprocessor
+#---------------------------------------------------------------------------
+
+# If the ENABLE_PREPROCESSING tag is set to YES (the default) Doxygen will
+# evaluate all C-preprocessor directives found in the sources and include
+# files.
+
+ENABLE_PREPROCESSING = YES
+
+# If the MACRO_EXPANSION tag is set to YES Doxygen will expand all macro
+# names in the source code. If set to NO (the default) only conditional
+# compilation will be performed. Macro expansion can be done in a controlled
+# way by setting EXPAND_ONLY_PREDEF to YES.
+
+MACRO_EXPANSION = YES
+
+# If the EXPAND_ONLY_PREDEF and MACRO_EXPANSION tags are both set to YES
+# then the macro expansion is limited to the macros specified with the
+# PREDEFINED and EXPAND_AS_PREDEFINED tags.
+
+EXPAND_ONLY_PREDEF = YES
+
+# If the SEARCH_INCLUDES tag is set to YES (the default) the includes files
+# in the INCLUDE_PATH (see below) will be search if a #include is found.
+
+SEARCH_INCLUDES = YES
+
+# The INCLUDE_PATH tag can be used to specify one or more directories that
+# contain include files that are not input files but should be processed by
+# the preprocessor.
+
+INCLUDE_PATH =
+
+# You can use the INCLUDE_FILE_PATTERNS tag to specify one or more wildcard
+# patterns (like *.h and *.hpp) to filter out the header-files in the
+# directories. If left blank, the patterns specified with FILE_PATTERNS will
+# be used.
+
+INCLUDE_FILE_PATTERNS =
+
+# The PREDEFINED tag can be used to specify one or more macro names that
+# are defined before the preprocessor is started (similar to the -D option of
+# gcc). The argument of the tag is a list of macros of the form: name
+# or name=definition (no spaces). If the definition and the = are
+# omitted =1 is assumed. To prevent a macro definition from being
+# undefined via #undef or recursively expanded use the := operator
+# instead of the = operator.
+
+PREDEFINED = __attribute__(x)=
+
+# If the MACRO_EXPANSION and EXPAND_ONLY_PREDEF tags are set to YES then
+# this tag can be used to specify a list of macro names that should be expanded.
+# The macro definition that is found in the sources will be used.
+# Use the PREDEFINED tag if you want to use a different macro definition.
+
+EXPAND_AS_DEFINED =
+
+# If the SKIP_FUNCTION_MACROS tag is set to YES (the default) then
+# doxygen's preprocessor will remove all function-like macros that are alone
+# on a line, have an all uppercase name, and do not end with a semicolon. Such
+# function macros are typically used for boiler-plate code, and will confuse
+# the parser if not removed.
+
+SKIP_FUNCTION_MACROS = YES
+
+#---------------------------------------------------------------------------
+# Configuration::additions related to external references
+#---------------------------------------------------------------------------
+
+# The TAGFILES option can be used to specify one or more tagfiles.
+# Optionally an initial location of the external documentation
+# can be added for each tagfile. The format of a tag file without
+# this location is as follows:
+# TAGFILES = file1 file2 ...
+# Adding location for the tag files is done as follows:
+# TAGFILES = file1=loc1 "file2 = loc2" ...
+# where "loc1" and "loc2" can be relative or absolute paths or
+# URLs. If a location is present for each tag, the installdox tool
+# does not have to be run to correct the links.
+# Note that each tag file must have a unique name
+# (where the name does NOT include the path)
+# If a tag file is not located in the directory in which doxygen
+# is run, you must also specify the path to the tagfile here.
+
+TAGFILES =
+
+# When a file name is specified after GENERATE_TAGFILE, doxygen will create
+# a tag file that is based on the input files it reads.
+
+GENERATE_TAGFILE =
+
+# If the ALLEXTERNALS tag is set to YES all external classes will be listed
+# in the class index. If set to NO only the inherited external classes
+# will be listed.
+
+ALLEXTERNALS = YES
+
+# If the EXTERNAL_GROUPS tag is set to YES all external groups will be listed
+# in the modules index. If set to NO, only the current project's groups will
+# be listed.
+
+EXTERNAL_GROUPS = YES
+
+# The PERL_PATH should be the absolute path and name of the perl script
+# interpreter (i.e. the result of `which perl').
+
+PERL_PATH =
+
+#---------------------------------------------------------------------------
+# Configuration options related to the dot tool
+#---------------------------------------------------------------------------
+
+# If the CLASS_DIAGRAMS tag is set to YES (the default) Doxygen will
+# generate a inheritance diagram (in HTML, RTF and LaTeX) for classes with base
+# or super classes. Setting the tag to NO turns the diagrams off. Note that
+# this option is superseded by the HAVE_DOT option below. This is only a
+# fallback. It is recommended to install and use dot, since it yields more
+# powerful graphs.
+
+CLASS_DIAGRAMS = YES
+
+# If set to YES, the inheritance and collaboration graphs will hide
+# inheritance and usage relations if the target is undocumented
+# or is not a class.
+
+HIDE_UNDOC_RELATIONS = NO
+
+# If you set the HAVE_DOT tag to YES then doxygen will assume the dot tool is
+# available from the path. This tool is part of Graphviz, a graph visualization
+# toolkit from AT&T and Lucent Bell Labs. The other options in this section
+# have no effect if this option is set to NO (the default)
+
+HAVE_DOT = @HAVE_DOT@
+
+# If the CLASS_GRAPH and HAVE_DOT tags are set to YES then doxygen
+# will generate a graph for each documented class showing the direct and
+# indirect inheritance relations. Setting this tag to YES will force the
+# the CLASS_DIAGRAMS tag to NO.
+
+CLASS_GRAPH = YES
+
+# If the COLLABORATION_GRAPH and HAVE_DOT tags are set to YES then doxygen
+# will generate a graph for each documented class showing the direct and
+# indirect implementation dependencies (inheritance, containment, and
+# class references variables) of the class with other documented classes.
+
+COLLABORATION_GRAPH = NO
+
+# If the GROUP_GRAPHS and HAVE_DOT tags are set to YES then doxygen
+# will generate a graph for groups, showing the direct groups dependencies
+
+#GROUP_GRAPHS = YES
+
+# If the UML_LOOK tag is set to YES doxygen will generate inheritance and
+# collaboration diagrams in a style similar to the OMG's Unified Modeling
+# Language.
+
+UML_LOOK = NO
+
+# If set to YES, the inheritance and collaboration graphs will show the
+# relations between templates and their instances.
+
+TEMPLATE_RELATIONS = NO
+
+# If the ENABLE_PREPROCESSING, SEARCH_INCLUDES, INCLUDE_GRAPH, and HAVE_DOT
+# tags are set to YES then doxygen will generate a graph for each documented
+# file showing the direct and indirect include dependencies of the file with
+# other documented files.
+
+INCLUDE_GRAPH = YES
+
+# If the ENABLE_PREPROCESSING, SEARCH_INCLUDES, INCLUDED_BY_GRAPH, and
+# HAVE_DOT tags are set to YES then doxygen will generate a graph for each
+# documented header file showing the documented files that directly or
+# indirectly include this file.
+
+INCLUDED_BY_GRAPH = YES
+
+# If the CALL_GRAPH and HAVE_DOT tags are set to YES then doxygen will
+# generate a call dependency graph for every global function or class method.
+# Note that enabling this option will significantly increase the time of a run.
+# So in most cases it will be better to enable call graphs for selected
+# functions only using the \callgraph command.
+
+CALL_GRAPH = NO
+
+# If the GRAPHICAL_HIERARCHY and HAVE_DOT tags are set to YES then doxygen
+# will graphical hierarchy of all classes instead of a textual one.
+
+GRAPHICAL_HIERARCHY = YES
+
+# If the DIRECTORY_GRAPH, SHOW_DIRECTORIES and HAVE_DOT tags are set to YES
+# then doxygen will show the dependencies a directory has on other directories
+# in a graphical way. The dependency relations are determined by the #include
+# relations between the files in the directories.
+
+DIRECTORY_GRAPH = NO
+
+# The DOT_IMAGE_FORMAT tag can be used to set the image format of the images
+# generated by dot. Possible values are png, jpg, or gif
+# If left blank png will be used.
+
+DOT_IMAGE_FORMAT = png
+
+# The tag DOT_PATH can be used to specify the path where the dot tool can be
+# found. If left blank, it is assumed the dot tool can be found in the path.
+
+DOT_PATH =
+
+# The DOTFILE_DIRS tag can be used to specify one or more directories that
+# contain dot files that are included in the documentation (see the
+# \dotfile command).
+
+DOTFILE_DIRS =
+
+# The MAX_DOT_GRAPH_WIDTH tag can be used to set the maximum allowed width
+# (in pixels) of the graphs generated by dot. If a graph becomes larger than
+# this value, doxygen will try to truncate the graph, so that it fits within
+# the specified constraint. Beware that most browsers cannot cope with very
+# large images.
+
+MAX_DOT_GRAPH_DEPTH = 0
+
+# Set the DOT_TRANSPARENT tag to YES to generate images with a transparent
+# background. This is disabled by default, which results in a white background.
+# Warning: Depending on the platform used, enabling this option may lead to
+# badly anti-aliased labels on the edges of a graph (i.e. they become hard to
+# read).
+
+DOT_TRANSPARENT = NO
+
+# Set the DOT_MULTI_TARGETS tag to YES allow dot to generate multiple output
+# files in one run (i.e. multiple -o and -T options on the command line). This
+# makes dot run faster, but since only newer versions of dot (>1.8.10)
+# support this, this feature is disabled by default.
+
+DOT_MULTI_TARGETS = NO
+
+# If the GENERATE_LEGEND tag is set to YES (the default) Doxygen will
+# generate a legend page explaining the meaning of the various boxes and
+# arrows in the dot generated graphs.
+
+GENERATE_LEGEND = NO
+
+# If the DOT_CLEANUP tag is set to YES (the default) Doxygen will
+# remove the intermediate dot files that are used to generate
+# the various graphs.
+
+DOT_CLEANUP = YES
+
+#---------------------------------------------------------------------------
+# Configuration::additions related to the search engine
+#---------------------------------------------------------------------------
+# The SEARCHENGINE tag specifies whether or not a search engine should be
+# used. If set to NO the values of all tags below this one will be ignored.
+
+SEARCHENGINE = NO
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_assert.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_assert.h
index 9e0f59c4f9105916cd257dba9cd08d06e7214f69..4a9c956f9ff18a7d070fdd00ae4ca8068e081668 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_assert.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_assert.h
@@ -20,27 +20,34 @@
/* */
/**************************************************************************/
+/*! ***********************************************************************
+ * \file e_acsl_assert.h
+ * \brief E-ACSL assertions and abort statements.
+***************************************************************************/
+
#ifndef E_ACSL_ASSERT
#define E_ACSL_ASSERT
#include "e_acsl_string.h"
#include "e_acsl_printf.h"
-/* Drop-in replacement for abort function */
+/*! \brief Drop-in replacement for abort function */
#define abort() exec_abort(__LINE__, __FILE__)
-/* Output a message to error stream using printf-like format string and abort
- * the execution. This is a wrapper for eprintf combined with abort */
+/*! \brief Output a message to error stream using printf-like format string
+ * and abort the execution.
+ *
+ * This is a wrapper for \p eprintf combined with \p abort */
static void vabort(char *fmt, ...);
-/* Drop-in replacement for system-wide assert macro */
+/*! \brief Drop-in replacement for system-wide assert macro */
#define assert(expr) \
((expr) ? (void)(0) : vabort("%s at %s:%d\n", \
#expr, __FILE__,__LINE__))
-/* Assert with printf-like error message support */
+/*! \brief Assert with printf-like error message support */
#define vassert(expr, fmt, ...) \
- vassert_fail(expr, __LINE__, __FILE__, fmt, __VA_ARGS__)
+ vassert_fail(expr, __LINE__, __FILE__, fmt, __VA_ARGS__)
static void exec_abort(int line, const char *file) {
eprintf("Execution aborted (%s:%d)\n", file, line);
@@ -62,7 +69,7 @@ static void vassert_fail(int expr, int line, char *file, char *fmt, ...) {
}
}
-/* Print a message to stderr and abort the execution */
+/*! \brief Print a message to stderr and abort the execution */
static void vabort(char *fmt, ...) {
va_list va;
va_start(va,fmt);
@@ -71,7 +78,7 @@ static void vabort(char *fmt, ...) {
abort();
}
-/* Default implementation of E-ACSL runtime assertions */
+/*! \brief Default implementation of E-ACSL runtime assertions */
static void runtime_assert(int predicate, char *kind,
char *fct, char *pred_txt, int line) {
if (!predicate) {
@@ -81,17 +88,18 @@ static void runtime_assert(int predicate, char *kind,
}
}
-/* Alias for runtime assertions. Since `__e_acsl_assert` is added as a weak
- * alias user-defined implementation of the `__e_acsl_assert` function will be
- * preferred at link time. */
+/*! \brief Alias for runtime assertions.
+ *
+ * Since \p __e_acsl_assert is added as a weak alias user-defined implementation
+ * of the \p __e_acsl_assert function will be preferred at link time. */
void __e_acsl_assert(int pred, char *kind, char *fct, char *pred_txt, int line)
__attribute__ ((weak, alias ("runtime_assert")));
/* Instances of assertions shared accross different memory models */
-/* Abort the execution if the size of the pointer computed during
- * instrumentation (_ptr_sz) does not match the size of the pointer used
- * by a compiler (void*) */
+/*! \brief Abort the execution if the size of the pointer computed during
+ * instrumentation (\p _ptr_sz) does not match the size of the pointer used
+ * by a compiler (\p void*) */
#define arch_assert(_ptr_sz) \
vassert(_ptr_sz == sizeof(void*), \
"Mismatch of instrumentation- and compile-time pointer sizes: " \
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_bits.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_bits.h
index 83baf0203e8ad739d0ffa94738214be88e13dab7..c7114754530d7e8738b0795e17ba7349466248bc 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_bits.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_bits.h
@@ -20,19 +20,23 @@
/* */
/**************************************************************************/
-/* Bit-level manipulations and endianness checks.
- * Should be included after e_acsl_printf.h and e_acsl_string.h headers. */
+/*! ***********************************************************************
+ * \file e_acsl_bits.h
+ * \brief Bit-level manipulations and endianness checks.
+ *
+ * Should be included after e_acsl_printf.h and e_acsl_string.h headers.
+ *
+ * FIXME: Present implementation is built for little-endian byte order. That
+ * is, the implementation assumes that least significant bytes are stored at
+ * the highest memory addresses. In future support for big-endian/PDP byte
+ * orders should also be provided.
+***************************************************************************/
#ifndef E_ACSL_BITS
#define E_ACSL_BITS
#include <stdint.h>
-/* FIXME: Present implementation is built for little-endian byte order. That
- * is, the implementation assumes that least significant bytes are stored at
- * the highest memory addresses. In future support for big-endian/PDP byte
- * orders should also be provided. */
-
/* Check if we have little-endian and abort the execution otherwise. */
#if __BYTE_ORDER__ == __ORDER_BIG_ENDIAN__
# error "Big-endian byte order is unsupported"
@@ -44,58 +48,117 @@
/* Bit-level manipulations {{{ */
-/* 64-bit type with all bits set to zeroes */
-const uint64_t ZERO = 0;
-
/* 64-bit type with all bits set to ones */
-const uint64_t ONE = ~0;
+#define ONE UINT64_MAX
-/* Set a given bit in a number to '1'.
- * Example: bitset(7, x) changes 7th lowest bit of x to 1 */
+/* 64-bit type with all bits set to zeroes */
+#define ZERO (~ONE)
+
+/* Set a given bit in a number to '1' (least-significant bit is at index zero). *
+ * Example:
+ * int x = 0;
+ * // x => 0000 0000 ...
+ * bitset(0, x)
+ * // x => 1000 0000 ...
+ * bitset(7, x)
+ * // x => 1000 0001 ... */
#define setbit(_bit,_number) (_number |= 1 << _bit)
-/* Same as bitset but the bit is set of 0 */
+/* Same as bitset but the bit cleared (set of zer0) */
#define clearbit(_bit, _number) (_number &= ~(1 << _bit))
-/* Evaluates to a true value if a given bit in a number is set to 1. */
+/* Evaluates to a true value if a given bit in a number is set to 1.
+ * int x = 1;
+ * // x => 1000 0000 ...
+ * checkbit(0, x) // true
+ * checkbit(1, x) // false */
#define checkbit(_bit, _number) ((_number >> _bit) & 1)
-/* Toggle a given bit. */
+/* Toggle a given bit.
+ * Example:
+ * int x = 4; (assume little-endian)
+ * // x => 0010 0000 ...
+ * togglebit(3, x);
+ * // x => 0000 0000 ...
+ * togglebit(3, x);
+ * // x => 0010 0000 ... */
#define togglebit(_bit, _number) (_number ^= 1 << _bit)
/* Set a given bit to a specified value (e.g., 0 or 1). */
#define changebit(_bit, _val, _number) \
(_number ^= (-_val ^ _number) & (1 << _bit))
-/* Set up to 64-bit in given number (from the left)
- * Example: setbits64(x, 7) sets first 7 bits in x to ones */
-#define setbits64(_number, _bits) (_number |= ~(ONE << _bits))
-
-/* Same as setbits64 but clears bits (sets to zeroes) */
-#define clearbits64(_number, _bits) (_number &= ONE << _bits)
-
-/* Assume _number is a 64-bit number and sets _bits from the right to ones
- * Example: let x is a 64-bit zero, then setbits64(x, 7) will yield:
- * 00000000 00000000 00000000 00000000 00000000 00000000 00000000 01111111 */
-#define setbits64_right(_number, _bits) (_number |= ~(ONE >> _bits))
+/* Set up to 64 bits from left to right to ones.
+ * Example:
+ * int x = 0;
+ * // x => 00000000 00000000 00000000 00000000
+ * setbits64(11, x)
+ * // => 11111111 11100000 00000000 00000000
+ * setbits64(65, x)
+ * // => behaviour undefined */
+#define setbits64(_bits, _number) (_number |= ~(ONE << _bits))
+
+/* Same as `setbits64' but clear the bits (set to zeroes). */
+#define clearbits64(_bits, _number) (_number &= ONE << _bits)
+
+/* Assume that `_number' is a 64-bit integral type.
+ * Set `_bits' bits from right to the left starting from a 64-bit boundary.
+ * Example:
+ * long x = 0;
+ * // x => ... 00000000 00000000 00000000 00000000
+ * setbits64_right(10, x)
+ * // x => ... 00000000 00000000 00000011 11111111 */
+#define setbits64_right(_bits, _number) (_number |= ~(ONE >> _bits))
/* Same as setbits64_right but clears bits (sets to zeroes) */
-#define clearbits64_right(_number, _bits) (_number &= ONE >> _bits)
-
+#define clearbits64_right(_bits, _number) (_number &= ONE >> _bits)
+
+/* Set `size' bits starting from an address given by `ptr' to ones.
+ * Example:
+ * char a[4];
+ * memset(a,0,4);
+ * // => 00000000 00000000 00000000 00000000
+ * setbits(&a, 11);
+ * // => 11111111 11100000 00000000 00000000 */
void setbits(void *ptr, size_t size) {
size_t i;
int64_t *lp = (int64_t*)ptr;
for (i = 0; i < size/64; i++)
*(lp+i) |= ONE;
- setbits64(*(lp+i), size%64);
+ setbits64(size%64, *(lp+i));
}
+/* Same as `setbits' but clear the bits (set to zeroes). */
void clearbits(void *ptr, size_t size) {
size_t i;
int64_t *lp = (int64_t*)ptr;
for (i = 0; i < size/64; i++)
*(lp+i) &= ZERO;
- clearbits64(*(lp+i), size%64);
+ clearbits64(size%64, *(lp+i));
+}
+
+/* Same as `setbits' but set the bits from right to left
+ * Example:
+ * char a[4];
+ * memset(a,0,4);
+ * // => 00000000 00000000 00000000 00000000
+ * setbits_right(&a, 11);
+ * // => 00000000 00000000 00000111 11111111 */
+void setbits_right(void *ptr, size_t size) {
+ size_t i = 0;
+ int64_t *lp = (int64_t*)ptr - 1;
+ for (i = 0; i < size/64; i++)
+ *(lp-i) |= ONE;
+ setbits64_right(size%64, *(lp-i));
+}
+
+/* Same as `setbits_right' but clear the bits (set to zeroes). */
+void clearbits_right(void *ptr, size_t size) {
+ size_t i = 0;
+ int64_t *lp = (int64_t*)ptr - 1;
+ for (i = 0; i < size/64; i++)
+ *(lp-i) &= ZERO;
+ clearbits64_right(size%64, *(lp-i));
}
/* }}} */
#endif
\ No newline at end of file
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_malloc.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_malloc.h
index 972b4315437dc362daa0fb64aa44458b6a15bf19..bf1979b7cee4bc72e47eba99f03fe7ee699fdc47 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_malloc.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_malloc.h
@@ -20,9 +20,11 @@
/* */
/**************************************************************************/
-/**********************************/
-/* Bindings for memory allocation */
-/**********************************/
+/*! ***********************************************************************
+ * \file e_acsl_malloc.h
+ *
+ * \brief E-ACSL memory allocation bindings.
+***************************************************************************/
/* Should be included after
* printf, debug and assert but before the actual code */
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
index 8fec227fc0b519277594caadf8878f8269e7fa01..05546aaf273bace1e17569e77e1641324e0738cc 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
@@ -20,71 +20,87 @@
/* */
/**************************************************************************/
+/*! ***********************************************************************
+ * \file e_acsl_mmodel_api.h
+ * \brief Public C API of E-ACSL Runtime Library
+ *
+ * Functions and variables with non-static linkage used for instrumentation.
+***************************************************************************/
+
#ifndef E_ACSL_MMODEL
#define E_ACSL_MMODEL
#include <stddef.h>
-/* Runtime assertion verifying a predicate */
+/*! \brief Runtime assertion verifying a predicate
+ * \param pred integer code of a predicate
+ * \param kind a C string representing an annotation's
+ * kind (e.g., "Assertion")
+ * \param fct
+ * \param pred_txt stringified predicate
+ * \param line line number of the predicate placement in the
+ * un-instrumented file */
/*@ requires pred != 0;
@ assigns \nothing; */
void e_acsl_assert(int pred, char *kind, char *fct, char *pred_txt, int line)
__attribute__((FC_BUILTIN));
-/* allocate size bytes and store the returned block
- * for further information, see malloc */
+/*! \brief Drop-in replacement for \p malloc with memory tracking enabled.
+ *
+ * For further information, see \p malloc(3). */
/*@ assigns \result \from size; */
void * __malloc(size_t size)
__attribute__((FC_BUILTIN)) ;
-/* free the block starting at ptr,
- * for further information, see free */
-/*@ assigns *((char*)ptr) \from ptr; */
-void __free(void * ptr)
- __attribute__((FC_BUILTIN));
-
-/* evaluate to a non-zero value if ptr points to a start address of a block
- * allocated via a memory allocation function (e.g., malloc, realloc etc) */
-/*@ assigns \result \from ptr; */
-int __freeable(void * ptr)
+/*! \brief Drop-in replacement for \p calloc with memory tracking enabled.
+ *
+ * For further information, see \p calloc(3). */
+/*@ assigns \result \from nbr_elt,size_elt; */
+void * __calloc(size_t nbr_elt, size_t size_elt)
__attribute__((FC_BUILTIN));
-/* resize the block starting at ptr to fit its new size,
- * for further information, see realloc */
+/*! \brief Drop-in replacement for \p realloc with memory tracking enabled.
+ *
+ * For further information, see realloc(3) */
/*@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
void * __realloc(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
-/* allocate memory for an array of nbr_block elements of size_block size,
- * this memory is set to zero, the returned block is stored,
- * for further information, see calloc */
-/*@ assigns \result \from nbr_elt,size_elt; */
-void * __calloc(size_t nbr_elt, size_t size_elt)
+/*! \brief Drop-in replacement for \p free with memory tracking enabled.
+ *
+ * For further information, see \p free(3). */
+/*@ assigns *((char*)ptr) \from ptr; */
+void __free(void * ptr)
__attribute__((FC_BUILTIN));
-/* From outside the library, the following functions have no side effect */
-
-/* store the block of size bytes starting at ptr */
+/*! \brief Store stack or globally-allocated memory block
+ * starting at an address given by \p ptr.
+ *
+ * \param ptr base address of the tracked memory block
+ * \param size size of the tracked block in bytes */
/*@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
void * __store_block(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
-/* remove the block starting at ptr */
+/*! \brief Remove a memory block which base address is \p ptr from tracking. */
/*@ assigns \nothing; */
void __delete_block(void * ptr)
__attribute__((FC_BUILTIN));
-/* mark the size bytes of ptr as initialized */
+/*! \brief Mark the \p size bytes starting at an address given by \p ptr as
+ * initialized. */
/*@ assigns \nothing; */
void __initialize(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
-/* mark all bytes of ptr as initialized */
+/*! \brief Mark all bytes belonging to a memory block which start address is
+ * given by \p ptr as initialized. */
/*@ assigns \nothing; */
void __full_init(void * ptr)
__attribute__((FC_BUILTIN));
-/* marks a block as read-only */
+/*! \brief Mark a memory block which start address is given by \ptr as
+ * read-only. */
/*@ assigns \nothing; */
void __readonly(void * ptr)
__attribute__((FC_BUILTIN));
@@ -93,34 +109,57 @@ void __readonly(void * ptr)
/* E-ACSL annotations */
/* ****************** */
-/* return whether the first size bytes of ptr are readable/writable */
+/*!\brief Implementation of the \b \\freeable predicate of E-ACSL.
+ *
+ * Evaluate to a non-zero value if \p ptr points to a start address of
+ * a block allocated via \p malloc, \p calloc or \p realloc. */
+/*@ assigns \result \from ptr; */
+int __freeable(void * ptr)
+ __attribute__((FC_BUILTIN));
+
+/*! \brief Implementation of the \b \\valid predicate of E-ACSL.
+ *
+ * Return a non-zero value if the first \p size bytes starting at an address given
+ * by \p ptr are readable and writable and 0 otherwise. */
/*@ ensures \result == 0 || \result == 1;
@ ensures \result == 1 ==> \valid(((char *)ptr)+(0..size-1));
@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
int __valid(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
-/* return whether the first size bytes of ptr are readable */
+/*! \brief Implementation of the \b \\valid_read predicate of E-ACSL.
+ *
+ * Return a non-zero value if the first \p size bytes starting at an address
+ * given by \p ptr are readable and 0 otherwise. */
/*@ ensures \result == 0 || \result == 1;
@ ensures \result == 1 ==> \valid_read(((char *)ptr)+(0..size-1));
@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
int __valid_read(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
-/* return the base address of the block containing ptr */
+/*! \brief Implementation of the \b \\base_addr predicate of E-ACSL.
+ *
+ * Return the base address of the memory block containing an address given
+ * by \p ptr */
/*@ ensures \result == \base_addr(ptr);
@ assigns \result \from ptr; */
void * __base_addr(void * ptr)
__attribute__((FC_BUILTIN));
-/* return the length (in bytes) of the block containing ptr */
+/*! \brief Implementation of the \b \\block_length predicate of E-ACSL.
+ *
+ * Return the byte length of the memory block of the block containing a memory
+ * address given by \p ptr */
/*@ ensures \result == \block_length(ptr);
@ assigns \result \from ptr; */
size_t __block_length(void * ptr)
__attribute__((FC_BUILTIN));
-/* return the offset of ptr within its block
- * FIXME: The return type of __offset should be changed to size_t.
+/*! \brief Implementation of the \b \\offset predicate of E-ACSL.
+ *
+ * Return the byte offset of address given by \p ptr within a memory blocks
+ * it belongs to */
+/* FIXME: The return type of __offset should be changed to size_t.
* In the current E-ACSL/Frama-C implementation, however, this change
* leads to a Frama-C failure. */
/*@ ensures \result == \offset(ptr);
@@ -128,41 +167,40 @@ size_t __block_length(void * ptr)
int __offset(void * ptr)
__attribute__((FC_BUILTIN));
-/* return whether the size bytes of ptr are initialized */
+/*! \brief Implementation of the \b \\initialized predicate of E-ACSL.
+ *
+ * Return a non-zero value if \p size bytes starting from an address given by
+ * \p ptr are initialized and zero otherwise. */
/*@ ensures \result == 0 || \result == 1;
@ ensures \result == 1 ==> \initialized(((char *)ptr)+(0..size-1));
@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
int __initialized(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
-/* print the content of the abstract structure */
-void __e_acsl_memory_debug(void)
- __attribute__((FC_BUILTIN));
-
/*@ ghost int extern __e_acsl_internal_heap; */
-/* erase the content of the abstract structure
- * have to be called at the end of the `main` */
+/*! \brief Clean-up memory tracking state before a program's termination. */
/*@ assigns \nothing; */
void __e_acsl_memory_clean(void)
__attribute__((FC_BUILTIN));
-/* initialize the abstract structure
- * have to be called before any other statement in `main` */
+/*! \brief Initialize memory tracking state.
+ *
+ * Called before any other statement in \p main */
/*@ assigns \nothing; */
void __e_acsl_memory_init(int *argc_ref, char ***argv, size_t ptr_size)
__attribute__((FC_BUILTIN));
-/* return the number of bytes dynamically allocated */
+/*! \brief Return the cumulative size (in bytes) of tracked heap allocation. */
/*@ assigns \result \from __e_acsl_internal_heap; */
size_t __get_heap_size(void)
__attribute__((FC_BUILTIN));
-/* for predicates */
+/*! \brief A variable holding a cumulative size (in bytes) of tracked
+ * heap allocation. */
extern size_t __heap_size;
/*@ predicate diffSize{L1,L2}(integer i) =
\at(__heap_size, L1) - \at(__heap_size, L2) == i;
*/
-
#endif
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_printf.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_printf.h
index c7617e74b595d7e57e1124fdf392eef0db1ea64a..d38530a31140add633a830fc5aafc581b2f91a74 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_printf.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_printf.h
@@ -33,6 +33,39 @@
/* */
/****************************************************************************/
+/*! ***********************************************************************
+ * \file e_acsl_printf.h
+ * \brief Malloc and stdio free implementation printf.
+ *
+ * Supported format strings:
+ * - Flag characters:
+ * - 0 - the following value will be is zero-padded.
+ *
+ * - Field width:
+ * - Optional positive decimal integer following flag characters.
+ *
+ * - Length modifier:
+ * - l - the following integer conversion corresponds to a long int or
+ * unsigned long int argument.
+ *
+ * - Standard conversion specifiers:
+ * - d - signed integers.
+ * - u - unsigned integers.
+ * - f - floating point numbers. Floating point numbers do not support
+ * - precision specification.
+ * - x,X - hexadecimal numbers.
+ * - p - void pointers.
+ *
+ * - Non-standard conversion specifiers:
+ * - a - memory-address.
+ * - b, B - print field width bits of a number left-to-right (b) or
+ * right-to-left (B). Unless specified field-width of 8 is used. Bits
+ * over a 64-bit boundary are ignored.
+ * - v, V - print first field width bits of a memory region given by a
+ * void pointer left-to-right (v) or right-to-left (V). Unless specified
+ * field-width of 8 is used.
+***************************************************************************/
+
#ifndef E_ACSL_PRINTF
#define E_ACSL_PRINTF
@@ -49,37 +82,7 @@
# include <linux/limits.h>
#endif
-/* Malloc/stdio free printf
- *
- * NOTE: The below implementation does not require system-wide I/O (stdio.h).
- *
- * Supported format strings:
- * - Flag characters:
- * 0 - the following value will be is zero-padded.
- *
- * - Field width:
- * Optional positive decimal integer following flag characters.
- *
- * - Length modifier:
- * l - the following integer conversion corresponds to a long int or
- * unsigned long int argument.
- *
- * - Standard conversion specifiers:
- * d - signed integers.
- * u - unsigned integers.
- * f - floating point numbers. Floating point numbers do not support
- * precision specification.
- * x,X - hexadecimal numbers.
- * p - void pointers.
- *
- * - Non-standard conversion specifiers:
- * a - memory-address.
- * b, B - print field width bits of a number left-to-right (b) or
- * right-to-left (B). Unless specified field-width of 8 is used. Bits
- * over a 64-bit boundary are ignored.
- * v, V - print first field width bits of a memory region given by a
- * void pointer left-to-right (v) or right-to-left (V). Unless specified
- * field-width of 8 is used. */
+
/* ****************** */
/* Public API */
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_string.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_string.h
index 9d2bc20fb61dbdc3fdafc73772a4b56371bf8ef2..67e0ed29d93a5a881d50b8045b63a17d4b3c00e5 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_string.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_string.h
@@ -20,18 +20,21 @@
/* */
/**************************************************************************/
-/** Replacement of system-wide <string.h> header for use with E-ACSL
+/*! ***********************************************************************
+ * \file e_acsl_string.h
+ * \brief Replacement of system-wide \p <string.h> header for use with E-ACSL
* runtime library.
*
* Intended use:
- * - For the case when the sources are compiled using GCC prefer __builtin_
- * versions of some of the string.h functions (e.g., memset). This is mostly
- * because the GCC builtins are on average faster. *
+ * - For the case when the sources are compiled using GCC prefer \p __builtin_
+ * versions of some of the string.h functions (e.g., \p memset). This is
+ * mostly because the GCC builtins are on average faster.
* - For the case it is not GCC system-wide versions should be used. This
- * and the above options require E_ACSL_BUILTINS macro to be defined
+ * and the above options require \p E_ACSL_BUILTINS macro to be defined
* at compile-time.
* - For the case when the analysed program contains customised definitions
- * of string.h functions use GLIBC-based implementations. */
+ * of string.h functions use GLIBC-based implementations.
+***************************************************************************/
#ifndef E_ACSL_STD_STRING
#define E_ACSL_STD_STRING
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_syscall.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_syscall.h
index da7ec1e46480a7596ba10804f88d3e6882682364..6f7db7a351c781feefeaf7cc7d46104991463814 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_syscall.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_syscall.h
@@ -20,12 +20,25 @@
/* */
/**************************************************************************/
-/* Re-declaration of standard libc syscall-based functions using direct
- * application of syscall. The aim is to avoid issues for the case when a
+/*! ***********************************************************************
+ * \file e_acsl_syscall.h
+ * \brief E-ACSL \p syscall bindings.
+ *
+ * Re-declaration of standard libc syscall-based functions using direct
+ * application of \p syscall. The aim is to avoid issues for the case when a
* target program provides custom implementations or wrappers for such
* functions. For instance, if an instrumented program provides a custom
* implementation of `write` E-ACSL RTL will still use the native system
- * call. */
+ * call.
+ *
+ * Note that this header following does not provide a re-declaration for \p
+ * mmap. This is because \p syscall returns \p int, while \p mmap should
+ * return an integer type wide enough to hold a memory address address. Also,
+ * since there is no \p sbrk system call, a re-declaration of \p sbrk is also
+ * missing. As a result, programs providing custom definitions of \p syscall,
+ * \p mmap or \p sbrk should be rejected. Re-definitions of the below functions
+ * should be safe.
+***************************************************************************/
#ifndef E_ACSL_SYSCALL
#define E_ACSL_SYSCALL
@@ -33,14 +46,8 @@
# include <fcntl.h>
# include <unistd.h>
# include <sys/syscall.h> /* SYS_xxx definitions */
-int syscall(int number, ...);
-/* Note that the following does not provide a re-declaration for `mmap`. This
- * is because syscall returns int, while mmap should return an integer type wide
- * enough to hold a memory address address. Also, since there is no `sbrk`
- * system call, re-declaration of sbrk is also missing. As a result, programs
- * providing custom definitions of `syscall`, `mmap` or `sbrk` should be
- * rejected. Re-definitions of the below functions should be safe. */
+int syscall(int number, ...);
# define write(...) syscall(SYS_write, __VA_ARGS__)
# define open(...) syscall(SYS_open, __VA_ARGS__)