Merge remote-tracking branch 'upstream/master' into merge-master-2017-08-03

.travis.yml

@@ -134,6 +134,15 @@ matrix:
       script: scripts/travis_lint.sh
       before_cache:
 
+    - env: NAME="DOXYGEN-CHECK"
+      addons:
+        apt:
+          packages:
+            - doxygen
+      install:
+      script: scripts/travis_doxygen.sh
+      before_cache:
+
   allow_failures:
     - env: NAME="CPP-LINT"
       install:
@@ -150,7 +159,7 @@ install:
 
 script:
   - if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
-    COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test" &&
+    COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\"" &&
     eval ${PRE_COMMAND} ${COMMAND}
   - COMMAND="make -C unit CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\" -j2" &&
     eval ${PRE_COMMAND} ${COMMAND}

CODING_STANDARD

@@ -1,205 +0,0 @@
-Here a few minimalistic coding rules for the CPROVER source tree.
-
-Whitespaces:
-- Use 2 spaces indent, no tabs.
-- No lines wider than 80 chars.
-  - When line is wider, do the following:
-    - Subsequent lines should be indented two more than the initial line
-    - Break after = if it is part of an assignment
-    - For chained calls, prefer immediately before .
-    - For other operators (e.g. &&, +) prefer immediately after the operator
-    - For brackets, break after the bracket
-      - In the case of function calls, put each argument on a separate line if
-        they do not fit after one line break
-      - Nested function calls do not need to be broken up into separate lines even
-        if the outer function call does.
-- If a method is bigger than 50 lines, break it into parts.
-- Put matching { } into the same column.
-- No spaces around operators (=, +, ==, ...)
-  Exceptions: Spaces around &&, || and <<
-- Space after comma (parameter lists, argument lists, ...)
-- Space after colon inside 'for'
-- For pointers and references, the */& should be attached to the variable name
-  as oppposed to the tyep. E.g. for a pointer to an int the syntax would be:
-    `int *x;`
-- No whitespaces at end of line
-- No whitespaces in blank lines
-- Put argument lists on next line (and ident 2 spaces) if too long
-- Put parameters on separate lines (and ident 2 spaces) if too long
-- No whitespaces around colon for inheritance,
-  put inherited into separate lines in case of multiple inheritance
-- The initializer list follows the constructor without a whitespace
-  around the colon. Break line after the colon if required and indent members.
-- if(...), else, for(...), do, and while(...) are always in a separate line
-- Break expressions in if, for, while if necessary and align them
-  with the first character following the opening parenthesis
-- Use {} instead of ; for the empty statement
-- Single line blocks without { } are allowed,
-  but put braces around multi-line blocks
-- Use blank lines to visually separate logically cohesive code blocks
-  within a function
-- Have a newline at the end of a file
-
-Comments:
-- Do not use /* */ except for file and function comment blocks
-- Each source and header file must start with a comment block
-  stating the Module name and Author [will be changed when we roll out doxygen]
-- Each function in the source file (not the header) is preceded
-  by a function comment header consisting of a comment block stating
-  Name, Inputs,  Outputs and Purpose [will be changed when we roll
-  out doxygen]
-   - It should look like this:
-   ```
-   /*******************************************************************\
-
-   Function: class_namet::function_name
-
-    Inputs:
-     arg_name - Description of its purpose
-     long_arg_name - Descriptions should be indented
-                     to match the first line of the
-                     description
-
-    Outputs: A description of what the function returns
-
-    Purpose: A description of what the function does.
-             Again, indentation with the line above
-
-   \*******************************************************************/
-   ```
-- An empty line should appear between the bottom of the function comment header
-  and the function.
-- Put comments on a separate line
-- Use comments to explain the non-obvious
-- Use #if 0 for commenting out source code
-- Use #ifdef DEBUG to guard debug code
-
-Naming:
-- Identifiers may use the characters [a-z0-9_] and should start with a
-  lower-case letter (parameters in constructors may start with _).
-- Use american spelling for identifiers.
-- Separate basic words by _
-- Avoid abbreviations (e.g. prefer symbol_table to of st).
-- User defined type identifiers have to be terminated by 't'. Moreover,
-  before 't' may not be '_'.
-- Do not use 'm_' prefix nor '_' suffix for names of attributes of structured
-  types.
-- Enum values may use the characters [A-Z0-9_]
-
-Header files:
-- Avoid unnecessary #includes, especially in header files
-- Prefer forward declaration to includes, but forward declare at the top
-  of the header file rather than in line
-- Guard headers with #ifndef CPROVER_DIRECTORIES_FILE_H, etc
-
-Make files
-- Each source file should appear on a separate line
-- The final source file should still be followed by a trailing slash
-- The last line should be a comment to not be deleted, i.e. should look like:
-```
-SRC = source_file.cpp \
-      source_file2.cpp \
-      # Empty last line
-```
-- This ensures the Makefiles can be easily merged.
-
-Program Command Line Options
-- Each program contains a program_name_parse_optionst class which should
-  contain a define PROGRAM_NAME_PARSE_OPTIONS which is a string of all the
-  parse options in brackets (with a colon after the bracket if it takes a
-  parameter)
-- Each parameter should be one per line to yield easy merging
-- If parameters are shared between programs, they should be pulled out into
-  a common file and then included using a define
-- The defines should be OPT_FLAG_NAMES which should go into the OPTIONS define
-- The defines should include HELP_FLAG_NAMES which should contain the help
-  output of the format:
-  ```
-  " --flag                explanations\n" \
-  " --another flag        more explanation\n" \
-   <-------30 chars------>
-- The defines may include PARSE_OPTIONS_FLAG_NAMES which move the options
-  from the command line into the options
-
-C++ features:
-- Do not use namespaces, except for anonymous namespaces.
-- Prefer use of 'typedef' insted of 'using'.
-- Prefer use of 'class' instead of 'struct'.
-- Write type modifiers before the type specifier.
-- Make references const whenever possible
-- Make functions const whenever possible
-- Do not hide base class functions
-- You are encouraged to use override
-- Single argument constructors must be explicit
-- Avoid implicit conversions
-- Avoid friend declarations
-- Avoid iterators, use ranged for instead
-- Avoid allocation with new/delete, use unique_ptr
-- Avoid pointers, use references
-- Avoid char *, use std::string
-- For numbers, use int, unsigned, long, unsigned long, double
-- Use mp_integer, not BigInt
-- Use the functions in util for conversions between numbers and strings
-- Avoid C-style functions. Use classes with an operator() instead.
-- Use irep_idt for identifiers (not std::string)
-- Avoid destructive updates if possible. The irept has constant time copy.
-- Use instances of std::size_t for comparison with return values of .size() of
-  STL containers and algorithms, and use them as indices to arrays or vectors.
-- Do not use default values in public functions
-- Use assertions to detect programming errors, e.g. whenever you make
-  assumptions on how your code is used
-- Use exceptions only when the execution of the program has to abort
-  because of erroneous user input
-- We allow to use 3rd-party libraries directly.
-  No wrapper matching the coding rules is required.
-  Allowed libraries are: STL.
-- When throwing, omit the brackets, i.e. `throw "error"`.
-- Error messages should start with a lower case letter.
-- Use the auto keyword if and only if one of the following
-  - The type is explictly repeated on the RHS (e.g. a constructor call)
-  - Adding the type will increase confusion (e.g. iterators, function pointers)
-- Avoid assert, if the condition is an actual invariant, use INVARIANT,
-  PRECONDITION, POSTCONDITION, CHECK_RETURN, UNREACHABLE or DATA_INVARIANT.
-  If there are possible reasons why it might fail, throw an exception.
-
-Architecture-specific code:
-- Avoid if possible.
-- Use __LINUX__, __MACH__, and _WIN32 to distinguish the architectures.
-- Don't include architecture-specific header files without #ifdef ...
-
-Output:
-- Do not output to cout or cerr directly (except in temporary debug code,
-  and then guard #include <iostream> by #ifdef DEBUG)
-- Derive from messaget if the class produces output and use the streams provided
-  (status(), error(), debug(), etc)
-- Use '\n' instead of std::endl
-
-Unit tests:
- - Unit tests are written using Catch: https://github.com/philsquared/Catch/
- - For large classes:
-    - Create a separate file that contains the tests for each method of each
-      class
-    - The file should be named according to
-      `unit/class/path/class_name/function_name.cpp`
- - For small classes:
-    - Create a separate file that contains the tests for all methods of each
-      class
-    - The file should be named according to unit/class/path/class_name.cpp
- - Catch supports tagging, tests should be tagged with all the following tags:
-    - [core] should be used for all tests unless the test takes more than 1
-      second to run, then it should be tagged with [long]
-    - [folder_name] of the file being tested
-    - [class_name] of the class being tested
-    - [function_name] of the function being tested
-
-You are allowed to break rules if you have a good reason to do so.
-
-Pre-commit hook to run cpplint locally
---------------------------------------
-To install the hook
-cp .githooks/pre-commit .git/hooks/pre-commit
-or use a symbolic link.
-Then, when running git commit, you should get the linter output
-(if any) before being prompted to enter a commit message.
-To bypass the check (e.g. if there was a false positive),
-add the option --no-verify.

CODING_STANDARD.md

@@ -0,0 +1,228 @@
+Here a few minimalistic coding rules for the CPROVER source tree.
+
+# Whitespaces
+- Use 2 spaces indent, no tabs.
+- No lines wider than 80 chars.
+  - When line is wider, do the following:
+    - Subsequent lines should be indented two more than the initial line
+    - Break after `=` if it is part of an assignment
+      - For chained calls, prefer immediately before `.`
+    - For other operators (e.g. `&&`, `+`) prefer immediately after the
+      operator
+    - For brackets, break after the bracket
+      - In the case of function calls, put each argument on a separate line if
+        they do not fit after one line break
+      - Nested function calls do not need to be broken up into separate lines
+        even if the outer function call does.
+- If a method is bigger than 50 lines, break it into parts.
+- Put matching `{ }` into the same column.
+- No spaces around operators (`=`, `+`, `==` ...) Exceptions: Spaces around
+  `&&`, `||` and `<<`
+- Space after comma (parameter lists, argument lists, ...)
+- Space after colon inside `for`
+- For pointers and references, the `*`/`&` should be attached to the variable
+  name as opposed to the type. E.g. for a pointer to an int the syntax would
+  be: `int *x;`
+- No whitespaces at end of line
+- No whitespaces in blank lines
+- Put argument lists on next line (and indent 2 spaces) if too long
+- Put parameters on separate lines (and indent 2 spaces) if too long
+- No whitespaces around colon for inheritance, put inherited into separate
+  lines in case of multiple inheritance
+- The initializer list follows the constructor without a whitespace around the
+  colon. Break line after the colon if required and indent members.
+- `if(...)`, `else`, `for(...)`, `do`, and `while(...)` are always in a
+  separate line
+- Break expressions in `if`, `for`, `while` if necessary and align them with
+  the first character following the opening parenthesis
+- Use `{}` instead of `;` for the empty statement
+- Single line blocks without `{ }` are allowed, but put braces around
+  multi-line blocks
+- Use blank lines to visually separate logically cohesive code blocks within a
+  function
+- Have a newline at the end of a file
+
+# Comments
+- Do not use `/* */`
+- Each source and header file must start with a comment block stating the
+  author. See existing source for an example of the format of this block. This
+  should be followed by a Doxygen `\file` comment:
+  ```c++
+  /// \file
+  /// <Some information about this file goes here>
+  ```
+  Note that the `\file` tag must be immediately followed by a newline in order
+  for Doxygen to relate the comment to the current file.
+- Each function should be preceded by a Doxygen comment describing that
+  function. The format should match the [LLVM
+  guidelines](http://llvm.org/docs/CodingStandards.html#doxygen-use-in-documentation-comments),
+  with one extension: `\param` and `\return` comments longer than a single line
+  should have subsequent lines indented by two spaces, so that the tags stand
+  out. An example:
+  ```c++
+  /// This sentence, until the first dot followed by whitespace, becomes
+  /// the brief description. More detailed text follows. Feel free to
+  /// break this into paragraphs to aid readability.
+  /// \param arg_name: This parameter doesn't need much description
+  /// \param [out] long_arg_name: This parameter is mutated by the function.
+  ///   Extra info about the parameter gets indented an extra two columns,
+  ///   like this.
+  /// \return The return value is literally the value returned by the
+  ///   function. For out-parameters, use "\param [out]".
+  return_typet my_function(argt arg_name, argt &long_arg_name)
+  ```
+- The priority of documentation is readability. Therefore, feel free to use
+  Doxygen features, or to add whitespace for multi-paragraph comment blocks if
+  necessary.
+- A comment block should immediately precede the definition of the entity it
+  documents, which will generally mean that it will live in the source file.
+  This allows us to take advantage of the one definition rule. If each entity
+  is defined only once, then it is also documented only once.
+- The documentation block must *immediately* precede the entity it documents.
+  Don't insert empty lines between docs and functions, because this will
+  confuse Doxygen.
+- Put comments on a separate line
+- Use comments to explain the non-obvious
+- Use #if 0 for commenting out source code
+- Use #ifdef DEBUG to guard debug code
+
+# Naming
+- Identifiers may use the characters `[a-z0-9_]` and should start with a
+  lower-case letter (parameters in constructors may start with `_`).
+- Use American spelling for identifiers.
+- Separate basic words by `_`
+- Avoid abbreviations (e.g. prefer `symbol_table` to `st`).
+- User defined type identifiers have to be terminated by `t`. Moreover, before
+  `t` may not be `_`.
+- Do not use `m_` prefix nor `_` suffix for names of attributes of structured
+  types.
+- Enum values may use the characters `[A-Z0-9_]`
+
+# Header files
+- Avoid unnecessary `#include`s, especially in header files
+- Prefer forward declaration to includes, but forward declare at the top of the
+  header file rather than in line
+- Guard headers with `#ifndef CPROVER_DIRECTORIES_FILE_H`, etc
+- The corresponding header for a given source file should always be the *first*
+  include in the source file. For example, given `foo.h` and `foo.cpp`, the
+  line `#include "foo.h"` should precede all other include statements in
+  `foo.cpp`.
+
+# Makefiles
+- Each source file should appear on a separate line
+- The final source file should still be followed by a trailing slash
+- The last line should be a comment to not be deleted, i.e. should look like:
+  ```makefile
+  SRC = source_file.cpp \
+        source_file2.cpp \
+        # Empty last line
+  ```
+  This ensures the Makefiles can be easily merged.
+
+# Program Command Line Options
+- Each program contains a `program_name_parse_optionst` class which should
+  contain a define `PROGRAM_NAME_PARSE_OPTIONS` which is a string of all the
+  parse options in brackets (with a colon after the bracket if it takes a
+  parameter)
+- Each parameter should be one per line to yield easy merging
+- If parameters are shared between programs, they should be pulled out into a
+  common file and then included using a define
+- The defines should be `OPT_FLAG_NAMES` which should go into the `OPTIONS`
+  define
+- The defines should include `HELP_FLAG_NAMES` which should contain the help
+  output in the format:
+  ```
+  " --flag                explanations\n" \
+  " --another flag        more explanation\n" \
+   <-------30 chars------>
+  ```
+- The defines may include `PARSE_OPTIONS_FLAG_NAMES` which move the options
+  from the command line into the options
+
+# C++ features
+- Do not use namespaces, except for anonymous namespaces.
+- Prefer use of `typedef` instead of `using`.
+- Prefer use of `class` instead of `struct`.
+- Write type modifiers before the type specifier.
+- Make references `const` whenever possible
+- Make member functions `const` whenever possible
+- Do not hide base class functions
+- You are encouraged to use `override`
+- Single argument constructors must be `explicit`
+- Avoid implicit conversions
+- Avoid `friend` declarations
+- Avoid iterators, use ranged `for` instead
+- Avoid allocation with `new`/`delete`, use `unique_ptr`
+- Avoid pointers, use references
+- Avoid `char *`, use `std::string`
+- For numbers, use `int`, `unsigned`, `long`, `unsigned long`, `double`
+- Use `mp_integer`, not `BigInt`
+- Use the functions in util for conversions between numbers and strings
+- Avoid C-style functions. Use classes with an `operator()` instead.
+- Use `irep_idt` for identifiers (not `std::string`)
+- Avoid destructive updates if possible. The `irept` has constant time copy.
+- Use instances of `std::size_t` for comparison with return values of `.size()`
+  of STL containers and algorithms, and use them as indices to arrays or
+  vectors.
+- Do not use default values in public functions
+- Use assertions to detect programming errors, e.g. whenever you make
+  assumptions on how your code is used
+- Use exceptions only when the execution of the program has to abort because of
+  erroneous user input
+- We allow to use 3rd-party libraries directly. No wrapper matching the coding
+  rules is required. Allowed libraries are: STL.
+- When throwing, omit the brackets, i.e. `throw "error"`.
+- Error messages should start with a lower case letter.
+- Use the `auto` keyword if and only if one of the following
+  - The type is explicitly repeated on the RHS (e.g. a constructor call)
+  - Adding the type will increase confusion (e.g. iterators, function pointers)
+- Avoid `assert`. If the condition is an actual invariant, use INVARIANT,
+  PRECONDITION, POSTCONDITION, CHECK_RETURN, UNREACHABLE or DATA_INVARIANT. If
+  there are possible reasons why it might fail, throw an exception.
+
+# Architecture-specific code
+- Avoid if possible.
+- Use `__LINUX__`, `__MACH__`, and `_WIN32` to distinguish the architectures.
+- Don't include architecture-specific header files without `#ifdef` ...
+
+# Output
+- Do not output to `cout` or `cerr` directly (except in temporary debug code,
+  and then guard `#include <iostream>` by `#ifdef DEBUG`)
+- Derive from `messaget` if the class produces output and use the streams
+  provided (`status()`, `error()`, `debug()`, etc)
+- Use `\n` instead of `std::endl`
+
+# Unit tests
+- Unit tests are written using [Catch](https://github.com/philsquared/Catch)
+- For large classes:
+  - Create a separate file that contains the tests for each method of each
+    class
+  - The file should be named according to
+    `unit/class/path/class_name/function_name.cpp`
+- For small classes:
+  - Create a separate file that contains the tests for all methods of each
+    class
+  - The file should be named according to `unit/class/path/class_name.cpp`
+- Catch supports tagging, tests should be tagged with all the following tags:
+  - [core] should be used for all tests unless the test takes more than 1
+    second to run, then it should be tagged with [long]
+  - [folder_name] of the file being tested
+  - [class_name] of the class being tested
+  - [function_name] of the function being tested
+
+---
+
+You are allowed to break rules if you have a good reason to do so.
+
+---
+
+# Pre-commit hook to run cpplint locally
+
+To install the hook
+```sh
+cp .githooks/pre-commit .git/hooks/pre-commit
+```
+or use a symbolic link. Then, when running git commit, you should get the
+linter output (if any) before being prompted to enter a commit message. To
+bypass the check (e.g. if there was a false positive), add the option
+`--no-verify`.

doc/CPPLINT.cfg

@@ -0,0 +1 @@
+exclude_files=.*

doc/architectural/cbmc-guide.md

@@ -0,0 +1,601 @@
+\ingroup module_hidden
+\page cbmc-guide CBMC Guide
+
+\author Martin Brain
+
+Background Information
+======================
+
+First off; read the \ref cprover-manual "CProver Manual". It describes
+how to get, build and use CBMC and SATABS. This document covers the
+internals of the system and how to get started on development.
+
+Documentation
+-------------
+
+Apart from the (user-orientated) CPROVER manual and this document, most
+of the rest of the documentation is inline in the code as `doxygen` and
+some comments. A man page for CBMC, goto-cc and goto-instrument is
+contained in the `doc/` directory and gives some options for these
+tools. All of these could be improved and patches are very welcome. In
+some cases the algorithms used are described in the relevant papers.
+
+Architecture
+------------
+
+CPROVER is structured in a similar fashion to a compiler. It has
+language specific front-ends which perform limited syntactic analysis
+and then convert to an intermediate format. The intermediate format can
+be output to files (this is what `goto-cc` does) and are (informally)
+referred to as “goto binaries” or “goto programs”. The back-end are
+tools process this format, either directly from the front-end or from
+it’s saved output. These include a wide range of analysis and
+transformation tools (see Section \[section:other-apps\]).
+
+Coding Standards
+----------------
+
+CPROVER is written in a fairly minimalist subset of C++; templates and
+meta-programming are avoided except where necessary. The standard
+library is used but in many cases there are alternatives provided in
+`util/` (see Section \[section:util\]) which are preferred.  Boost is
+not used.
+
+Patches should be formatted so that code is indented with two space
+characters, not tab and wrapped to 75 or 72 columns. Headers for doxygen
+should be given (and preferably filled!) and the author will be the
+person who first created the file.
+
+Identifiers should be lower case with underscores to separate words.
+Types (classes, structures and typedefs) names must[^1] end with a `t`.
+Types that model types (i.e. C types in the program that is being
+interpreted) are named with `_typet`. For example `ui_message_handlert`
+rather than `UI_message_handlert` or `UIMessageHandler` and
+`union_typet`.
+
+How to Contribute
+-----------------
+
+Fixes, changes and enhancements to the CPROVER code base should be
+developed against the `trunk` version and submitted to Daniel as patches
+produced by `diff -Naur` or `svn diff`. Entire applications are best
+developed independently (`git svn` is a popular choice for tracking the
+main trunk but also having local development) until it is clear what
+their utility, future and maintenance is likely to be.
+
+Other Useful Code {#section:other-apps}
+-----------------
+
+The CPROVER subversion archive contains a number of separate programs.
+Others are developed separately as patches or separate
+branches.Interfaces are have been and are continuing to stablise but
+older code may require work to compile and function correctly.
+
+In the main archive:
+
+* `CBMC`:   A bounded model checking tool for C and C++. See Section
+  \[section:CBMC\].
+
+* `goto-cc`:   A drop-in, flag compatible replacement for GCC and other
+  compilers that produces goto-programs rather than executable binaries.
+  See Section \[section:goto-cc\].
+
+* `goto-instrument`:   A collection of functions for instrumenting and
+  modifying goto-programs. See Section \[section:goto-instrument\].
+
+Model checkers and similar tools:
+
+* `SatABS`:   A CEGAR model checker using predicate abstraction. Is
+  roughly 10,000 lines of code (on top of the CPROVER code base) and is
+  developed in its own subversion archive. It uses an external model
+  checker to find potentially feasible paths. Key limitations are
+  related to code with pointers and there is scope for significant
+  improvement.
+
+* `Scratch`:   Alistair Donaldson’s k-induction based tool. The
+  front-end is in the old project CVS and some of the functionality is
+  in `goto-instrument`.
+
+* `Wolverine`:   An implementation of Ken McMillan’s IMPACT algorithm
+  for sequential programs. In the old project CVS.
+
+* `C-Impact`:   An implementation of Ken McMillan’s IMPACT algorithm for
+  parallel programs. In the old project CVS.
+
+* `LoopFrog`:   A loop summarisation tool.
+
+* `???`:   Christoph’s termination analyser.
+
+Test case generation:
+
+* `cover`:   A basic test-input generation tool. In the old
+    project CVS.
+
+* `FShell`:   A test-input generation tool that allows the user to
+  specify the desired coverage using a custom language (which includes
+  regular expressions over paths). It uses incremental SAT and is thus
+  faster than the naïve “add assertions one at a time and use the
+  counter-examples” approach. Is developed in its own subversion.
+
+Alternative front-ends and input translators:
+
+* `Scoot`:   A System-C to C translator. Probably in the old
+    project CVS.
+
+* `???`:   A Simulink to C translator. In the old project CVS.
+
+* `???`:   A Verilog front-end. In the old project CVS.
+
+* `???`:   A converter from Codewarrior project files to Makefiles. In
+    the old project CVS.
+
+Other tools:
+
+* `ai`:   Leo’s hybrid abstract interpretation / CEGAR tool.
+
+* `DeltaCheck?`:   Ajitha’s slicing tool, aimed at locating changes and
+  differential verification. In the old project CVS.
+
+There are tools based on the CPROVER framework from other research
+groups which are not listed here.
+
+Source Walkthrough
+==================
+
+This section walks through the code bases in a rough order of interest /
+comprehensibility to the new developer.
+
+`doc`
+-----
+
+At the moment just contains the CBMC man page.
+
+`regression/`
+-------------
+
+The regression tests are currently being moved from CVS. The
+`regression/` directory contains all of those that have
+been moved. They are grouped into directories for each of the tools.
+Each of these contains a directory per test case, containing a C or C++
+file that triggers the bug and a `.dsc` file that describes
+the tests, expected output and so on. There is a Perl script,
+`test.pl` that is used to invoke the tests as:
+
+    ../test.pl -c PATH_TO_CBMC
+
+The `–help` option gives instructions for use and the
+format of the description files.
+
+`src/`
+------
+
+The source code is divided into a number of sub-directories, each
+containing the code for a different part of the system. In the top level
+files there are only a few files:
+
+* `config.inc`:   The user-editable configuration parameters for the
+  build process. The main use of this file is setting the paths for the
+  various external SAT solvers that are used. As such, anyone building
+  from source will likely need to edit this.
+
+* `Makefile`:   The main systems Make file. Parallel builds are
+  supported and encouraged; please don’t break them!
+
+* `common`:   System specific magic required to get the system to build.
+  This should only need to be edited if porting CBMC to a new platform /
+  build environment.
+
+* `doxygen.cfg`:   The config file for doxygen.cfg
+
+### `util/` {#section:util}
+
+`util/` contains the low-level data structures and
+manipulation functions that are used through-out the CPROVER code-base.
+For almost any low-level task, the code required is probably in
+`util/`. Key files include:
+
+* `irep.h`:   This contains the definition of `irept`, the basis of many
+  of the data structures in the project. They should not be used
+  directly; one of the derived classes should be used. For more
+  information see Section \[section:irept\].
+
+* `expr.h`:   The parent class for all of the expressions. Provides a
+  number of generic functions, `exprt` can be used with these but when
+  creating data, subclasses of `exprt` should be used.
+
+* `std_expr.h`:   Provides subclasses of `exprt` for common kinds of
+  expression for example `plus_exprt`, `minus_exprt`,
+  `dereference_exprt`. These are the intended interface for creating
+  expressions.
+
+* `std_types.h`:   Provides subclasses of `typet` (a subclass of
+  `irept`) to model C and C++ types. This is one of the preferred
+  interfaces to `irept`. The front-ends handle type promotion and most
+  coercision so the type system and checking goto-programs is simpler
+  than C.
+
+* `dstring.h`:   The CPROVER string class. This enables sharing between
+  strings which significantly reduces the amount of memory required and
+  speeds comparison. `dstring` should not be used directly, `irep_idt`
+  should be used instead, which (dependent on build options) is an alias
+  for `dstring`.
+
+* `mp_arith.h`:   The wrapper class for multi-precision arithmetic
+  within CPROVER. Also see `arith_tools.h`.
+
+* `ieee_float.h`:   The arbitrary precision float model used within
+  CPROVER. Based on `mp_integer`s.
+
+* `context.h`:   A generic container for symbol table like constructs
+  such as namespaces. Lookup gives type, location of declaration, name,
+  ‘pretty name’, whether it is static or not.
+
+* `namespace.h`:   The preferred interface for the context class. The
+  key function is `lookup` which converts a string (`irep_idt`) to a
+  symbol which gives the scope of declaration, type and so on. This
+  works for functions as well as variables.
+
+### `langapi/`
+
+This contains the basic interfaces and support classes for programming
+language front ends. Developers only really need look at this if they
+are adding support for a new language. It’s main users are the two (in
+trunk) language front-ends; `ansi-c/` and
+`cpp/`.
+
+### `ansi-c/`
+
+Contains the front-end for ANSI C, plus a variety of common extensions.
+This parses the file, performs some basic sanity checks (this is one
+area in which the UI could be improved; patches most welcome) and then
+produces a goto-program (see below). The parser is a traditional Flex /
+Bison system.
+
+`internal_addition.c` contains the implementation of various ‘magic’
+functions that are that allow control of the analysis from the source
+code level. These include assertions, assumptions, atomic blocks, memory
+fences and rounding modes.
+
+The `library/` subdirectory contains versions of some of the C standard
+header files that make use of the CPROVER built-in functions. This
+allows CPROVER programs to be ‘aware’ of the functionality and model it
+correctly. Examples include `stdio.c`, `string.c`, `setjmp.c` and
+various threading interfaces.
+
+### `cpp/`
+
+This directory contains the C++ front-end. It supports the subset of C++
+commonly found in embedded and system applications. Consequentially it
+doesn’t have full support for templates and many of the more advanced
+and obscure C++ features. The subset of the language that can be handled
+is being extended over time so bug reports of programs that cannot be
+parsed are useful.
+
+The functionality is very similar to the ANSI C front end; parsing the
+code and converting to goto-programs. It makes use of code from
+`langapi` and `ansi-c`.
+
+### `goto-programs/`
+
+Goto programs are the intermediate representation of the CPROVER tool
+chain. They are language independent and similar to many of the compiler
+intermediate languages. Section \[section:goto-programs\] describes the
+`goto_programt` and `goto_functionst` data structures in detail. However
+it useful to understand some of the basic concepts. Each function is a
+list of instructions, each of which has a type (one of 18 kinds of
+instruction), a code expression, a guard expression and potentially some
+targets for the next instruction. They are not natively in static
+single-assign (SSA) form. Transitions are nondeterministic (although in
+practise the guards on the transitions normally cover form a disjoint
+cover of all possibilities). Local variables have non-deterministic
+values if they are not initialised.  Variables and data within the
+program is commonly one of three types (parameterised by width):
+`unsignedbv_typet`, `signedbv_typet` and `floatbv_typet`, see
+`util/std_types.h` for more information. Goto programs can be serialised
+in a binary (wrapped in ELF headers) format or in XML (see the various
+`_serialization` files).
+
+The `cbmc` option `–show-goto-programs` is often a good starting point
+as it outputs goto-programs in a human readable form. However there are
+a few things to be aware of. Functions have an internal name (for
+example `c::f00`) and a ‘pretty name’ (for example `f00`) and which is
+used depends on whether it is internal or being presented to the user.
+The `main` method is the ‘logical’ main which is not necessarily the
+main method from the code. In the output `NONDET` is use to represent a
+nondeterministic assignment to a variable. Likewise `IF` as a beautified
+`GOTO` instruction where the guard expression is used as the condition.
+`RETURN` instructions may be dropped if they precede an `END_FUNCTION`
+instruction. The comment lines are generated from the `locationt` field
+of the `instructiont` structure.
+
+`goto-programs/` is one of the few places in the CPROVER codebase that
+templates are used. The intention is to allow the general architecture
+of program and functions to be used for other formalisms.  At the moment
+most of the templates have a single instantiation; for example
+`goto_functionst` and `goto_function_templatet` and `goto_programt` and
+`goto_program_templatet`.
+
+### `goto-symex/`
+
+This directory contains a symbolic evaluation system for goto-programs.
+This takes a goto-program and translates it to an equation system by
+traversing the program, branching and merging and unwinding loops as
+needed. Each reverse goto has a separate counter (the actual counting is
+handled by `cbmc`, see the `–unwind` and `–unwind-set` options). When a
+counter limit is reach, an assertion can be added to explicitly show
+when analysis is incomplete.  The symbolic execution includes constant
+folding so loops that have a constant number of iterations will be
+handled completely (assuming the unwinding limit is sufficient).
+
+The output of the symbolic execution is a system of equations; an object
+containing a list of `symex_target_elements`, each of which are
+equalities between `expr` expressions. See `symex_target_equation.h`.
+The output is in static, single assignment (SSA) form, which is *not*
+the case for goto-programs.
+
+### `pointer-analysis/`
+
+To perform symbolic execution on programs with dereferencing of
+arbitrary pointers, some alias analysis is needed.  `pointer-analysis`
+contains the three levels of analysis; flow and context insensitive,
+context sensitive and flow and context sensitive. The code needed is
+subtle and sophisticated and thus there may be bugs.
+
+### `solvers/`
+
+The `solvers/` directory contains interfaces to a number of
+different decision procedures, roughly one per directory.
+
+* prop/:   The basic and common functionality. The key file is
+  `prop_conv.h` which defines `prop_convt`.  This is the base class that
+  is used to interface to the decision procedures. The key functions are
+  `convert` which takes an `exprt` and converts it to the appropriate,
+  solver specific, data structures and `dec_solve` (inherited from
+  `decision_proceduret`) which invokes the actual decision procedures.
+  Individual decision procedures (named `*_dect`) objects can be created
+  but `prop_convt` is the preferred interface for code that uses them.
+
+* flattening/:   A library that converts operations to bit-vectors,
+  including calling the conversions in `floatbv` as necessary. Is
+  implemented as a simple conversion (with caching) and then a
+  post-processing function that adds extra constraints. This is not used
+  by the SMT or CVC back-ends.
+
+* dplib/:   Provides the `dplib_dect` object which used the decision
+  procedure library from “Decision Procedures : An Algorithmic Point of
+  View”.
+
+* cvc/:   Provides the `cvc_dect` type which interfaces to the old (pre
+  SMTLib) input format for the CVC family of solvers.  This format is
+  still supported by depreciated in favour of SMTLib 2.
+
+* smt1/:   Provides the `smt1_dect` type which converts the formulae to
+  SMTLib version 1 and then invokes one of Boolector, CVC3, OpenSMT,
+  Yices, MathSAT or Z3. Again, note that this format is depreciated.
+
+* smt2/:   Provides the `smt2_dect` type which functions in a similar
+  way to `smt1_dect`, calling Boolector, CVC3, MathSAT, Yices or Z3.
+  Note that the interaction with the solver is batched and uses
+  temporary files rather than using the interactive command supported by
+  SMTLib 2. With the `–fpa` option, this output mode will not flatten
+  the floating point arithmetic and instead output the proposed SMTLib
+  floating point standard.
+
+* qbf/:   Back-ends for a variety of QBF solvers. Appears to be no
+  longer used or maintained.
+
+* sat/:   Back-ends for a variety of SAT solvers and DIMACS output.
+
+### `cbmc/` {#section:CBMC}
+
+This contains the first full application. CBMC is a bounded model
+checker that uses the front ends (`ansi-c`, `cpp`, goto-program or
+others) to create a goto-program, `goto-symex` to unwind the loops the
+given number of times and to produce and equation system and finally
+`solvers` to find a counter-example (technically, `goto-symex` is then
+used to construct the counter-example trace).
+
+### `goto-cc/` {#section:goto-cc}
+
+`goto-cc` is a compiler replacement that just performs the first step of
+the process; converting C or C++ programs to goto-binaries. It is
+intended to be dropped in to an existing build procedure in place of the
+compiler, thus it emulates flags that would affect the semantics of the
+code produced. Which set of flags are emulated depends on the naming of
+the `goto-cc/` binary. If it is called `goto-cc` then it emulates GCC
+flags, `goto-armcc` emulates the ARM compiler, `goto-cl` emulates VCC
+and `goto-cw` emulates the Code Warrior compiler. The output of this
+tool can then be used with `cbmc` or `goto-instrument`.
+
+### `goto-instrument/` {#section:goto-instrument}
+
+The `goto-instrument/` directory contains a number of tools, one per
+file, that are built into the `goto-instrument` program. All of them
+take in a goto-program (produced by `goto-cc`) and either modify it or
+perform some analysis. Examples include `nondet_static.cpp` which
+initialises static variables to a non-deterministic value,
+`nondet_volatile.cpp` which assigns a non-deterministic value to any
+volatile variable before it is read and `weak_memory.h` which performs
+the necessary transformations to reason about weak memory models. The
+exception to the “one file for each piece of functionality” rule are the
+program instrumentation options (mostly those given as “Safety checks”
+in the `goto-instrument` help text) which are included in the
+`goto-program/` directory. An example of this is
+`goto-program/stack_depth.h` and the general rule seems to be that
+transformations and instrumentation that `cbmc` uses should be in
+`goto-program/`, others should be in `goto-instrument`.
+
+`goto-instrument` is a very good template for new analysis tools. New
+developers are advised to copy the directory, remove all files apart
+from `main.*`, `parseoptions.*` and the `Makefile` and use these as the
+skeleton of their application. The `doit()` method in `parseoptions.cpp`
+is the preferred location for the top level control for the program.
+
+### `linking/`
+
+Probably the code to emulate a linker. This allows multiple ‘object
+files’ (goto-programs) to be linked into one ‘executable’ (another
+goto-program), thus allowing existing build systems to be used to build
+complete goto-program binaries.
+
+### `big-int/`
+
+CPROVER is distributed with its own multi-precision arithmetic library;
+mainly for historical and portability reasons. The library is externally
+developed and thus `big-int` contains the source as it is distributed.
+This should not be used directly, see `util/mp_arith.h` for the CPROVER
+interface.
+
+### `xmllang/`
+
+CPROVER has optional XML output for results and there is an XML format
+for goto-programs. It is used to interface to various IDEs. The
+`xmllang/` directory contains the parser and helper functions for
+handling this format.
+
+### `floatbv/`
+
+This library contains the code that is used to convert floating point
+variables (`floatbv`) to bit vectors (`bv`).  This is referred to as
+‘bit-blasting’ and is called in the `solver` code during conversion to
+SAT or SMT. It also contains the abstraction code described in the
+FMCAD09 paper.
+
+Data Structures
+===============
+
+This section discusses some of the key data-structures used in the
+CPROVER codebase.
+
+`irept` {#section:irept}
+------------------------
+
+There are a large number of kind of tree structured or tree-like data in
+CPROVER. `irept` provides a single, unified representation for all of
+these, allowing structure sharing and reference counting of data. As
+such `irept` is the basic unit of data in CPROVER.  Each `irept`
+contains[^2] a basic unit of data (of type `dt`) which contains four
+things:
+
+* `data`:   A string[^3], which is returned when the `id()` function is
+  used.
+
+* `named_sub`:   A map from `irep_namet` (a string) to an `irept`. This
+  is used for named children, i.e.  subexpressions, parameters, etc.
+
+* `comments`:   Another map from `irep_namet` to `irept` which is used
+  for annotations and other ‘non-semantic’ information
+
+* `sub`:   A vector of `irept` which is used to store ordered but
+  unnamed children.
+
+The `irept::pretty` function outputs the contents of an `irept` directly
+and can be used to understand an debug problems with `irept`s.
+
+On their own `irept`s do not “mean” anything; they are effectively
+generic tree nodes. Their interpretation depends on the contents of
+result of the `id` function (the `data`) field. `util/irep_ids.txt`
+contains the complete list of `id` values. During the build process it
+is used to generate `util/irep_ids.h` which gives constants for each id
+(named `ID_`). These can then be used to identify what kind of data
+`irept` stores and thus what can be done with it.
+
+To simplify this process, there are a variety of classes that inherit
+from `irept`, roughly corresponding to the ids listed (i.e.  `ID_or`
+(the string `"or”`) corresponds to the class `or_exprt`). These give
+semantically relevant accessor functions for the data; effectively
+different APIs for the same underlying data structure. None of these
+classes add fields (only methods) and so static casting can be used. The
+inheritance graph of the subclasses of `irept` is a useful starting
+point for working out how to manipulate data.
+
+There are three main groups of classes (or APIs); those derived from
+`typet`, `codet` and `exprt` respectively. Although all of these inherit
+from `irept`, these are the most abstract level that code should handle
+data. If code is manipulating plain `irept`s then something is wrong
+with the architecture of the code.
+
+Many of the key descendent of `exprt` are declared in `std_expr.h`. All
+expressions have a named subfield / annotation which gives the type of
+the expression (slightly simplified from C/C++ as `unsignedbv_typet`,
+`signedbv_typet`, `floatbv_typet`, etc.). All type conversions are
+explicit with an expression with `id() == ID_typecast` and an ‘interface
+class’ named `typecast_exprt`. One key descendent of `exprt` is
+`symbol_exprt` which creates `irept` instances with the id of “symbol”.
+These are used to represent variables; the name of which can be found
+using the `get_identifier` accessor function.
+
+`codet` inherits from `exprt` and is defined in `std_code.h`. They
+represent executable code; statements in C rather than expressions. In
+the front-end there are versions of these that hold whole code blocks,
+but in goto-programs these have been flattened so that each `irept`
+represents one sequence point (almost one line of code / one
+semi-colon). The most common descendents of `codet` are `code_assignt`
+so a common pattern is to cast the `codet` to an assignment and then
+recurse on the expression on either side.
+
+`goto-programs` {#section:goto-programs}
+----------------------------------------
+
+The common starting point for working with goto-programs is the
+`read_goto_binary` function which populates an object of
+`goto_functionst` type. This is defined in `goto_functions.h` and is an
+instantiation of the template `goto_functions_templatet` which is
+contained in `goto_functions_template.h`. They are wrappers around a map
+from strings to `goto_programt`’s and iteration macros are provided.
+Note that `goto_function_templatet` (no `s`) is defined in the same
+header as `goto_functions_templatet` and is gives the C type for the
+function and Boolean which indicates whether the body is available
+(before linking this might not always be true). Also note the slightly
+counter-intuitive naming; `goto_functionst` instances are the top level
+structure representing the program and contain `goto_programt` instances
+which represent the individual functions. At the time of writing
+`goto_functionst` is the only instantiation of the template
+`goto_functions_templatet` but other could be produced if a different
+data-structures / kinds of models were needed for functions.
+
+`goto_programt` is also an instantiation of a template. In a similar
+fashion it is `goto_program_templatet` and allows the types of the guard
+and expression used in instructions to be parameterised. Again, this is
+currently the only use of the template. As such there are only really
+helper functions in `goto_program.h` and thus `goto_program_template.h`
+is probably the key file that describes the representation of (C)
+functions in the goto-program format. It is reasonably stable and
+reasonably documented and thus is a good place to start looking at the
+code.
+
+An instance of `goto_program_templatet` is effectively a list of
+instructions (and inner template called `instructiont`). It is important
+to use the copy and insertion functions that are provided as iterators
+are used to link instructions to their predecessors and targets and
+careless manipulation of the list could break these. Likewise there are
+helper macros for iterating over the instructions in an instance of
+`goto_program_templatet` and the use of these is good style and strongly
+encouraged.
+
+Individual instructions are instances of type `instructiont`. They
+represent one step in the function.  Each has a type, an instance of
+`goto_program_instruction_typet` which denotes what kind of instruction
+it is. They can be computational (such as `ASSIGN` or `FUNCTION_CALL`),
+logical (such as `ASSUME` and `ASSERT`) or informational (such as
+`LOCATION` and `DEAD`). At the time of writing there are 18 possible
+values for `goto_program_instruction_typet` / kinds of instruction.
+Instructions also have a guard field (the condition under which it is
+executed) and a code field (what the instruction does). These may be
+empty depending on the kind of instruction. In the default
+instantiations these are of type `exprt` and `codet` respectively and
+thus covered by the previous discussion of `irept` and its descendents.
+The next instructions (remembering that transitions are guarded by
+non-deterministic) are given by the list `targets` (with the
+corresponding list of labels `labels`) and the corresponding set of
+previous instructions is get by `incoming_edges`. Finally `instructiont`
+have informational `function` and `location` fields that indicate where
+they are in the code.
+
+[^1]: There are a couple of exceptions, including the graph classes
+
+[^2]: Or references, if reference counted data sharing is enabled. It is
+    enabled by default; see the `SHARING` macro.
+
+[^3]: When `USE_DSTRING` is enabled (it is by default), this is actually
+a `dstring` and thus an integer which is a reference into a string table

doc/architectural/front-page.md

@@ -0,0 +1,46 @@
+CProver Documentation
+=====================
+
+\author Kareem Khazem
+
+These pages contain user tutorials, automatically-generated API
+documentation, and higher-level architectural overviews for the
+CProver codebase. Users can download CProver tools from the
+<a href="http://www.cprover.org/">CProver website</a>; contributors
+should use the <a href="https://github.com/diffblue/cbmc">repository</a>
+hosted on GitHub.
+
+### For users:
+
+* The \ref cprover-manual "CProver Manual" details the capabilities of
+  CBMC and SATABS and describes how to install and use these tools. It
+  also covers the underlying theory and prerequisite concepts behind how
+  these tools work.
+
+### For contributors:
+
+* If you already know exactly what you're looking for, the API reference
+  is generated from the codebase. You can search for classes and class
+  members in the search bar at top-right or use one of the links in the
+  sidebar.
+
+* For higher-level architectural information, each of the pages under
+  the "Modules" link in the sidebar gives an overview of a directory in
+  the CProver codebase.
+
+* The \ref module_cbmc "CBMC guided tour" is a good start for new
+  contributors to CBMC. It describes the stages through which CBMC
+  transforms source files into bug reports and counterexamples, linking
+  to the relevant documentation for each stage.
+
+* The \subpage cbmc-hacking "CBMC hacking HOWTO" helps new contributors
+  to CProver to get their feet wet through a series of programming
+  exercises---mostly modifying goto-instrument, and thus learning to
+  manipulate the main data structures used within CBMC.
+
+* The \subpage cbmc-guide "CBMC guide" is a single document describing
+  the layout of the codebase and many of the important data structures.
+  It probably contains more information than the module pages at the
+  moment, but may be somewhat out-of-date.
+
+\defgroup module_hidden _hidden

doc/architectural/howto.md

@@ -0,0 +1,243 @@
+\ingroup module_hidden
+\page cbmc-hacking CBMC Hacking HOWTO
+
+\author Kareem Khazem
+
+This is an introduction to hacking on the `cprover` codebase.  It is not
+intended as a user guide to `CBMC` or related tools.  It is structured
+as a series of programming exercises that aim to acclimatise the reader
+to the basic data structures and workflow needed for contributing to
+`CBMC`.
+
+
+## Initial setup
+
+Clone the [CBMC repository][cbmc-repo] and build it:
+
+    git clone https://github.com/diffblue/cbmc.git
+    cd cbmc/src
+    make minisat2-download
+    make
+
+Ensure that [graphviz][graphviz] is installed on your system (in
+particular, you should be able to run a program called `dot`).  Install
+[Doxygen][doxygen] and generate doxygen documentation:
+
+    # In the src directory
+    doxygen doxyfile
+    # View the documentation in a web browser
+    firefox doxy/html/index.html
+
+If you've never used doxygen documentation before, get familiar with the
+layout.  Open the generated HTML page in a web browser; search for the
+class `goto_programt` in the search bar, and jump to the documentation
+for that class; and read through the copious documentation.
+
+The build writes executable programs into several of the source
+directories.  In this tutorial, we'll be using binaries inside the
+`cbmc`, `goto-instrument`, and `goto-cc` directories.  Add these
+directories to your `$PATH`:
+
+    # Assuming you cloned CBMC into ~/code
+    export PATH=~/code/cbmc/src/goto-instrument:~/code/cbmc/src/goto-cc:~/code/cbmc/src/cbmc:$PATH
+    # Add to your shell's startup configuration file so that you don't have to run that command every time.
+    echo 'export PATH=~/code/cbmc/src/goto-instrument:~/code/cbmc/src/goto-cc:~/code/cbmc/src/cbmc:$PATH' >> .bashrc
+
+Optional: install an image viewer that can read images on stdin.
+I use [feh][feh].
+
+[cbmc-repo]:  https://github.com/diffblue/cbmc/
+[doxygen]:    http://www.stack.nl/~dimitri/doxygen/
+[graphviz]:   http://www.graphviz.org/
+[feh]:        https://feh.finalrewind.org/
+
+
+
+## Whirlwind tour of the tools
+
+CBMC's code is located under the `cbmc` directory.  Even if you plan to
+contribute only to CBMC, it is important to be familiar with several
+other of cprover's auxiliary tools.
+
+
+### Compiling with `goto-cc`
+
+There should be an executable file called `goto-cc` in the `goto-cc`
+directory; make a symbolic link to it called `goto-gcc`:
+
+    cd cbmc/src/goto-cc
+    ln -s "$(pwd)/goto-cc" goto-gcc
+
+Find or write a moderately-interesting C program; we'll call it `main.c`.
+Run the following commands:
+
+    goto-gcc -o main.goto main.c
+    cc -o main.exe main.c
+
+Invoke `./main.goto` and `./main.exe` and observe that they run identically.
+The version that was compiled with `goto-gcc` is larger, though:
+
+    du -hs *.{goto,exe}
+
+Programs compiled with `goto-gcc` are mostly identical to their `clang`-
+or `gcc`-compiled counterparts, but contain additional object code in
+cprover's intermediate representation.  The intermediate representation
+is (informally) called a *goto-program*.
+
+
+### Viewing goto-programs
+
+`goto-instrument` is a Swiss army knife for viewing goto-programs and
+performing single program analyses on them.  Run the following command:
+
+    goto-instrument --show-goto-functions main.goto
+
+Many of the instructions in the goto-program intermediate representation
+are similar to their C counterparts.  `if` and `goto` statements replace
+structured programming constructs.
+
+Find or write a small C program (2 or 3 functions, each containing a few
+varied statements).  Compile it using `goto-gcc` as above into an object
+file called `main`.  If you installed `feh`, try the following command
+to dump a control-flow graph:
+
+    goto-instrument --dot main | tail -n +2 | dot -Tpng | feh -
+
+If you didn't install `feh`, you can write the diagram to the file and
+then view it:
+
+    goto-instrument --dot main | tail -n +2 | dot -Tpng > main.png
+    Now open main.png with an image viewer
+
+(the invocation of `tail` is used to filter out the first line of
+`goto-instrument` output.  If `goto-instrument` writes more or less
+debug output by the time you read this, read the output of
+`goto-instrument --dot main` and change the invocation of `tail`
+accordingly.)
+
+There are a few other views of goto-programs.  Run `goto-instrument -h`
+and try the various switches under the "Diagnosis" section.
+
+
+
+## Learning about goto-programs
+
+In this section, you will learn about the basic goto-program data
+structures.  Reading from and manipulating these data structures form
+the core of writing an analysis for CBMC.
+
+
+### First steps with `goto-instrument`
+
+<div class=memdoc>
+**Task:** Write a simple C program with a few functions, each containing
+a few statements.  Compile the program with `goto-gcc` into a binary
+called `main`.
+</div>
+
+
+The entry point of `goto-instrument` is in `goto_instrument_main.cpp`.
+Follow the control flow into `goto_instrument_parse_optionst::doit()`, located in `goto_instrument_parse_options.cpp`.
+At some point in that function, there will be a long sequence of `if` statements.
+
+<div class=memdoc>
+**Task:** Add a `--greet` switch to `goto-instrument`, taking an optional
+argument, with the following behaviour:
+
+    $ goto-instrument --greet main
+    hello, world!
+    $ goto-instrument --greet Leperina main
+    hello, Leperina!
+
+You will also need to add the `greet` option to the
+`goto_instrument_parse_options.h` file in order for this to work.
+Notice that in the `.h` file, options that take an argument are followed
+by a colon (like `(property):`), while simple switches have no colon.
+Make sure that you `return 0;` after printing the message.
+</div>
+
+The idea behind `goto-instrument` is that it parses a goto-program and
+then performs one single analysis on that goto-program, and then
+returns.  Each of the switches in  `doit` function of
+`goto_instrument_parse_options` does something different with the
+goto-program that was supplied on the command line.
+
+
+### Goto-program basics
+
+At this point in `goto-instrument_parse_options` (where the `if`
+statements are), the goto-program will have been loaded into the object
+`goto_functions`, of type `goto_functionst`.  This has a field called
+`function_map`, a map from function names to functions.
+
+
+<div class="memdoc">
+**Task:** Add a `--print-function-names` switch to `goto-instrument`
+that prints out the name of every function in the goto-binary.  Are
+there any functions that you didn't expect to see?
+</div>
+
+The following is quite difficult to follow from doxygen, but: the value
+type of `function_map` is `goto_function_templatet<goto_programt>`.
+
+
+<div class=memdoc>
+**Task:** Read the documentation for `goto_function_templatet<bodyT>`
+and `goto_programt`.
+</div>
+
+Each goto_programt object contains a list of
+\ref goto_program_templatet::instructiont called
+`instructions`.  Each instruction has a field called `code`, which has
+type \ref codet.
+
+<div class=memdoc>
+**Task:** Add a `--pretty-program` switch to `goto-instrument`.  This
+switch should use the `codet::pretty()` function to pretty-print every
+\ref codet in the entire program.  The strings that `pretty()` generates
+for a codet look like this:
+
+    index
+      * type: unsignedbv
+          * width: 8
+          * #c_type: char
+      0: symbol
+          * type: array
+              * size: nil
+                  * type: 
+              * #source_location: 
+                * file: src/main.c
+                * line: 18
+                * function: 
+                * working_directory: /some/dir
+              0: unsignedbv
+                  * width: 8
+                  * #c_type: char
+    ...
+</div>
+
+The sub-nodes of a particular node in the pretty representation are
+numbered, starting from 0.  They can be accessed through the `op0()`,
+`op1()` and `op2()` methods in the `exprt` class.
+
+Every node in the pretty representation has an identifier, accessed
+through the `id()` function.  The file `util/irep_ids.def` lists the
+possible values of these identifiers; have a quick scan through that
+file.  In the pretty representation above, the following facts are true
+of that particular node:
+
+  - `node.id() == ID_index`
+  - `node.type().id() == ID_unsignedbv`
+  - `node.op0().id() == ID_symbol`
+  - `node.op0().type().id() == ID_array`
+
+The fact that the `op0()` child has a `symbol` ID menas that you could
+cast it to a `symbol_exprt` (which is a subtype of `exprt`) using the
+function `to_symbol_expr`.
+
+<div class=memdoc>
+**Task:** Add flags to `goto-instrument` to print out the following information:
+* the name of every function that is *called* in the program;
+* the value of every constant in the program;
+* the value of every symbol in the program.
+</div>

doc/guide/CBMC-guide.tex

@@ -1,714 +0,0 @@
-\documentclass{article}
-
-\newcommand{\dir}[1]{\texttt{#1}}
-\newcommand{\file}[1]{\texttt{#1}}
-\newcommand{\code}[1]{\texttt{#1}}
-\newcommand{\prog}[1]{\texttt{#1}}
-
-\title{Beginner's Guide to CPROVER}
-\author{Martin Brain\thanks{But most of the content is from Michael Tautschnig}}
-
-\begin{document}
-
-\maketitle
-
-\section{Background Information}
-
-First off; read the CPROVER manual.  It describes how to get, build
-and use CBMC and SATABS.  This document covers the internals of the
-system and how to get started on development.
-
-
-\subsection{Documentation}
-
-Apart from the (user-orientated) CPROVER manual and this document,
-most of the rest of the documentation is inline in the code
-as \texttt{doxygen} and some comments.  A man page for CBMC, goto-cc
-and goto-instrument is contained in the \dir{doc/} directory and gives
-some options for these tools.  All of these could be improved
-and patches are very welcome.  In some cases the algorithms used are
-described in the relevant papers.
-
-\subsection{Architecture}
-
-CPROVER is structured in a similar fashion to a compiler.  It has
-language specific front-ends which perform limited syntactic analysis
-and then convert to an intermediate format.  The intermediate format
-can be output to files (this is what \texttt{goto-cc} does) and are
-(informally) referred to as ``goto binaries'' or ``goto programs''.
-The back-end are tools process this format, either directly from the
-front-end or from it's saved output.  These include a wide range of
-analysis and transformation tools (see Section \ref{section:other-apps}).
-
-\subsection{Coding Standards}
-
-CPROVER is written in a fairly minimalist subset of C++; templates and
-meta-programming are avoided except where necessary.  The standard
-library is used but in many cases there are alternatives provided in
-\dir{util/} (see Section \ref{section:util}) which are preferred.
-Boost is not used.
-
-Patches should be formatted so that code is indented with two space
-characters, not tab and wrapped to 75 or 72 columns.  Headers for
-doxygen should be given (and preferably filled!) and the author will
-be the person who first created the file.
-
-Identifiers should be lower case with underscores to separate words.
-Types (classes, structures and typedefs) names must\footnote{There are
-a couple of exceptions, including the graph classes} end with a
-\code{t}.  Types that model types (i.e. C types in the program that is
-being interpreted) are named with \code{\_typet}.
-For example \code{ui\_message\_handlert} rather than
-\code{UI\_message\_handlert} or \code{UIMessageHandler} and
-\code{union\_typet}.
-
-
-
-\subsection{How to Contribute}
-
-Fixes, changes and enhancements to the CPROVER code base should be
-developed against the \texttt{trunk} version and submitted to Daniel
-as patches produced by \texttt{diff -Naur} or \texttt{svn diff}.
-Entire applications are best developed independently (\texttt{git svn}
-is a popular choice for tracking the main trunk but also having local
-development) until it is clear what their utility, future and
-maintenance is likely to be.
-
-
-\subsection{Other Useful Code}
-\label{section:other-apps}
-
-The CPROVER subversion archive contains a number of separate
-programs.  Others are developed separately as patches or separate
-branches.%  New applications are initially developed in their version
-%control system and may be merged into the main subversion system
-%depending on their utility, popularity and maintenance.
-Interfaces are have been and are continuing to stablise but older code
-may require work to compile and function correctly.
-
-In the main archive:
-
-\begin{description}
-  \item[\prog{CBMC}]{A bounded model checking tool for C and C++. See
-    Section \ref{section:CBMC}.}
-  \item[\prog{goto-cc}]{A drop-in, flag compatible replacement for GCC
-    and other compilers that produces goto-programs rather than
-    executable binaries.  See Section \ref{section:goto-cc}.}
-  \item[\prog{goto-instrument}]{A collection of functions for
-    instrumenting and modifying goto-programs.  See Section
-    \ref{section:goto-instrument}.}
-\end{description}
-
-Model checkers and similar tools:
-
-\begin{description}
-  \item[\prog{SatABS}]{A CEGAR model checker using predicate
-    abstraction.  Is roughly 10,000 lines of code (on top of the CPROVER
-    code base) and is developed in its own subversion archive.  It
-    uses an external model checker to find potentially feasible paths.
-    Key limitations are related to code with pointers and there is
-    scope for significant improvement.}
-
-  \item[\prog{Scratch}]{Alistair Donaldson's k-induction based tool.
-    The front-end is in the old project CVS and some of the
-    functionality is in \prog{goto-instrument}.}
-
-  \item[\prog{Wolverine}]{An implementation of Ken McMillan's IMPACT
-    algorithm for sequential programs.  In the old project CVS.}
-
-  \item[\prog{C-Impact}]{An implementation of Ken McMillan's IMPACT
-    algorithm for parallel programs.  In the old project CVS.}
-
-  \item[\prog{LoopFrog}]{A loop summarisation tool.}
-
-  \item[\prog{???}]{Christoph's termination analyser.}
-
-\end{description}
-
-
-Test case generation:
-
-\begin{description}
-  \item[\prog{cover}]{A basic test-input generation tool.  In the old
-    project CVS.}
-
-  \item[\prog{FShell}]{A test-input generation tool that allows the
-      user to specify the desired coverage using a custom language
-      (which includes regular expressions over paths).  It uses
-      incremental SAT and is thus faster than the na\"ive ``add
-      assertions one at a time and use the counter-examples''
-      approach.  Is developed in its own subversion.}
-\end{description}
-
-
-
-Alternative front-ends and input translators:
-
-\begin{description}
-  \item[\prog{Scoot}]{A System-C to C translator.  Probably in the old
-    project CVS.}
-  
-  \item[\prog{???}]{A Simulink to C translator.  In the old project CVS.}
-
-  \item[\prog{???}]{A Verilog front-end.  In the old project CVS.}
-
-  \item[\prog{???}]{A converter from Codewarrior project files to
-    Makefiles.  In the old project CVS.}
-\end{description}
-
-
-Other tools:
-
-\begin{description}
-  \item[\prog{ai}]{Leo's hybrid abstract interpretation / CEGAR tool.}
-
-  \item[\prog{DeltaCheck?}]{Ajitha's slicing tool, aimed at locating
-    changes and differential verification.  In the old project CVS.}
-\end{description}
-
-
-There are tools based on the CPROVER framework from other research
-groups which are not listed here.
-
-
-
-
-
-
-\section{Source Walkthrough}
-
-This section walks through the code bases in a rough order of interest
-/ comprehensibility to the new developer.
-
-
-
-\subsection{\dir{doc}}
-
-At the moment just contains the CBMC man page.
-
-\subsection{\dir{regression/}}
-
-The regression tests are currently being moved from CVS.  The
-\dir{regression/} directory contains all of those that have been
-moved.  They are grouped into directories for each of the tools.  Each
-of these contains a directory per test case, containing a C or C++
-file that triggers the bug and a \file{.dsc} file that describes the
-tests, expected output and so on.  There is a Perl script,
-\file{test.pl} that is used to invoke the tests as:
-
-\begin{center}
-  \code{../test.pl -c PATH\_TO\_CBMC}
-\end{center}
-
-The \code{--help} option gives instructions for use and the format of
-the description files.
-
-
-
-\subsection{\dir{src/}}
-
-The source code is divided into a number of sub-directories, each
-containing the code for a different part of the system.  In the top
-level files there are only a few files:
-
-\begin{description}
-  \item[\file{config.inc}]{The user-editable configuration parameters
-    for the build process.  The main use of this file is setting the
-    paths for the various external SAT solvers that are used.  As
-    such, anyone building from source will likely need to edit this.}
-  \item[\file{Makefile}]{The main systems Make file.  Parallel builds
-    are supported and encouraged; please don't break them!}
-  \item[\file{common}]{System specific magic required to get the
-    system to build.  This should only need to be edited if porting
-    CBMC to a new platform / build environment.}
-  \item[\file{doxygen.cfg}]{The config file for doxygen.cfg}
-\end{description}
-
-
-
-\subsubsection{\dir{util/}}
-\label{section:util}
-
-\dir{util/} contains the low-level data structures and manipulation
-functions that are used through-out the CPROVER code-base.  For almost
-any low-level task, the code required is probably in \dir{util/}.  Key
-files include:
-
-\begin{description}
-  \item[\file{irep.h}]{This contains the definition of \code{irept},
-    the basis of many of the data structures in the project.  They
-    should not be used directly; one of the derived classes should be
-    used.  For more information see Section \ref{section:irept}.}
-  \item[\file{expr.h}]{The parent class for all of the expressions.
-    Provides a number of generic functions, \code{exprt} can be used
-    with these but when creating data, subclasses of \code{exprt}
-    should be used.}
-  \item[\file{std\_expr.h}]{Provides subclasses of \code{exprt} for
-    common kinds of expression for example \code{plus\_exprt},
-    \code{minus\_exprt}, \code{dereference\_exprt}.  These are the
-    intended interface for creating expressions.}
-  \item[\file{std\_types.h}]{Provides subclasses of \code{typet} (a
-    subclass of \code{irept}) to model C and C++ types.  This is one
-    of the preferred interfaces to \code{irept}.  The front-ends handle
-    type promotion and most coercision so the type system and checking
-    goto-programs is simpler than C.}
-  \item[\file{dstring.h}]{The CPROVER string class.  This enables
-    sharing between strings which significantly reduces the amount of
-    memory required and speeds comparison.  \code{dstring} should not
-    be used directly, \code{irep\_idt} should be used instead, which
-    (dependent on build options) is an alias for \code{dstring}.}
-  \item[\file{mp\_arith.h}]{The wrapper class for multi-precision
-    arithmetic within CPROVER.  Also see \file{arith\_tools.h}.}
-  \item[\file{ieee\_float.h}]{The arbitrary precision float model used
-    within CPROVER.  Based on \code{mp\_integer}s.}
-  \item[\file{context.h}]{A generic container for symbol table like
-    constructs such as namespaces.  Lookup gives type, location of
-    declaration, name, `pretty name', whether it is static or not.}
-  \item[\file{namespace.h}]{The preferred interface for the context
-    class.  The key function is \code{lookup} which converts a string
-    (\code{irep\_idt}) to a symbol which gives the scope of
-    declaration, type and so on.  This works for functions as well as variables.}
-\end{description}
-
-
-
-
-\subsubsection{\dir{langapi/}}
-
-This contains the basic interfaces and support classes for programming
-language front ends.  Developers only really need look at this if they
-are adding support for a new language.  It's main users are the two
-(in trunk) language front-ends; \dir{ansi-c/} and \dir{cpp/}.
-
-
-\subsubsection{\dir{ansi-c/}}
-
-Contains the front-end for ANSI C, plus a variety of common
-extensions.  This parses the file, performs some basic sanity checks
-(this is one area in which the UI could be improved; patches most
-welcome) and then produces a goto-program (see below).  The parser is
-a traditional Flex / Bison system.  
-
-\file{internal\_addition.c} contains the implementation of various
-`magic' functions that are that allow control of the analysis from the
-source code level.  These include assertions, assumptions, atomic
-blocks, memory fences and rounding modes.
-
-The \dir{library/} subdirectory contains versions of some of the C
-standard header files that make use of the CPROVER built-in
-functions.  This allows CPROVER programs to be `aware' of the
-functionality and model it correctly.  Examples include
-\file{stdio.c}, \file{string.c}, \file{setjmp.c} and various threading
-interfaces.
-
-
-\subsubsection{\dir{cpp/}}
-
-This directory contains the C++ front-end.  It supports the subset of
-C++ commonly found in embedded and system applications.
-Consequentially it doesn't have full support for templates and many of
-the more advanced and obscure C++ features.  The subset of the
-language that can be handled is being extended over time so bug
-reports of programs that cannot be parsed are useful.
-
-The functionality is very similar to the ANSI C front end; parsing the
-code and converting to goto-programs.  It makes use of code from
-\dir{langapi} and \dir{ansi-c}.
-
-
-
-
-\subsubsection{\dir{goto-programs/}}
-
-Goto programs are the intermediate representation of the CPROVER tool
-chain.  They are language independent and similar to many of the
-compiler intermediate languages.  Section \ref{section:goto-programs}
-describes the \code{goto\_programt} and \code{goto\_functionst} data
-structures in detail.  However it useful to understand some of the
-basic concepts.  Each function is a list of instructions, each of
-which has a type (one of 18 kinds of instruction), a code expression,
-a guard expression and potentially some targets for the next
-instruction.  They are not natively in static single-assign (SSA)
-form.  Transitions are nondeterministic (although in practise the
-guards on the transitions normally cover form a disjoint cover of all
-possibilities).  Local variables have non-deterministic values if they
-are not initialised.  Variables and data within the program is
-commonly one of three types (parameterised by width):
-\code{unsignedbv\_typet}, \code{signedbv\_typet} and
-\code{floatbv\_typet}, see \file{util/std\_types.h} for more
-information. Goto programs can be serialised in a binary (wrapped in
-ELF headers) format or in XML (see the various \code{\_serialization}
-files).
-
-
-The \prog{cbmc} option \code{--show-goto-programs} is often a
-good starting point as it outputs goto-programs in a human
-readable form.  However there are a few things to be aware of.
-Functions have an internal name (for example \code{c::f00}) and a
-`pretty name' (for example \code{f00}) and which is used depends on
-whether it is internal or being presented to the user.  The
-\code{main} method is the `logical' main which is not necessarily the
-main method from the code.  In the output \code{NONDET} is use to
-represent a nondeterministic assignment to a variable.  Likewise
-\code{IF} as a beautified \code{GOTO} instruction where the guard
-expression is used as the condition.  \code{RETURN} instructions may
-be dropped if they precede an \code{END\_FUNCTION} instruction.  The
-comment lines are generated from the \code{locationt} field of the
-\code{instructiont} structure.
-
-\dir{goto-programs/} is one of the few places in the CPROVER codebase
-that templates are used.  The intention is to allow the general
-architecture of program and functions to be used for other
-formalisms.  At the moment most of the templates have a single
-instantiation; for example \code{goto\_functionst} and
-\code{goto\_function\_templatet} and \code{goto\_programt} and \code{goto\_program\_templatet}.
-
-
-
-\subsubsection{\dir{goto-symex/}}
-
-This directory contains a symbolic evaluation system for
-goto-programs.  This takes a goto-program and translates it to an
-equation system by traversing the program, branching and merging and
-unwinding loops as needed.  Each reverse goto has a separate counter
-(the actual counting is handled by \prog{cbmc}, see the \code{--unwind}
-and \code{--unwind-set} options).  When a counter limit
-is reach, an assertion can be added to explicitly show when analysis
-is incomplete.  The symbolic execution includes constant folding so
-loops that have a constant number of iterations will be handled
-completely (assuming the unwinding limit is sufficient).
-
-The output of the symbolic execution is a system of equations; an
-object containing a list of \code{symex\_target\_elements}, each of
-which are equalities between \prog{expr} expressions.  See
-\file{symex\_target\_equation.h}.  The output is in static, single
-assignment (SSA) form, which is \emph{not} the case for goto-programs.
-
-
-
-\subsubsection{\dir{pointer-analysis/}}
-
-To perform symbolic execution on programs with dereferencing of
-arbitrary pointers, some alias analysis is needed.
-\dir{pointer-analysis} contains the three levels of analysis; flow and
-context insensitive, context sensitive and flow and context
-sensitive.  The code needed is subtle and sophisticated and thus there
-may be bugs.
-
-
-
-
-\subsubsection{\dir{solvers/}}
-
-The \dir{solvers/} directory contains interfaces to a number of
-different decision procedures, roughly one per directory.  
-
-\begin{description}
-
-  \item[prop/]{The basic and common functionality.  The key file is
-    \file{prop\_conv.h} which defines \code{prop\_convt}.  This is the
-     base class that is used to interface to the decision procedures.
-     The key functions are \code{convert} which takes an \code{exprt}
-     and converts it to the appropriate, solver specific, data
-     structures and \code{dec\_solve} (inherited from
-     \code{decision\_proceduret}) which invokes the actual decision
-     procedures.  Individual decision procedures (named
-     \code{*\_dect}) objects can be created but \code{prop\_convt} is
-     the preferred interface for code that uses them.}  
-
-  \item[flattening/]{A library that converts operations to
-    bit-vectors, including calling the conversions in \dir{floatbv} as
-    necessary.  Is implemented as a simple conversion (with caching)
-    and then a post-processing function that adds extra constraints.
-    This is not used by the SMT or CVC back-ends.}  
-
-  %%%%
-
-  \item[dplib/]{Provides the \code{dplib\_dect} object which used the
-    decision procedure library from ``Decision Procedures : An
-    Algorithmic Point of View''.}  
-
-  \item[cvc/]{Provides the \code{cvc\_dect} type which interfaces to
-    the old (pre SMTLib) input format for the CVC family of solvers.
-    This format is still supported by depreciated in favour of SMTLib 2.}  
-
-  \item[smt1/]{Provides the \code{smt1\_dect} type which converts the
-    formulae to SMTLib version 1 and then invokes one of Boolector,
-    CVC3, OpenSMT, Yices, MathSAT or Z3.  Again, note that this format
-    is depreciated.}  
-
-  \item[smt2/]{Provides the \code{smt2\_dect} type which functions in
-    a similar way to \code{smt1\_dect}, calling Boolector, CVC3,
-    MathSAT, Yices or Z3.  Note that the interaction with the solver
-    is batched and uses temporary files rather than using the
-    interactive command supported by SMTLib 2.  With the \code{--fpa}
-    option, this output mode will not flatten the floating point
-    arithmetic and instead output the proposed SMTLib floating point
-    standard.}
-  
-  \item[qbf/]{Back-ends for a variety of QBF solvers.  Appears to be
-    no longer used or maintained.}
-  
-  \item[sat/]{Back-ends for a variety of SAT solvers and DIMACS
-    output.}  
-\end{description}
-
-
-
-
-
-\subsubsection{\dir{cbmc/}}
-\label{section:CBMC}
-
-This contains the first full application.  CBMC is a bounded model
-checker that uses the front ends (\dir{ansi-c}, \dir{cpp}, goto-program or others)
-to create a goto-program, \dir{goto-symex} to unwind the loops the given
-number of times and to produce and equation system and finally
-\dir{solvers} to find a counter-example (technically, \dir{goto-symex}
-is then used to construct the counter-example trace).
-
-
-
-\subsubsection{\dir{goto-cc/}}
-\label{section:goto-cc}
-
-\dir{goto-cc} is a compiler replacement that just performs the first
-step of the process; converting C or C++ programs to goto-binaries.
-It is intended to be dropped in to an existing build procedure in
-place of the compiler, thus it emulates flags that would affect the
-semantics of the code produced.  Which set of flags are emulated
-depends on the naming of the \dir{goto-cc/} binary.  If it is called
-\prog{goto-cc} then it emulates GCC flags, \prog{goto-armcc} emulates
-the ARM compiler, \prog{goto-cl} emulates VCC and \prog{goto-cw}
-emulates the Code Warrior compiler.  The output of this tool can then
-be used with \prog{cbmc} or \prog{goto-instrument}.
-
-
-
-
-\subsubsection{\dir{goto-instrument/}}
-\label{section:goto-instrument}
-
-The \dir{goto-instrument/} directory contains a number of tools, one
-per file, that are built into the \prog{goto-instrument} program.  All
-of them take in a goto-program (produced by \prog{goto-cc}) and either
-modify it or perform some analysis.  Examples include
-\file{nondet\_static.cpp} which initialises static variables to a
-non-deterministic value, \file{nondet\_volatile.cpp} which assigns
-a non-deterministic value to any volatile variable before it is read
-and \file{weak\_memory.h} which performs the necessary transformations
-to reason about weak memory models.  The exception to the ``one file
-for each piece of functionality'' rule are the program instrumentation
-options (mostly those given as ``Safety checks'' in the
-\prog{goto-instrument} help text) which are included in the
-\prog{goto-program/} directory.  An example of this is
-\file{goto-program/stack\_depth.h} and the general rule seems to be
-that transformations and instrumentation that \prog{cbmc} uses should
-be in \dir{goto-program/}, others should be in \dir{goto-instrument}.
-
-\prog{goto-instrument} is a very good template for new analysis
-tools.  New developers are advised to copy the directory, remove all
-files apart from \file{main.*}, \file{parseoptions.*} and the
-\file{Makefile} and use these as the skeleton of their application.
-The \code{doit()} method in \file{parseoptions.cpp} is the preferred
-location for the top level control for the program.
-
-
-
-\subsubsection{\dir{linking/}}
-
-Probably the code to emulate a linker.  This allows multiple `object
-files' (goto-programs) to be linked into one `executable' (another
-goto-program), thus allowing existing build systems to be used to
-build complete goto-program binaries.
-
-
-\subsubsection{\dir{big-int/}}
-
-CPROVER is distributed with its own multi-precision arithmetic
-library; mainly for historical and portability reasons.  The library is externally
-developed and thus \dir{big-int} contains the source as it is
-distributed.  This should not be used directly, see
-\file{util/mp\_arith.h} for the CPROVER interface.
-
-
-
-\subsubsection{\dir{xmllang/}}
-
-CPROVER has optional XML output for results and there is an XML format
-for goto-programs.  It is used to interface to various IDEs.  The
-\dir{xmllang/} directory contains the parser and helper functions for
-handling this format.
-
-
-
-\subsubsection{\dir{floatbv/}}
-
-This library contains the code that is used to convert floating point
-variables (\code{floatbv}) to bit vectors (\code{bv}).  This is
-referred to as `bit-blasting' and is called in the \dir{solver} code
-during conversion to SAT or SMT.  It also contains the abstraction
-code described in the FMCAD09 paper.
-
-
-
-
-
-
-
-
-\section{Data Structures}
-
-This section discusses some of the key data-structures used in the
-CPROVER codebase.
-
-\subsection{\code{irept}}
-\label{section:irept}
-
-There are a large number of kind of tree structured or tree-like data
-in CPROVER.  \code{irept} provides a single, unified representation for
-all of these, allowing structure sharing and reference counting of
-data.  As such \code{irept} is the basic unit of data in CPROVER.
-Each \code{irept} contains\footnote{Or references, if reference
-  counted data sharing is enabled.  It is enabled by default; see the
-  \code{SHARING} macro.} a basic unit of data (of type \code{dt})
-which contains four things:
-
-\begin{description}
-\item[\code{data}]{A string\footnote{When \code{USE\_DSTRING} is enabled (it
-    is by default), this is actually a \code{dstring} and thus an
-    integer which is a reference into a string table}, which is
-    returned when the \code{id()} function is used.}
-\item[\code{named\_sub}]{A map from \code{irep\_namet} (a string) to
-    an \code{irept}.  This is used for named children,
-    i.e. subexpressions, parameters, etc.}
-\item[\code{comments}]{Another map from \code{irep\_namet} to
-  \code{irept} which is used for annotations and other `non-semantic' information}
-\item[\code{sub}]{A vector of \code{irept} which is used to store
-  ordered but unnamed children.}
-\end{description}
-
-The \code{irept::pretty} function outputs the contents of an
-\code{irept} directly and can be used to understand an debug problems
-with \code{irept}s.
-
-
-On their own \code{irept}s do not ``mean'' anything; they are
-effectively generic tree nodes.  Their interpretation depends on the
-contents of result of the \code{id} function (the \code{data}) field.
-\file{util/irep\_ids.txt} contains the complete list of \code{id}
-values.  During the build process it is used to generate
-\file{util/irep\_ids.h} which gives constants for each id (named
-\code{ID\_*}).  These can then be used to identify what kind of data
-\code{irept} stores and thus what can be done with it.
-
-To simplify this process, there are a variety of classes that inherit
-from \code{irept}, roughly corresponding to the ids listed
-(i.e. \code{ID\_or} (the string \code{"or''}) corresponds to the class
-\code{or\_exprt}).  These give semantically relevant accessor
-functions for the data; effectively different APIs for the same
-underlying data structure.  None of these classes add fields (only
-methods) and so static casting can be used.  The inheritance graph of
-the subclasses of \code{irept} is a useful starting point for working
-out how to manipulate data.
-
-There are three main groups of classes (or APIs); those derived from
-\code{typet}, \code{codet} and \code{exprt} respectively.  Although
-all of these inherit from \code{irept}, these are the most abstract
-level that code should handle data.  If code is manipulating plain
-\code{irept}s then something is wrong with the architecture of the
-code.
-
-Many of the key descendent of \code{exprt} are declared in
-\file{std\_expr.h}.  All expressions have a named subfield /
-annotation which gives the type of the expression (slightly
-simplified from C/C++ as \code{unsignedbv\_typet},
-\code{signedbv\_typet}, \code{floatbv\_typet}, etc.).  All type
-conversions are explicit with an expression with \code{id() ==
-  ID\_typecast} and an `interface class' named
-\code{typecast\_exprt}.  One key descendent of \code{exprt} is
-\code{symbol\_exprt} which creates \code{irept} instances with the id
-of ``symbol''.  These are used to represent variables; the name of
-which can be found using the \code{get\_identifier} accessor function.
-
-
-\code{codet} inherits from \code{exprt} and is defined in
-\file{std\_code.h}.  They represent executable code; statements in C
-rather than expressions.  In the front-end there are versions of these
-that hold whole code blocks, but in goto-programs these have been
-flattened so that each \code{irept} represents one sequence point
-(almost one line of code / one semi-colon).  The most common
-descendents of \code{codet} are \code{code\_assignt} so a common
-pattern is to cast the \code{codet} to an assignment and then recurse
-on the expression on either side.
-
-
-
-
-
-
-\subsection{\code{goto-programs}}
-\label{section:goto-programs}
-
-The common starting point for working with goto-programs is the
-\code{read\_goto\_binary} function which populates an object of
-\code{goto\_functionst} type.  This is defined in
-\file{goto\_functions.h} and is an instantiation of the template
-\code{goto\_functions\_templatet} which is contained in
-\file{goto\_functions\_template.h}.  They are wrappers around a map from
-strings to \code{goto\_programt}'s and iteration macros are provided.
-Note that \code{goto\_function\_templatet} (no \code{s}) is defined in
-the same header as \code{goto\_functions\_templatet} and is gives the
-C type for the function and Boolean which indicates whether the body
-is available (before linking this might not always be true).  Also
-note the slightly counter-intuitive naming; \code{goto\_functionst}
-instances are the top level structure representing the program and
-contain \code{goto\_programt} instances which represent the individual
-functions.  At the time of writing \code{goto\_functionst} is the only
-instantiation of the template \code{goto\_functions\_templatet} but
-other could be produced if a different data-structures / kinds of models
-were needed for functions.
-
-\code{goto\_programt} is also an instantiation of a template.  In a
-similar fashion it is \code{goto\_program\_templatet} and allows the
-types of the guard and expression used in instructions to be
-parameterised.  Again, this is currently the only use of the template.
-As such there are only really helper functions in
-\file{goto\_program.h} and thus \code{goto\_program\_template.h} is
-probably the key file that describes the representation of (C)
-functions in the goto-program format.  It is reasonably stable and
-reasonably documented and thus is a good place to start looking at the code.
-
-An instance of \code{goto\_program\_templatet} is effectively a list
-of instructions (and inner template called \code{instructiont}).  It
-is important to use the copy and insertion functions that are provided
-as iterators are used to link instructions to their predecessors and
-targets and careless manipulation of the list could break these.
-Likewise there are helper macros for iterating over the instructions
-in an instance of \code{goto\_program\_templatet} and the use of these
-is good style and strongly encouraged.
-
-Individual instructions are instances of type \code{instructiont}.
-They represent one step in the function.  Each has a type, an instance
-of \code{goto\_program\_instruction\_typet} which denotes what kind of
-instruction it is.  They can be computational (such as \code{ASSIGN}
-or \code{FUNCTION\_CALL}), logical (such as \code{ASSUME} and
-\code{ASSERT}) or informational (such as \code{LOCATION} and
-\code{DEAD}).  At the time of writing there are 18 possible values for
-\code{goto\_program\_instruction\_typet} / kinds of instruction.
-Instructions also have a guard field (the condition under which it is
-executed) and a code field (what the instruction does).  These may be
-empty depending on the kind of instruction.  In the default
-instantiations these are of type \code{exprt} and \code{codet}
-respectively and thus covered by the previous discussion of
-\code{irept} and its descendents.  The next instructions (remembering
-that transitions are guarded by non-deterministic) are given by the
-list \code{targets} (with the corresponding list of labels
-\code{labels}) and the corresponding set of previous instructions is
-get by \code{incoming\_edges}.  Finally \code{instructiont} have
-informational \code{function} and \code{location} fields that indicate
-where they are in the code.
-
-
-
-\end{document}

doc/html-manual/api.shtml

@@ -1,323 +0,0 @@
-<!--#include virtual="header.inc" -->
-
-<p><a href="./">CPROVER Manual TOC</a></p>
-
-<h2>The CPROVER API Reference</h2>
-
-<p class="justified">
-The following sections summarize the functions available to programs
-that are passed to the CPROVER tools.
-</p>
-
-<h3>Functions</h3>
-
-<h4>__CPROVER_assume, __CPROVER_assert, assert</h4>
-
-<hr>
-<code>
-void __CPROVER_assume(_Bool assumption);<br>
-void __CPROVER_assert(_Bool assertion, const char *description);<br>
-void assert(_Bool assertion);
-</code>
-<hr>
-
-<p class="justified">
-The function <b>__CPROVER_assume</b> adds an expression as a constraint
-to the program. If the expression evaluates to false, the execution
-aborts without failure. More detail on the use of assumptions is
-in the section on <a href="modeling-assertions.shtml">Assumptions
-and Assertions</a>.
-</p>
-
-<h4>__CPROVER_same_object, __CPROVER_POINTER_OBJECT,
-__CPROVER_POINTER_OFFSET,
-__CPROVER_DYNAMIC_OBJECT</h4>
-
-<hr>
-<code>
-_Bool __CPROVER_same_object(const void *, const void *);<br>
-unsigned __CPROVER_POINTER_OBJECT(const void *p);<br>
-signed __CPROVER_POINTER_OFFSET(const void *p);<br>
-_Bool __CPROVER_DYNAMIC_OBJECT(const void *p);
-</code>
-<hr>
-
-<p class="justified">
-The function <b>__CPROVER_same_object</b> returns true
-if the two pointers given as arguments point to the same
-object.
-The function <b>__CPROVER_POINTER_OFFSET</b> returns
-the offset of the given pointer relative to the base
-address of the object.
-The function <b>__CPROVER_DYNAMIC_OBJECT</b>
-returns true if the pointer passed
-as arguments points to a dynamically allocated object.
-</p>
-
-<h4>__CPROVER_is_zero_string,
-__CPROVER_zero_string_length,
-__CPROVER_buffer_size</h4>
-
-<hr>
-<code>
-_Bool __CPROVER_is_zero_string(const void *);<br>
-__CPROVER_size_t __CPROVER_zero_string_length(const void *);<br>
-__CPROVER_size_t __CPROVER_buffer_size(const void *);
-</code>
-<hr>
-
-<p class="justified">
-</p>
-
-<h4>__CPROVER_initialize</h4>
-
-<hr>
-<code>
-void __CPROVER_initialize(void);
-</code>
-<hr>
-
-<p class="justified">
-The function <b>__CPROVER_initialize</b> computes the initial
-state of the program. It is called prior to calling the
-main procedure of the program.
-</p>
-
-<h4>__CPROVER_input, __CPROVER_output</h4>
-
-<hr>
-<code>
-void __CPROVER_input(const char *id, ...);<br>
-void __CPROVER_output(const char *id, ...);
-</code>
-<hr>
-
-<p class="justified">
-The functions <b>__CPROVER_input</b> and <b>__CPROVER_output</b>
-are used to report an input or output value. Note that they do not generate
-input or output values. The first argument is a string constant
-to distinguish multiple inputs and outputs (inputs are typically
-generated using nondeterminism, as described
-<a href="modeling-nondet.shtml">here</a>).
-The string constant is followed by an arbitrary number of values of
-arbitrary types.
-</p>
-
-<h4>__CPROVER_cover</h4>
-
-<hr>
-<code>
-void __CPROVER_cover(_Bool condition);
-</code>
-<hr>
-
-<p>This statement defines a custom coverage criterion, for usage
-with the <a href="cover.shtml">test suite generation feature</a>.</p>
-
-<p class="justified">
-</p>
-
-<h4>__CPROVER_isnan, __CPROVER_isfinite, __CPROVER_isinf,
-__CPROVER_isnormal, __CPROVER_sign</h4>
-
-<hr>
-<code>
-_Bool __CPROVER_isnan(double f);<br>
-_Bool __CPROVER_isfinite(double f);<br>
-_Bool __CPROVER_isinf(double f);<br>
-_Bool __CPROVER_isnormal(double f);<br>
-_Bool __CPROVER_sign(double f);
-</code>
-<hr>
-
-<p class="justified">
-The function <b>__CPROVER_isnan</b> returns true if the double-precision
-floating-point number passed as argument is a
-<a href="http://en.wikipedia.org/wiki/NaN">NaN</a>.
-</p>
-
-<p class="justified">
-The function <b>__CPROVER_isfinite</b> returns true if the double-precision
-floating-point number passed as argument is a
-finite number.
-</p>
-
-<p class="justified">
-This function <b>__CPROVER_isinf</b> returns true if the double-precision
-floating-point number passed as argument is plus
-or minus infinity.
-</p>
-
-<p class="justified">
-The function <b>__CPROVER_isnormal</b> returns true if the double-precision
-floating-point number passed as argument is a
-normal number.
-</p>
-
-<p class="justified">
-This function <b>__CPROVER_sign</b> returns true if the double-precision
-floating-point number passed as argument is
-negative.
-</p>
-
-<h4>__CPROVER_abs, __CPROVER_labs, __CPROVER_fabs, __CPROVER_fabsl, __CPROVER_fabsf</h4>
-
-<hr>
-<code>
-int __CPROVER_abs(int x);<br>
-long int __CPROVER_labs(long int x);<br>
-double __CPROVER_fabs(double x);<br>
-long double __CPROVER_fabsl(long double x);<br>
-float __CPROVER_fabsf(float x);
-</code>
-<hr>
-
-<p class="justified">
-These functions return the absolute value of the given
-argument.
-</p>
-
-<h4>__CPROVER_array_equal, __CPROVER_array_copy, __CPROVER_array_set</h4>
-
-<hr>
-<code>
-_Bool __CPROVER_array_equal(const void array1[], const void array2[]);<br>
-void __CPROVER_array_copy(const void dest[], const void src[]);<br>
-void __CPROVER_array_set(const void dest[], value);
-</code>
-<hr>
-
-<p class="justified">
-The function <b>__CPROVER_array_equal</b> returns true if the values
-stored in the given arrays are equal.
-The function <b>__CPROVER_array_copy</b> copies the contents of
-the array <b>src</b> to the array <b>dest</b>.
-The function <b>__CPROVER_array_set</b> initializes the array <b>dest</b> with
-the given value.
-</p>
-
-<h4>Uninterpreted Functions</h4>
-
-<p class="justified">
-Uninterpreted functions are documented <a href="modeling-nondet.shtml">here</a>.
-</p>
-
-<h3>Predefined Types and Symbols</h3>
-
-<h4>__CPROVER_bitvector</h4>
-
-<hr>
-<code>
-__CPROVER_bitvector [ <i>expression</i> ]
-</code>
-<hr>
-
-<p class="justified">
-This type is only available in the C frontend. It is used
-to specify a bit vector with arbitrary but fixed size. The
-usual integer type modifiers <b>signed</b> and <b>unsigned</b>
-can be applied. The usual arithmetic promotions will be
-applied to operands of this type.
-</p>
-
-<h4>__CPROVER_floatbv</h4>
-
-<hr>
-<code>
-__CPROVER_floatbv [ <i>expression</i> ] [ <i>expression</i> ]
-</code>
-<hr>
-
-<p class="justified">
-This type is only available in the C frontend.  It is used
-to specify an IEEE-754 floating point number with arbitrary
-but fixed size.  The first parameter is the total size (in bits)
-of the number, and the second is the size (in bits) of the
-mantissa, or significand (not including the hidden bit, thus for
-single precision this should be 23).
-</p>
-
-<h4>__CPROVER_fixedbv</h4>
-
-<hr>
-<code>
-__CPROVER_fixedbv [ <i>expression</i> ] [ <i>expression</i> ]
-</code>
-<hr>
-
-<p class="justified">
-This type is only available in the C frontend.  It is used
-to specify a fixed-point bit vector with arbitrary
-but fixed size.  The first parameter is the total size (in bits)
-of the type, and the second is the number of bits after the radix
-point.
-</p>
-
-<h4>__CPROVER_size_t</h4>
-
-<p class="justified">
-The type of sizeof expressions.
-</p>
-
-<h4>__CPROVER_rounding_mode</h4>
-
-<hr>
-<code>
-extern int __CPROVER_rounding_mode;
-</code>
-<hr>
-
-<p class="justified">
-This variable contains the IEEE floating-point
-arithmetic rounding mode.
-</p>
-
-<h4>__CPROVER_constant_infinity_uint</h4>
-
-<p class="justified">
-This is a constant that models a large unsigned
-integer.
-</p>
-
-<h4>__CPROVER_integer, __CPROVER_rational</h4>
-
-<p class="justified">
-<b>__CPROVER_integer</b> is an unbounded, signed integer type.
-<b>__CPROVER_rational</b> is an unbounded, signed rational
-number type.
-</p>
-
-<h4>__CPROVER_memory</h4>
-
-<hr>
-<code>
-extern unsigned char __CPROVER_memory[];
-</code>
-<hr>
-
-<p class="justified">
-This array models the contents of integer-addressed memory.
-</p>
-
-<h4>__CPROVER::unsignedbv&lt;N&gt; (C++ only)</h4>
-
-<p class="justified">This type is the equivalent of <b>unsigned __CPROVER_bitvector[N]</b> in the C++ front-end.
-</p>
-
-<h4>__CPROVER::signedbv&lt;N&gt; (C++ only)</h4>
-
-<p class="justified">This type is the equivalent of <b>signed __CPROVER_bitvector[N]</b> in the C++ front-end.
-</p>
-
-<h4>__CPROVER::fixedbv&lt;N&gt; (C++ only)</h4>
-
-<p class="justified">This type is the equivalent of <b>__CPROVER_fixedbv[N,m]</b> in the C++ front-end.
-</p>
-
-<h3>Concurrency</h3>
-
-<p class="justified">
-Asynchronous threads are created by preceding an instruction with a label with the prefix <b>__CPROVER_ASYNC_</b>.
-</p>
-
-<!--#include virtual="footer.inc" -->

doc/html-manual/architecture.shtml

@@ -1,93 +0,0 @@
-<!--#include virtual="header.inc" -->
-
-<p><a href="./">CPROVER Manual TOC</a></p>
-
-<h2>Build Systems and Libraries</h2>
-
-<h3>Architectural Settings</h3>
-
-<p class="justified"> The behavior of a C/C++ program depends on a number of
-parameters that are specific to the architecture the program was compiled
-for. The three most important architectural parameters are:</p>
-
-<ul>
-<li>The width of the various scalar types; e.g., compare the value
-of <code>sizeof(long int)</code> on various machines.</li>
-
-<li>The width of pointers; e.g., compare the value
-of <code>sizeof(int *)</code> on various machines.</li>
-
-<li>The <a href="http://en.wikipedia.org/wiki/Endianness">endianness</a>
-of the architecture.</li>
-</ul>
-
-<p class="justified">
-In general, the CPROVER tools attempt to adopt the settings of the
-particular architecture the tool itself was compiled for. For example,
-when running a 64 bit binary of CBMC on Linux, the program will be processed
-assuming that <code>sizeof(long int)==8</code>.</p>
-
-<p class="justified">
-As a consequence of these architectural parameters,
-you may observe different verification results for an identical
-program when running CBMC on different machines. In order to get
-consistent results, or when aiming at validating a program written
-for a different platform, the following command-line arguments can
-be passed to the CPROVER tools:</p>
-
-<ul>
-<li>The word-width can be set with <code>--16</code>,
-<code>--32</code>, <code>--64</code>.</li>
-<li>The endianness can be defined with
-<code>--little-endian</code> and <code>--big-endian</code>.</li>
-</ul>
-
-<p class="justified">
-When using a goto binary, CBMC and the other tools read the configuration
-from the binary, i.e., the setting when running goto-cc is the one that
-matters; the option given to the model checker is ignored in this case.
-</p>
-
-<p class="justified">
-In order to see the effect of the options <code>--16</code>,
-<code>--32</code> and <code>--64</code>, pass
-the following program to CBMC:</p>
-
-<hr>
-<code>
-#include &lt;stdio.h&gt;<br>
-#include &lt;assert.h&gt;<br>
-<br>
-int main() {<br>
-&nbsp;&nbsp;printf("sizeof(long int): %d\n", (int)sizeof(long int));<br>
-&nbsp;&nbsp;printf("sizeof(int *): %d\n", (int)sizeof(int *));<br>
-&nbsp;&nbsp;assert(0);<br>
-}
-</code>
-<hr>
-
-<p class="justified">
-The counterexample trace contains the strings printed by the
-<code>printf</code> command.</p>
-
-<p class="justified">
-The effects of endianness are
-more subtle. Try the following program with <code>--big-endian</code>
-and <code>--little-endian</code>:</p>
-
-<hr>
-<pre><code>
-#include &lt;stdio.h&gt;<br>
-#include &lt;assert.h&gt;<br>
-<br>
-int main() {<br>
-&nbsp;&nbsp;int i=0x01020304;<br>
-&nbsp;&nbsp;char *p=(char *)&amp;i;<br>
-&nbsp;&nbsp;printf("Bytes of i: %d, %d, %d, %d\n",<br>
-&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;p[0], p[1], p[2], p[3]);<br>
-&nbsp;&nbsp;assert(0);<br>
-}
-</code></pre>
-<hr>
-
-<!--#include virtual="footer.inc" -->

doc/html-manual/cbmc-loops.shtml

@@ -1,233 +0,0 @@
-<!--#include virtual="header.inc" -->
-
-<link rel="stylesheet" href="highlight/styles/default.css">
-<script src="highlight/highlight.pack.js" type="text/javascript"></script>
-<script type="text/javascript">hljs.initHighlightingOnLoad();</script>
-
-<p><a href="./">CPROVER Manual TOC</a></p>
-
-<h2>CBMC: Bounded Model Checking for C/C++ and Java</h2>
-
-<h3>Understanding Loop Unwinding</h3>
-
-<h4>Iteration-based Unwinding</h4>
-
-<p class="justified">
-The basic idea of CBMC is to model the computation of the programs up to a
-particular depth.  Technically, this is achieved by a process that
-essentially amounts to <i>unwinding loops</i>.  This concept is best
-illustrated with a generic example:
-</p>
-
-<pre><code>int main(int argc, char **argv) {
-  while(cond) {
-    <font color="#3030f0">BODY CODE</font>
-  }
-}
-</code></pre>
-
-<p class="justified">
-A BMC instance that will find bugs with up to five iterations of the loop would
-contain five copies of the loop body, and essentially corresponds to checking
-the following loop-free program:
-</p>
-
-<pre><code>int main(int argc, char **argv) {
-  if(cond) {
-    <font color="#3030f0">BODY CODE COPY 1</font>
-    if(cond) {
-      <font color="#3030f0">BODY CODE COPY 2</font>
-      if(cond) {
-        <font color="#3030f0">BODY CODE COPY 3</font>
-        if(cond) {
-          <font color="#3030f0">BODY CODE COPY 4</font>
-          if(cond) {
-            <font color="#3030f0">BODY CODE COPY 5</font>
-          }
-        }
-      }
-    }
-  }
-}
-</code></pre>
-
-<p class="justified">
-Note the use of the <code>if</code> statement to prevent the execution of
-the loop body in the case that the loop ends before five iterations are executed.
-The construction above is meant to produce a program that is trace equivalent
-with the original programs for those traces that contain up to five iterations
-of the loop.
-</p>
-
-<p class="justified">
-In many cases, CBMC is able to automatically determine an upper bound on the
-
-number of loop iterations. This may even work when the number of loop
-unwindings is not constant. Consider the following example:
-</p>
-
-<pre><code>_Bool f();
-
-int main() {
-  for(int i=0; i<100; i++) {
-    if(f()) break;
-  }
-  
-  assert(0);
-}
-</code></pre>
-
-<p class="justified">
-The loop in the program above has an obvious upper bound on the number of
-iterations, but note that the loop may abort prematurely depending on the
-value that is returned by <code>f()</code>.  CBMC is nevertheless able to
-automatically unwind the loop to completion.</p>
-
-<p class="justified">
-This automatic detection of the unwinding
-bound may fail if the number of loop iterations is highly data-dependent.
-Furthermore, the number of iterations that are executed by any given
-loop may be too large or may simply be unbounded. For this case,
-CBMC offers the command-line option <code>--unwind B</code>, where
-<code>B</code> denotes a number that corresponds to the maximal number
-of loop unwindings CBMC performs on any loop.
-</p>
-
-<p class="justified">
-Note that the number of unwindings is measured by counting the number of
-<i>backjumps</i>.  In the example above, note that the condition
-<code>i<100</code> is in fact evaluated 101 times before the loop
-terminates.  Thus, the loop requires a limit of 101, and not 100.</p>
-
-<h4>Setting Separate Unwinding Limits</h4>
-
-<p class="justified">
-The setting given with <code>--unwind</code> is used globally,
-that is, for all loops in the program. In order to set individual
-limits for the loops, first use
-</p>
-
-<code>
-&nbsp;&nbsp;--show-loops
-</code>
-
-<p class="justified">
-to obtain a list of all loops in the program. Then identify the loops
-you need to set a separate bound for, and note their loop ID. Then
-use
-</p>
-
-<code>
-&nbsp;&nbsp;--unwindset L:B,L:B,...
-</code>
-
-<p>
-where <code>L</code> denotes a loop ID and <code>B</code> denotes
-the bound for that loop.</p>
-
-<p class="justified">
-As an example, consider a program with two loops in the function
-main:
-</p>
-
-<code>
-&nbsp;&nbsp;--unwindset c::main.0:10,c::main.1:20
-</code>
-
-<p class="justified">
-This sets a bound of 10 for the first loop, and a bound of 20 for
-the second loop.
-</p>
-
-<p class="justified">
-What if the number of unwindings specified is too small? In this case, bugs
-that require paths that are deeper may be missed.  In order to address this
-problem, CBMC can optionally insert checks that the given unwinding bound is
-actually sufficiently large.  These checks are called <i>unwinding
-assertions</i>, and are enabled with the option
-<code>--unwinding-assertions</code>.  Continuing the generic example above,
-this unwinding assertion for a bound of five corresponds to checking the
-following loop-free program:
-</p>
-
-<pre><code>int main(int argc, char **argv) {
-  if(cond) {
-    <font color="#3030f0">BODY CODE COPY 1</font>
-    if(cond) {
-      <font color="#3030f0">BODY CODE COPY 2</font>
-      if(cond) {
-        <font color="#3030f0">BODY CODE COPY 3</font>
-        if(cond) {
-          <font color="#3030f0">BODY CODE COPY 4</font>
-          if(cond) {
-            <font color="#3030f0">BODY CODE COPY 5</font>
-            <font color="#ff3030">assert(!cond);</font>
-          }
-        }
-      }
-    }
-  }
-}
-</code></pre>
-
-<p class="justified">
-The unwinding assertions can be verified just like any other generated
-assertion.  If all of them are proven to hold, the given loop bounds are
-sufficient for the program.  This establishes a <a
-href="http://en.wikipedia.org/wiki/Worst-case_execution_time"><i>high-level
-worst-case execution time</i></a> (WCET). 
-</p>
-
-<p class="justified">
-In some cases, it is desirable to cut off very deep loops in favor
-of code that follows the loop. As an example, consider the
-following program:
-</p>
-
-<pre><code>int main() {
-  for(int i=0; i<10000; i++) {
-    <font color="#3030f0">BODY CODE</font>
-  }
-  
-  assert(0);
-}
-</code></pre>
-
-<p class="justified">
-In the example above, small values of <code>--unwind</code> will
-prevent that the assertion is reached. If the code in the loop
-is considered irrelevant to the later assertion, use the option
-</p>
-
-<code>
-&nbsp;&nbsp;--partial-loops
-</code>
-
-<p class="justified">
-This option will allow paths that execute loops only partially,
-enabling a counterexample for the assertion above even for
-small unwinding bounds. The disadvantage of using this option
-is that the resulting path may be spurious, i.e., may not
-exist in the original program.
-</p>
-
-<h4>Depth-based Unwinding</h4>
-
-<p class="justified">
-The loop-based unwinding bound is not always appropriate. In particular,
-it is often difficult to control the size of the generated formula
-when using the <code>--unwind</code> option. The option
-</p>
-
-<code>
-&nbsp;&nbsp;--depth <i>nr</i>
-</code>
-
-<p class="justified">
-specifies an unwinding bound in terms of the number of instructions that are
-executed on a given path, irrespectively of the number of loop iterations.
-Note that CBMC uses the number of instructions in the control-flow graph
-as the criterion, not the number of instructions in the source code.
-</p>
-
-<!--#include virtual="footer.inc" -->

doc/html-manual/cbmc.shtml

@@ -1,377 +0,0 @@
-<!--#include virtual="header.inc" -->
-
-<link rel="stylesheet" href="highlight/styles/default.css">
-<script src="highlight/highlight.pack.js" type="text/javascript"></script>
-<script type="text/javascript">hljs.initHighlightingOnLoad();</script>
-
-<p><a href="./">CPROVER Manual TOC</a></p>
-
-<h2>CBMC: Bounded Model Checking for C/C++ and Java</h2>
-
-<h3>A Short Tutorial</h3>
-
-<h4>First Steps</h4>
-
-<p class="justified">
-We assume you have already installed CBMC and the necessary support files
-on your system. If not so, please follow <a href="installation-cbmc.shtml">
-these instructions</a>.
-</p>
-
-<p class="justified">
-Like a compiler, CBMC takes the names of .c files as command line
-arguments. CBMC then translates the program and merges the function
-definitions from the various .c files, just like a linker. But instead
-of producing a binary for execution, CBMC performs symbolic simulation on
-the program.
-</p>
-
-<p class="justified">
-As an example, consider the following simple program, named
-<a href="file1.c">file1.c</a>:
-</p>
-
-<pre><code class="c">int puts(const char *s) { }
-
-int main(int argc, char **argv) {
-  puts(argv[2]);
-}
-</code></pre>
-
-<p class="justified">
-Of course, this program is faulty, as the <code>argv</code> array might have fewer
-than three elements, and then the array access <code>argv[2]</code> is out of bounds.
-Now, run CBMC as follows:
-</p>
-
-<code>
-&nbsp;&nbsp;cbmc file1.c --show-properties --bounds-check --pointer-check
-</code>
-
-<p class="justified">The two options <code>--bounds-check</code> and <code>--pointer-check</code>
-instruct CBMC to look for errors related to pointers and array bounds.
-CBMC will print the list of properties it checks. Note that it lists,
-among others, a property labeled with "object bounds in argv" together with
-the location of the faulty array access.  As you can see, CBMC largely
-determines the property it needs to check itself.  This is realized by means
-of a preliminary static analysis, which relies on computing a fixed point on
-various <a
-href="http://en.wikipedia.org/wiki/Abstract_interpretation">abstract
-domains</a>.  More detail on automatically generated properties is provided
-<a href="properties.shtml">here</a>.</p>
-
-<p class="justified">
-Note that these automatically generated properties need not necessarily
-correspond to bugs &ndash; these are just <i>potential</i> flaws, as
-abstract interpretation might be imprecise.  Whether these properties
-hold or correspond to actual bugs needs to be determined by further analysis.
-</p>
-
-<p class="justified">
-CBMC performs this analysis using <i>symbolic simulation</i>, which
-corresponds to a translation of the program into a formula.  The formula is
-then combined with the property.  Let's look at the formula that is
-generated by CBMC's symbolic simulation:</p>
-
-<code>
-&nbsp;&nbsp;cbmc file1.c --show-vcc --bounds-check --pointer-check
-</code>
-
-<p class="justified">
-With this option, CBMC performs the symbolic simulation and prints the
-verification conditions on the screen. A verification condition needs
-to be proven to be valid by a <i><a href="http://en.wikipedia.org/wiki/Decision_problem">
-decision procedure</a></i> in order to assert that the corresponding property
-holds. Let's run the decision procedure:</p>
-
-<code>
-&nbsp;&nbsp;cbmc file1.c --bounds-check --pointer-check
-</code>
-
-<p class="justified">
-CBMC transforms the equation you have seen before into CNF and passes it to
-a SAT solver (more background on this step is in the book on <a
-href="http://www.decision-procedures.org/">Decision Procedures</a>).  It
-then determines which of the properties that it has generated for the
-program hold and which do not.  Using the SAT solver, CBMC detects that the
-property for the object bounds of <code>argv</code> does not hold, and will
-thus print a line as follows:
-</p>
-
-<code>
-[main.pointer_dereference.6] dereference failure: object bounds in argv[(signed long int)2]: FAILURE
-</code>
-
-<h3>Counterexample Traces</h3>
-
-<p class="justified">
-Let us have a closer look at this property and why it fails. To aid the
-understanding of the problem, CBMC can generate a <i>counterexample
-trace</i> for failed properties. To obtain this trace, run
-</p>
-
-<code>
-&nbsp;&nbsp;cbmc file1.c --bounds-check --trace
-</code>
-
-<p class="justified">
-CBMC then prints a counterexample trace, i.e., a program trace that begins
-with <code>main</code> and ends in a state which violates the property.  In
-our example, the program trace ends in the faulty array access.  It also
-gives the values the input variables must have for the bug to occur.  In
-this example, <code>argc</code> must be one to trigger the out-of-bounds
-array access.  If you add a branch to the example that requires that
-<code>argc&gt;=3</code>, the bug is fixed and CBMC will report that the
-proofs of all properties have been successful.</p>
-
-<h3>Verifying Modules</h3>
-
-<p class="justified">
-In the example above, we used a program that starts with a <code>main</code>
-function. However, CBMC is aimed at embedded software, and these
-kinds of programs usually have different entry points. Furthermore, CBMC
-is also useful for verifying program modules. Consider the following example,
-called <a href="file2.c">file2.c</a>:
-</p>
-
-<pre><code>int array[10];
-int sum() {
-  unsigned i, sum;
-
-  sum=0;
-  for(i=0; i&lt;10; i++)
-    sum+=array[i];
-}
-</code></pre>
-
-<p class="justified">
-In order to set the entry point to the <code>sum</code> function, run
-</p>
-
-<code>
-&nbsp;&nbsp;cbmc file2.c --function sum --bounds-check
-</code>
-
-<p class="justified">
-It is often necessary to build a suitable <i>harness</i> for the function
-in order to set up the environment appropriately.
-</p>
-
-<h3>Loop Unwinding</h3>
-
-<p class="justified">
-When running the previous example, you will have noted that CBMC unwinds the
-<code>for</code> loop in the program.  As CBMC performs Bounded Model
-Checking, all loops have to have a finite upper run-time bound in order to
-guarantee that all bugs are found.  CBMC can optionally check that enough
-unwinding is performed.  As an example, consider the program <a
-href="binsearch.c">binsearch.c</a>:
-</p>
-
-<pre><code>int binsearch(int x) {
-  int a[16];
-  signed low=0, high=16;
-
-  while(low&lt;high) {
-    signed middle=low+((high-low)>>1);
-
-    if(a[middle]&lt;x)
-      high=middle;
-    else if(a[middle]&gt;x)
-      low=middle+1;
-    else // a[middle]==x
-      return middle;
-  }
-
-  return -1;
-}
-</code></pre>
-
-<p class="justified">
-If you run CBMC on this function, you will notice that the unwinding
-does not stop on its own.  The built-in simplifier is not able to determine
-a run time bound for this loop.  The unwinding bound has to be given as a
-command line argument:</p>
-
-<code>
-&nbsp;&nbsp;cbmc binsearch.c --function binsearch --unwind 6 --bounds-check --unwinding-assertions
-</code>
-
-<p class="justified">
-CBMC verifies that verifies the array accesses are within the bounds; note
-that this actually depends on the result of the right shift.  In addition,
-as CBMC is given the option
-<nobr><code>--unwinding-assertions</code></nobr>, it also checks that enough
-unwinding is done, i.e., it proves a run-time bound.  For any lower
-unwinding bound, there are traces that require more loop iterations.  Thus,
-CBMC will report that the unwinding assertion has failed. As usual, a counterexample
-trace that documents this can be obtained with the option
-<code>--property</code>.
-</p>
-
-<h3>Unbounded Loops</h3>
-
-<p class="justified">
-CBMC can also be used for programs with unbounded loops. In this
-case, CBMC is used for bug hunting only; CBMC does not attempt to find
-all bugs. The following program
-(<a href="lock-example.c">lock-example.c</a>) is an example
-of a program with a user-specified property:</p>
-
-<pre><code>_Bool nondet_bool();
-_Bool LOCK = 0;
-
-_Bool lock() {
-  if(nondet_bool()) {
-    assert(!LOCK);
-    LOCK=1;
-    return 1; }
-
-  return 0;
-}
-
-void unlock() {
-  assert(LOCK);
-  LOCK=0;
-}
-
-int main() {
-  unsigned got_lock = 0;
-  int times;
-
-  while(times > 0) {
-    if(lock()) {
-      got_lock++;
-      /* critical section */
-    }
-
-    if(got_lock!=0)
-      unlock();
-
-    got_lock--;
-    times--;
-} }
-</code></pre>
-
-<p class="justified">
-The <code>while</code> loop in the <code>main</code> function has no
-(useful) run-time bound.  Thus, a bound has to be set on the amount of
-unwinding that CBMC performs.  There are two ways to do so:
-</p>
-
-<ol>
-
-<li>The <code>--unwind</code> command-line parameter can to be used to limit
-the number of times loops are unwound.</li>
-
-<li>The <code>--depth</code> command-line parameter can be used to limit
-the number of program steps to be processed.</li>
-
-</ol>
-
-<p class="justified">
-Given the option <code>--unwinding-assertions</code>, CBMC checks whether
-the arugment to <code>--unwind</code> is large enough to cover all program
-paths. If the argument is too small, CBMC will detect that not enough
-unwinding is done reports that an unwinding assertion has failed.
-</p>
-
-<p class="justified">
-Reconsider the example. For a loop unwinding bound of one, no bug is found.
-But already for a bound of two, CBMC detects a trace that violates an
-assertion. Without unwinding assertions, or when using the <code>--depth</code>
-command line switch, CBMC does not prove the program correct, but it can be
-helpful to find program bugs. The various command line options that CBMC
-offers for loop unwinding are described in the section on
-<a href="cbmc-loops.shtml">understanding loop unwinding</a>.</p>
-
-<h3>A Note About Compilers and the ANSI-C Library</h3>
-
-<p class="justified">
-Most C programs make use of functions provided by a library; instances are
-functions from the standard ANSI-C library such as <code>malloc</code> or
-<code>printf</code>. The verification of programs that use such functions
-has two requirements:</p>
-
-<ol>
-
-<li>Appropriate header files have to be provided. These header files
-contain <i>declarations</i> of the functions that are to be used.
-</li>
-
-<li>Appropriate <i>definitions</i> have to be provided.</li>
-
-</ol>
-
-<p class="justified">
-Most C compilers come with header files for the ANSI-C library functions. 
-We briefly discuss how to obtain/install these library files.
-</p>
-
-<h4>Linux</h4>
-
-<p class="justified">
-Linux systems that are able to compile software are usually equipped with
-the appropriate header files. Consult the documentation of your distribution
-on how to install the compiler and the header files. First try to compile
-some significant program before attempting to verify it.
-</p>
-
-<h4>Windows</h4>
-
-<p class="justified">
-On Microsoft Windows, CBMC is pre-configured to use the compiler that is
-part of Microsoft's Visual Studio.  Microsoft's <a
-href="http://www.visualstudio.com/en-us/products/visual-studio-community-vs">
-Visual Studio Community</a> is fully featured and available for download for
-free from the Microsoft webpage.  Visual Studio installs the usual set of
-header files together with the compiler.  However, the Visual Studio
-compiler requires a large set of environment variables to function
-correctly.  It is therefore required to run CBMC from the <i>Visual Studio
-Command Prompt</i>, which can be found in the menu <i>Visual Studio
-Tools</i>.
-</p>
-
-<p class="justified">
-Note that in both cases, only header files are available. CBMC only
-comes with a small set of definitions, which includes functions such as
-<code>malloc</code>. Detailed information about the built-in definitions is
-<a href="libraries.shtml">here</a>.</p>
-
-<h3>Command Line Interface</h3>
-
-<p class="justified">
-This section describes the command line interface of CBMC. Like a C
-compiler, CBMC takes the names of the .c source files as arguments.
-Additional options allow to customize the behavior of CBMC. Use
-<code>cbmc --help</code> to get a full list of the available options.
-</p>
-
-<p class="justified">
-Structured output can be obtained from CBMC using the option <code>--xml-ui</code>.
-Any output from CBMC (e.g., counterexamples) will then use an XML
-representation.
-</p>
-
-<div class="box1">
-<div class="caption">Further Reading</div>
-
-<ul>
-<li><a href="cbmc-loops.shtml">Understanding Loop Unwinding</a></li>
-<li><a target=_top href="http://www-2.cs.cmu.edu/~svc/papers/view-publications-ck03.html">
-    Hardware Verification using ANSI-C Programs as a Reference</a></li>
-<li><a target=_top href="http://www-2.cs.cmu.edu/~svc/papers/view-publications-cky03.html">
-    Behavioral Consistency of C and Verilog Programs Using Bounded Model
-    Checking</a></li>
-<li><a target=_top href="http://www-2.cs.cmu.edu/~svc/papers/view-publications-ckl2004.html">A
-    Tool for Checking ANSI-C Programs</a></li>
-</ul>
-
-<p class="justified">
-We also have a <a href="http://www.cprover.org/cbmc/applications/">list of
-interesting applications of CBMC</a>.</p>
-
-</div>
-
-<!--#include virtual="footer.inc" -->
-

doc/html-manual/counter.v

@@ -1,10 +0,0 @@
-module top(input clk);
-
-  reg [3:0] counter;
-
-  initial counter=0;
-
-  always @(posedge clk)
-    counter=counter+1;
-
-endmodule

doc/html-manual/cover.shtml

@@ -1,276 +0,0 @@
-<!--#include virtual="header.inc" -->
-
-<link rel="stylesheet" href="highlight/styles/default.css">
-<script src="highlight/highlight.pack.js" type="text/javascript"></script>
-<script type="text/javascript">hljs.initHighlightingOnLoad();</script>
-
-<p><a href="./">CPROVER Manual TOC</a></p>
-
-<h2>Automatic Test Suite Generation with CBMC</h2>
-
-<h3>A Small Tutorial with A Case Study</h3>
-
-<p class="justified">
-We assume that CBMC is installed on your system. If not so, follow
-<a href="installation-cbmc.shtml">these instructions</a>.</p>
-
-<p class="justified">
-CBMC can be used to automatically generate test cases that satisfy a certain <a
-href="https://en.wikipedia.org/wiki/Code_coverage">code coverage</a>
-criterion.  Common coverage criteria include branch coverage, condition
-coverage and <a
-href="https://en.wikipedia.org/wiki/Modified_condition/decision_coverage">Modified
-Condition/Decision Coverage (MC/DC)</a>.  Among others, MC/DC is required
-by several avionics software development guidelines to ensure adequate testing
-of safety critical software.  Briefly, in order to satisfy MC/DC,
-for every conditional statement containing boolean decisions, each Boolean
-variable should be evaluated one time to "true" and one time to "false",
-in a way that affects the outcome of the decision.
-</p>
-
-<p class="justified">
-In the following, we are going to demonstrate how to apply the test suite
-generation functionality in CBMC, by means of a case study.  The program
-<a href="pid.c">pid.c</a> is an excerpt from a real-time embedded benchmark <a
-href="https://www.irit.fr/recherches/ARCHI/MARCH/rubrique.php3?id_rubrique=97">PapaBench</a>,
-and implements part of a fly-by-wire autopilot for an Unmanned Aerial Vehicle (UAV).
-It is adjusted mildly for our purposes.
-</p>
-
-<p class="justified">
-The aim of function <code>climb_pid_run</code> is to control the vertical climb of the UAV.
-Details on the theory behind this operation are documented in the <a
-href="https://wiki.paparazziuav.org/wiki/Theory_of_Operation">wiki</a> for the Paparazzi UAV project.
-The behaviour of this simple controller, supposing that the desired speed is 0.5 meters per second, 
-is plotted in the Figure below.
-</p>
-
-<center>
-  <!--<embed src="pid.pdf" width="400px" height="250px" /> -->
-<img src="pid.png" width="400px" height="250px" alt="The pid controller">
-
-</center>
-
-<pre><code class="c numbered">01: // CONSTANTS:
-02: #define MAX_CLIMB_SUM_ERR 10
-03: #define MAX_CLIMB 1
-04:
-05: #define CLOCK 16
-06: #define MAX_PPRZ (CLOCK*600)
-07:
-08: #define CLIMB_LEVEL_GAZ 0.31
-09: #define CLIMB_GAZ_OF_CLIMB 0.75
-10: #define CLIMB_PITCH_OF_VZ_PGAIN 0.05
-11: #define CLIMB_PGAIN -0.03
-12: #define CLIMB_IGAIN 0.1
-13:
-14: const float pitch_of_vz_pgain=CLIMB_PITCH_OF_VZ_PGAIN;
-15: const float climb_pgain=CLIMB_PGAIN;
-16: const float climb_igain=CLIMB_IGAIN;
-17: const float nav_pitch=0;
-18:
-19: /** PID function INPUTS */
-20: // The user input: target speed in vertical direction
-21: float desired_climb;
-22: // Vertical speed of the UAV detected by GPS sensor
-23: float estimator_z_dot;
-24:
-25: /** PID function OUTPUTS */
-26: float desired_gaz;
-27: float desired_pitch;
-28:
-29: /** The state variable: accumulated error in the control */
-30: float climb_sum_err=0;
-31:
-32: /** Computes desired_gaz and desired_pitch */
-33: void climb_pid_run() 
-34: {
-35:
-36:   float err=estimator_z_dot-desired_climb;
-37:
-38:   float fgaz=climb_pgain*(err+climb_igain*climb_sum_err)+CLIMB_LEVEL_GAZ+CLIMB_GAZ_OF_CLIMB*desired_climb;
-39:
-40:   float pprz=fgaz*MAX_PPRZ;
-41:   desired_gaz=((pprz>=0 && pprz<=MAX_PPRZ) ? pprz : (pprz>MAX_PPRZ ? MAX_PPRZ : 0));
-42:
-43:   /** pitch offset for climb */
-44:   float pitch_of_vz=(desired_climb>0) ? desired_climb*pitch_of_vz_pgain : 0;
-45:   desired_pitch=nav_pitch+pitch_of_vz;
-46:
-47:   climb_sum_err=err+climb_sum_err;
-48:   if (climb_sum_err>MAX_CLIMB_SUM_ERR) climb_sum_err=MAX_CLIMB_SUM_ERR;
-49:   if (climb_sum_err<-MAX_CLIMB_SUM_ERR) climb_sum_err=-MAX_CLIMB_SUM_ERR;
-50:
-51: }
-52:
-53: int main()
-54: {
-55:
-56:   while(1)
-57:   {
-58:     /** Non-deterministic input values */ 
-59:     desired_climb=nondet_float();
-60:     estimator_z_dot=nondet_float();
-61:
-62:     /** Range of input values */ 
-63:     __CPROVER_assume(desired_climb>=-MAX_CLIMB && desired_climb<=MAX_CLIMB);
-64:     __CPROVER_assume(estimator_z_dot>=-MAX_CLIMB && estimator_z_dot<=MAX_CLIMB);
-65:
-66:     __CPROVER_input("desired_climb", desired_climb);
-67:     __CPROVER_input("estimator_z_dot", estimator_z_dot);
-68:
-69:     climb_pid_run();
-70:
-71:     __CPROVER_output("desired_gaz", desired_gaz);
-72:     __CPROVER_output("desired_pitch", desired_pitch);
-73:
-74:   }
-75:
-76:   return 0;
-77: }
-</code></pre>
-
-<p class="justified">
-In order to test the PID controller, we construct a main control loop,
-which repeatedly invokes the function <code>climb_pid_run</code> (line 69). 
-This PID function has two input variables: the desired speed <code>desired_climb</code>
-and the estimated speed <code>estimated_z_dot</code>.
-In the beginning of each loop iteration, values of the inputs are assigned non-deterministically.
-Subsequently, the <code>__CPROVER_assume</code> statement in lines 63 and 64 guarantees that
-both values are bounded within a valid range.
-The <code>__CPROVER_input</code> and <code>__CPROVER_output</code> will help clarify the inputs
-and outputs of interest for generating test suites.
-</p>
-
-<p class="justified">
-To demonstrate the automatic test suite generation in CBMC,
-we call the following command and we are going to explain the command line options one by one.
-</p>
-
-<pre><code>cbmc pid.c --cover mcdc --unwind 6 --xml-ui
-</code></pre>
-
-<p class="justified">
-The option <code>--cover mcdc</code> specifies the code coverage criterion.
-There are four conditional statements in the PID function: in line 41, line 44, 
-line 48 and line 49. 
-To satisfy MC/DC, the test suite has to meet multiple requirements.
-For instance, each conditional statement needs to evaluate to <em>true</em> and <em>false</em>.
-Consider the condition <code>"pprz>=0 && pprz<=MAX_PPRZ"</code> in line 41. CBMC
-instruments three coverage goals to control the respective evaluated results of <code>"pprz>=0"</code> and 
-<code>"pprz<=MAX_PPRZ"</code>. 
-We list them in below and they satisfy the MC/DC rules.
-Note that <code>MAX_PPRZ</code> is defined as 16 * 600 in line 06 of the program.
-</p>
-
-<pre>
-<code>!(pprz >= (float)0) && pprz <= (float)(16 * 600)  id="climb_pid_run.coverage.1"
-pprz >= (float)0 && !(pprz <= (float)(16 * 600))  id="climb_pid_run.coverage.2"
-pprz >= (float)0 && pprz <= (float)(16 * 600)     id="climb_pid_run.coverage.3"
-</code></pre>
-
-<p class="justified">
-The "id" of each coverage goal is automatically assigned by CBMC.  For every
-coverage goal, a test suite (if there exists) that <!-- the program execution that-->
-satisfies such a goal is printed out in XML format, as the parameter
-<code>--xml-ui</code> is given.  Multiple coverage goals can share a
-test suite, when the corresponding execution of the program satisfies all these
-goals at the same time.  <!--Each trace corresponds to a test case.-->
-</p>
-
-<p class="justified">
-In the end, the following test suites are automatically generated for testing the PID controller.
-A test suite consists of a sequence of input parameters that are
-passed to the PID function <code>climb_pid_run</code> at each loop iteration. 
-For example, Test 1 covers the MC/DC goal with id="climb_pid_run.coverage.1".
-The complete output from CBMC is in
-<a href="pid_test_suites.xml">pid_test_suites.xml</a>, where every test suite and the coverage goals it is for
-are clearly described.
-
-<pre><code>Test suite:
-Test 1. 
-  (iteration 1) desired_climb=-1.000000f, estimator_z_dot=1.000000f
-
-Test 2.
-  (iteration 1) desired_climb=-1.000000f, estimator_z_dot=1.000000f 
-  (iteration 2) desired_climb=1.000000f, estimator_z_dot=-1.000000f 
-
-Test 3.
-  (iteration 1) desired_climb=0.000000f, estimator_z_dot=-1.000000f
-  (iteration 2) desired_climb=1.000000f, estimator_z_dot=-1.000000f
-
-Test 4.
-  (iteration 1) desired_climb=1.000000f, estimator_z_dot=-1.000000f
-  (iteration 2) desired_climb=1.000000f, estimator_z_dot=-1.000000f
-  (iteration 3) desired_climb=1.000000f, estimator_z_dot=-1.000000f
-  (iteration 4) desired_climb=1.000000f, estimator_z_dot=-1.000000f
-  (iteration 5) desired_climb=0.000000f, estimator_z_dot=-1.000000f
-  (iteration 6) desired_climb=1.000000f, estimator_z_dot=-1.000000f
-
-Test 5.
-  (iteration 1) desired_climb=-1.000000f, estimator_z_dot=1.000000f
-  (iteration 2) desired_climb=-1.000000f, estimator_z_dot=1.000000f
-  (iteration 3) desired_climb=-1.000000f, estimator_z_dot=1.000000f
-  (iteration 4) desired_climb=-1.000000f, estimator_z_dot=1.000000f
-  (iteration 5) desired_climb=-1.000000f, estimator_z_dot=1.000000f
-  (iteration 6) desired_climb=-1.000000f, estimator_z_dot=1.000000f
-</code></pre>
-
-<p class="justified">
-The option <code>--unwind 6</code> unwinds the loop inside the main
-function body six times. In order to achieve the complete coverage on all the instrumented goals 
-in the PID function <code>climb_pid_run</code>, the loop must be unwound sufficient enough times.
-For example, <code>climb_pid_run</code> needs to be called at least six times for evaluating the 
-condition <code>climb_sum_err>MAX_CLIMB_SUM_ERR</code> in line 48 to <em>true</em>.
-This corresponds to the Test 5.
-An introduction to the use of loop unwinding can be found
-in <a href="cbmc-loops.shtml">Understanding Loop Unwinding</a>.
-</p>
-
-<p class="justified">
-In this small tutorial, we present the automatic test suite generation
-functionality of CBMC, by applying the MC/DC code coverage criterion to a
-PID controller case study.  In addition to <code>--cover mcdc</code>, other
-coverage criteria like <code>branch</code>, <code>decision</code>,
-<code>path</code> etc.  are also available when calling CBMC.
-</p>
-
-<h3>Coverage Criteria</h3>
-
-<p class="justified">
-The table below summarizes the coverage criteria that CBMC supports.
-</p>
-
-<table class="fancy">
-
-<tr><th>Criterion</th><th>Definition</th></tr>
-
-<tr><td>assertion</td>
-<td>For every assertion, generate a test that reaches it</td></tr>
-
-<tr><td class="alt">location</td>
-<td class="alt">For every location, generate a test that reaches it</td></tr>
-
-<tr><td>branch</td>
-<td>Generate a test for every branch outcome</td></tr>
-
-<tr><td class="alt">decision</td>
-<td class="alt">Generate a test for both outcomes of every Boolean expression
-that is not an operand of a propositional connective</td></tr>
-
-<tr><td>condition</td>
-<td>Generate a test for both outcomes of every Boolean expression</td></tr>
-
-<tr><td class="alt">mcdc</td>
-<td class="alt">Modified Condition/Decision Coverage (MC/DC)</td></tr>
-
-<tr><td>path</td>
-<td>Bounded path coverage</td></tr>
-
-<tr><td class="alt">cover</td>
-<td class="alt">Generate a test for every <code>__CPROVER_cover</code> statement
-</td></tr>
-
-</table>
-
-<!--#include virtual="footer.inc" -->

doc/html-manual/cprover-source.shtml

@@ -1,877 +0,0 @@
-<!--#include virtual="header.inc" -->
-
-<link rel="stylesheet" href="highlight/styles/default.css">
-<script src="highlight/highlight.pack.js" type="text/javascript"></script>
-<script type="text/javascript">hljs.initHighlightingOnLoad();</script>
-
-<p><a href="./">CPROVER Manual TOC</a></p>
-
-<h2>The CPROVER Source Code Reference</h2>
-
-<p class="justified">
-The following sections provide an introduction for anybody who
-wishes to modify CBMC or build new tools on top of the APIs used
-by CBMC. They summarize key components, data structures and APIs
-that are used to build the CPROVER tools.
-</p>
-
-<h3>Source Code Availability and Compilation</h3>
-
-<p class="justified">
-The most recent source code of CBMC and the CPROVER infrastructure can be obtained
-via git at <a
-href="https://github.com/diffblue/cbmc.git">https://github.com/diffblue/cbmc.git</a>.
-Tar balls for releases are available at <a
-href="https://github.com/diffblue/cbmc/releases">https://github.com/diffblue/cbmc/releases</a>.
-</p>
-
-<p class="justified">
-Detailed instructions on how to build CBMC from source are given
-in the file <a href="https://raw.githubusercontent.com/diffblue/cbmc/master/COMPILING">COMPILING</a>.
-</p>
-
-<h3>Components</h3>
-
-<center><img src="c_to_ir.svg" width=500></center>
-<center>From C source code file to CPROVER's IR</center>
-
-<p class="justified">
-The sources of the C frontend are located in the "src/ansi-c" directory.  It
-uses a standard Flex/Bison setup for scanning and parsing the files. The
-Flex scanner produces a token sequence, which is turned into a tree
-representation of the input program using the Bison grammar.  The
-typechecker subsequently annotates this parse tree with types and generates
-a symbol table.  The symbol table is a map from identifiers (functions,
-variables and types) to their definitions.
-</p>
-
-<p class="justified">
-The following example illustrates how to use the frontend for parsing files and
-for translating them into a symbol table.  A call to <i>parse</i> generates
-the parse tree of the program.  The conversion into the symbol table is
-performed during type checking, which is done by a call to the
-<i>typecheck</i> method.  The symbol table is a map from identifiers to the
-<i>symbolt</i> data structure.
-</p>
-
-<pre><code class="c++">#include &lt;iostream&gt;
-#include &lt;fstream&gt;
-#include &lt;sstream&gt;
-#include &lt;string&gt;
-
-#include &lt;ansi-c/ansi_c_language.h&gt;
-#include &lt;util/cmdline.h&gt;
-#include &lt;util/config.h&gt;
-
-int main(int argc, const char* argv[])
-{
-   // Command line: parse  -I incl_dir file1 ...
-   cmdlinet cmdl;
-   cmdl.parse(argc, argv, "I:");
-
-   config.init();
-
-   if(cmdl.isset('I'))	
-     config.ansi_c.include_paths=cmdl.get_values('I');
-
-   // Set language to C
-   std::auto_ptr&lt;languaget&gt; clang=new_ansi_c_language();
-
-   // Symbol table
-   symbol_tablet my_symbol_table;
-
-   for(const auto & arg : cmdl.args)
-   {
-     // Source code stream
-     std::ifstream in(arg.c_str());	
-
-     // Parse
-     clang-&gt;parse(in, "", std::cerr);
-
-     // Typecheck
-     clang-&gt;typecheck(my_symbol_table, arg, std::cerr);
-  }
-
-  // Do some final adjustements
-  clang-&gt;final(my_symbol_table, std::cerr);
-
-  my_symbol_table.show(std::cout);
-
-  return 0;
-}
-</code></pre>
-
-<p class="justified">
-The parse trees are implemented using a class called <i>irept</i>.  Its
-declaration and definiton can be found in the files "src/util/irep.h" and
-"src/util/irep.cpp", respectively.
-</p>
-
-<p class="justified">
-The excerpt below gives some details of the class <i>irept</i>:
-</p>
-
-<pre><code class="c++">class irept
-{
-public:
-  typedef std::vector&lt;irept&gt; subt;
-  typedef std::map&lt;irep_name_string, irept&gt; named_subt;
-  ...
-
-public:
-  class dt
-  {
-  public:
-    unsigned ref_count;
-    dstring data;
-    named_subt named_sub;
-    named_subt comments;
-    subt sub;
-    ...
-  };
-
-protected:
-  dt *data;
-  ...
-};
-</code></pre>
-
-<p class="justified">
-Every node of any tree is an object of class <i>irept</i>. Each node has a
-pointer to an object of class <i>dt</i>. The <i>dt</i> objects are used
-for storing the actual content of nodes. Objects of class <i>dt</i> are
-dynamically allocated and can be shared between nodes. A reference-counter
-mechanism is implemented to automatically free unreachable <i>dt</i>
-objects. A shallow copy of a tree is an <i>O</i>(1) operation.
-</p>
-
-<p class="justified">
-The field <i>data</i> of class <i>dt</i> is a (hashed) string
-representing the label of the nodes. The fields <i>named_sub</i>,
-<i>comments</i> and <i>sub</i> are links to childs. Edges are either
-labeled with a string or ordered. The string-labeled edges are stored in the
-map <i>comments</i> if their first character is '#'. Otherwise, they are
-stored in the map <i>named_sub</i>. The labels of edges are unique for a
-given node; however, their ordering is not preserved. The field <i>sub</i>
-is a vector of nodes that is used for storing the ordered children. The order
-of edges of this kind is preserved during copy.
-</p>
-
-<center><img src="ireptree.svg" width=350></center>
-<center>Tree for the expression <i>a+b</i> with <i>int a; char
-b;</i>.</center>
-
-<h4>Interface of Class <i>irept</i></h4>
-
-<h5>id</h5>
-
-<pre><code class="c++">const irep_idt &amp;id();
-void id(const irep_idt &amp;_data);
-</code></pre>
-
-<p class="justified">
-The first method returns a constant reference to the label of the node. The
-second method sets the label of the node.
-</p>
-
-<h5>is_nil and is_not_nil</h5>
-
-<pre><code class="c++">virtual bool is_nil() const;
-virtual bool is_not_nil() const;
-</code></pre>
-
-<p class="justified">
-The first  method returns true if the label of the node is equal to  "nil".
-The second method returns false if the label of the node is equal to "nil".
-</p>
-
-<h5>find, add and get</h5>
-
-<pre><code class="c++">const irept &amp;find(const irep_namet &amp;name) const;
-irept &amp;add(const irep_namet &amp;name);
-const irep_idt &amp;get(const irep_namet &amp;name) const;
-</code></pre>
-
-<ol>
-
-<li>The first method looks for an edge with label <i>name</i>
-and returns the corresponding child. If no edge with label <i>name</i>
-is found, then <i>nil_rep</i> is returned.</li>
-
-<li>The second method does the same as the first except that if
-no edge with label <i>name</i> if found, then a new child is created
-and returned.
-</li>
-
-<li>The third method does the same as the first except that the label
-of the child is returned (instead of a reference).
-If no edge with label <i>name</i> is found, then an empty
-string is returned.
-</li>
-
-</ol>
-
-<h5>set</h5>
-
-<pre><code class="c++">void set(const irep_namet &amp;name,
-         const irep_idt &amp;value);
-void set(const irep_namet &amp;name, const long value);
-void set(const irep_namet &amp;name, const irept &amp;irep);
-</code></pre>
-
-<p class="justified">
-These methods create a new edge with label <i>name</i>.
-</p>
-
-<p class="justified">
-If the second argument is an object of class <i>irept</i>, then it is
-assigned to the new child.
-
-<p class="justified">
-If the second argument is a string, then it is set as node-label of the new child.
-
-<p class="justified">
-If the second argument is a number, then it is converted to a
-string and set as node-label of the new child.
-
-<h5>remove</h5>
-
-<pre><code class="c++">void remove(const irep_namet &amp;name);
-</code></pre>
-
-<p class="justified">
-This method looks for an edge with label <i>name</i>
-and removes it.
-
-<h5>move_to_sub and move_to_named_sub</h5>
-
-<pre><code class="c++">void move_to_sub(irept &amp;irep);
-void move_to_named_sub(const irep_namet &amp;name, irept &amp;irep);
-</code></pre>
-
-<p class="justified">
-The first method creates a new ordered edge with a child equal to
-<i>irep</i>. Then it sets <i>irep</i> to <i>nil</i>. The index of the
-edge is equal to the size of vector <i>sub</i> before the call.
-</p>
-
-<p class="justified">
-The second method does the same but for labeled edges.
-</p>
-
-<h5>swap</h5>
-
-<pre><code class="c++">void swap(irept &amp;irep);
-</code></pre>
-
-<p class="justified">
-Exchange the content of the invoked node with the one of <i>irep</i>.
-</p>
-
-<h5>make_nil</h5>
-
-<pre><code class="c++">void make_nil();
-</code></pre>
-
-<p class="justified">
-Set the label of the node to "nil" and remove all outgoing edges.
-</p>
-
-<h5>get_sub and get_named_sub and get_comments</h5>
-
-<pre><code class="c++">const subt &amp;get_sub();
-const named_subt &amp;get_named_sub();
-const named_subt &amp;get_comments();
-</code></pre>
-
-<p class="justified">
-Return a constant reference to
-<i>sub</i>, <i>named_sub</i>, and <i>comments</i>,  respectively.
-</p>
-
-<h3>Types</h3>
-
-<p class="justified">
-The class <i>typet</i> inherits from <i>irept</i>. Types may have
-subtypes. This is modeled with two edges named "subtype" and "subtypes". The
-class <i>typet</i> only add specialized methods for accessing the subtype
-information to the interface of <i>irept</i>.
-</p>
-
-<h4>Interface of class <i>typet</i></h4>
-
-<h5>has_subtype and has_subtypes</h5>
-
-<pre><code class="c++">bool has_subtype() const;
-bool has_subtypes() const;
-</code></pre>
-
-<p class="justified">
-The first method returns true if the a subtype node exists. is not
-<i>nil</i>. The second method returns true is a subtypes node exists.
-</p>
-
-<h5>subtype and subtypes</h5>
-
-<pre><code class="c++">typet &amp;subtype();
-typest &amp;subtypes();
-</code></pre>
-
-<p class="justified">
-The first method returns a reference to the 'subtype' node.
-The second method returns a reference to the vector of subtypes.
-</p>
-
-<h4>Subtypes of <i>typet</i></h4>
-
-<p class="justified">
-A number of subtypes of <code>typet</code> exist which allow convenient
-creation and manipulation of <code>typet</code> objects for special types.
-</p>
-
-<table>
-<tr><th>Class</th><th>Description</th></tr>
-
-<tr><td valign=top><code>bool_typet</code></td>
-<td>Boolean type</td></tr>
-
-<tr><td valign=top><code>symbol_typet</code></td>
-<td>Symbol type. Has edge "identifier" to a string value, which can be accessed with <code>get_identifier</code> and <code>set_identifier</code>.</td></tr>
-
-<tr><td valign=top><code>struct_typet</code>, <code>union_typet</code></td>
-<td>Represent a struct, resp.&nbsp;union types. Convenience functions to access components <code>components()</code>.</td></tr>
-
-<tr><td valign=top><code>code_typet</code></td>
-<td>The type of a function/procedure. Convenience functions to access <code>arguments()</code> and <code>return_type()</code>. </td></tr>
-
-<tr><td valign=top><code>array_typet</code></td>
-<td>Convenience function <code>size()</code> to access size of the array.</td></tr>
-
-<tr><td valign=top><code>pointer_typet</code></td>
-<td>Pointer type, subtype stores the type of the object pointed to.</td></tr>
-
-<tr><td valign=top><code>reference_typet</code></td>
-<td>Represents a reference type, subtype stores the type of the object referenced to. </td></tr>
-
-<tr><td valign=top><code>bv_typet</code></td>
-<td>Represents a bit vector type with variable width.</td></tr>
-
-<tr><td valign=top><code>fixed_bv_typet</code></td>
-<td>Represents a bit vector that encodes a fixed-point number.</td></tr>
-
-<tr><td valign=top><code>floatbv_typet</code></td>
-<td>Represents a bit vector that encodes a floating-point number.</td></tr>
-
-<tr><td valign=top><code>string_typet</code></td>
-<td>Represents a string type.</td></tr>
-
-</table>
-
-<h3>Source Locations</h3>
-
-<p class="justified">
-The class <i>source_locationt</i> inherits from the class <i>irept</i>.  It
-is used to store locations in text files.  It adds specialized methods to
-manipulate the edges named "file", "line", "column", "function".
-</p>
-
-<h3>Expressions</h3>
-
-<p class="justified">
-The class <i>exprt</i> inherits from class <i>irept</i>. Expressions
-have operands and a type. This is modeled with ordered edges for the
-operands and an edge labeled"type", respectively. The class <i>exprt</i>
-only adds specialized methods for accessing operands and type information
-to the interface of <i>irept</i>.
-</p>
-
-<center><img src="expr.svg" width=150></center>
-<center>Representation of a binary expression</center>
-
-<h4>Interface of class <i>exprt</i></h4>
-
-<h5>constructors</h5>
-
-<pre><code class="c++">explicit exprt(const irep_idt &amp;id);
-</code></pre>
-
-<p class="justified">
-Creates an <i>exprt</i> object with a given label and no type.
-</p>
- 
-<pre><code class="c++">exprt(const irep_idt &amp;id, const typet &amp;type);
-</code></pre>
-
-<p class="justified">
-Creates an <i>exprt</i> object with a given label and type.
-</p>
-
-<h5>type</h5>
-
-<pre><code class="c++">const typet &amp;type() const;
-typet &amp;type();
-</code></pre>
-
-<p class="justified">
-Return a reference to the 'type' node
-</p>
-
-<h5>has_operands</h5>
-
-<pre><code class="c++">bool has_operands() const;
-</code></pre>
-
-<p class="justified">
-Return true if the expression has at least one operand.
-</p>
-
-<h5>operands</h5>
-
-<pre><code class="c++">const operandst &amp;operands() const;
-</code></pre>
-
-<p class="justified">
-Return a reference to the vector of operands.
-</p>
-
-<pre><code class="c++">const exprt &amp;op0();
-const exprt &amp;op1();
-const exprt &amp;op2();
-const exprt &amp;op3();
-exprt &amp;op0();
-exprt &amp;op1();
-exprt &amp;op2();
-exprt &amp;op3();
-</code></pre>
-
-<p class="justified">
-Return a reference to a specific operand. Avoid calling
-if the operand does not exist. 
-</p>
-
-<h5>Constructing common expressions</h5>
-
-<pre><code class="c++">void make_true();
-void make_false();
-void make_bool(bool value);
-</code></pre>
-
-<p class="justified">
-Turn the current <i>exprt</i> instance into a expression of type "bool"
-with label "constant" and a single edge labeled "value", which points to
-a new node with label either "true" or "false".
-</p>
-
-<pre><code class="c++">void make_typecast(const typet &amp;_type);
-</code></pre> 
-
-<p class="justified">
-Turns the current <i>exprt</i> instance into a typecast.  The old value of
-the instance is appended as the single operand of the typecast, i.e., the
-result is a typecast-expression of the old expression to the indicated type.
-</p>
-
-<pre><code class="c++">void make_not();
-</code></pre> 
-
-<p class="justified">
-Turns the current <i>exprt</i> instance into an expression with label
-"not" of the same type as the original expression.  The old value of the
-instance is appended as the operand of the "not"-node.  If the original
-expression is of type "bool", the result represents the negation of the
-original expression with the following simplifications possibly applied:
-</p>
-
-<ul>
-<li>&not; &not; f = f</li>
-<li>&not; <i>true</i> = <i>false</i></li>
-<li>&not; <i>false</i> = <i>true</i></li>
-</ul>
-
-<pre>
-void negate();
-</pre> 
-
-<p class="justified">
-Turns the current <i>exprt</i> instance into a negation of itself, depending
-on its type:
-</p>
-
-<ul>
-
-<li>For boolean expressions, <code>make_not</code> is called.</li>
-
-<li>For integers, the current instance is turned into a numeric negation
-expression "unary-" of its old value.  Chains of "unary-" nodes and
-negations of integer constants are simplified.</li>
-
-<li>For all other types, <code>irept::make_nil</code> is called.</li>
-
-</ul>
-
-<pre><code class="c++">bool sum(const exprt &amp;expr);
-bool mul(const exprt &amp;expr);
-bool subtract(const exprt &amp;expr);
-</code></pre> 
-
-<p class="justified">
-Expect the "this" object and the function argument to be constants of the
-same numeric type.  Turn the current <code>exprt</code> instance into a
-constant expression of the same type, whose "value" edge points to the
-result of the sum, product, or difference of the two expressions.  If the
-operation fails for some reason (e.g., the types are different),
-<code>true</code> is returned.
-</p>
-
-<h5>Testing common expressions</h5>
- 
-<pre><code class="c++">bool is_constant() const;
-</code></pre> 
-
-<p class="justified">
-Returns true if the expression label is "constant".
-</p>
-
-<pre><code class="c++">bool is_boolean() const;
-</code></pre> 
-
-<p class="justified">
-Returns true if the label of the type is "bool".
-
-<pre><code class="c++">bool is_false() const;
-bool is_true() const;
-</code></pre> 
-
-<p class="justified">
-The first function returns true if the expression is a boolean constant with
-value "false".  The second function returns true for any boolean constant
-that is not of value "false".
-</p>
-
-<pre><code class="c++">bool is_zero() const;
-bool is_one() const;
-</code></pre> 
-
-<p class="justified">
-The first function returns true if the expression represents a zero numeric
-constant, or if the expression represents a null pointer. The second
-function returns true if the expression represents a numeric constant with
-value "1".
-</p>
-
-<h4>Subtypes of <i>exprt</i></h4>
-
-<p class="justified">
-A number of subtypes of <code>exprt</code> provide further convenience functions
-for edge access or other specialized behaviour:
-</p>
-
-<table>
-
-<tr><th>Class</th><th>Description</th></tr>
-
-<tr><td valign=top><code>transt</code></td>
-<td valign=top>Represents an SMV-style transition system with invariants
-<code>invar()</code>, initial state <code>init()</code> and transition
-function <code>trans()</code>.</td>
-</tr>
-
-<tr><td valign=top><code>true_exprt</code></td>
-<td valign=top>Boolean constant true expression.</td>
-</tr>
-
-<tr><td valign=top><code>false_exprt</code></td>
-<td valign=top>Boolean constant false expression.</td>
-</tr>
-
-<tr><td valign=top><code>symbol_exprt</code></td>
-<td valign=top>Represents a symbol (e.g., a variable occurrence), convenience function for manipulating "identifier"-edge <code>set_identifier</code> and <code>get_identifier</code></td>
-</tr>
-
-<tr><td valign=top><code>predicate_exprt</code></td>
-<td valign=top>Convenience constructors to create expressions of type "bool".</td>
-</tr>
-
-<tr><td valign=top><code>binary_relation_exprt : predicate_exprt</code></td>
-<td valign=top>Convenience functions to create and manipulate binary expressions of type "bool".</td>
-</tr>
-
-<tr><td valign=top><code>equality_exprt : binary_relation_exprt</code></td>
-<td valign=top>Convenience functions to create and manipulate equality expressions such as "a == b".</td>
-</tr>
-
-<tr><td valign=top><code>ieee_float_equal_exprt : binary_relation_exprt</code></td>
-<td valign=top>Convenience functions to create and manipulate equality expressions between floating-point numbers.
-</td>
-</tr>
-
-<tr><td valign=top><code>index_exprt</code></td>
-<td valign=top>Represents an array access expression such as "a[i]". Convenience functions <code>array()</code> and <code>index()</code> for accessing the array expressions and indexing expression.</td>
-</tr>
-
-<tr><td valign=top><code>typecast_exprt</code></td>
-<td valign=top>Represents a cast to the type of the expression.</td>
-</tr>
-
-<tr><td valign=top> 
-<code>and_exprt</code>,
-<code>implies_exprt</code>,
-<code>or_exprt</code>,
-<code>not_exprt</code></td>
-<td valign=top>Representations of logical operators with convenience constructors.</td>
-</tr>
-
-<tr><td valign=top><code>address_of_exprt</code></td>
-<td>Representation of a C-style <code>&amp;a</code> address-of operation. Convenience function <code>object()</code> for accessing operand.</td>
-</tr>
-
-<tr><td valign=top><code>dereference_exprt</code></td>
-<td>Representation of a C-style <code>*a</code> pointer-dereference operation. Convenience function <code>object()</code> for accessing operand.</td>
-</tr>
-
-<tr><td valign=top><code>if_exprt</code></td>
-<td>Representation of a conditional expresion, with convenience functions <code>cond()</code>, <code>true_case()</code> and <code>false_case()</code> for accessing operands.</td>
-</tr>
-
-<tr><td valign=top><code>member_exprt</code></td>
-<td>Represents a <code>some_struct.some_field</code> member access.</td>
-</tr>
-
-<tr><td valign=top><code>codet</code></td>
-<td>Represents a segment of code.</td>
-</tr>
-
-</table>
-
-<h3>Symbols and the Symbol Table</h3>
-
-<h4>Symbol</h4>
-
-<p class="justified">
-A symbol is an object of class <code>symbolt</code>. This class
-is declared in "util/symbol.h". The code below shows a partial
-declaration of the interface:
-</p>
-
-<pre><code class="c++">class symbolt
-{
-public:
-  typet type;
-  exprt value;
-  std::string name;
-  std::string base_name;
-  ...
-};
-</code></pre>
-
-<p class="justified">
-Symbol names are unique. Scopes are handled by adding prefixes
-to symbols:
-</p>
-
-<pre><code class="c++">int main(int argc, char* argv[]) {
-	
-	               // Symbol name: c::main::0::alice
-   char alice = 0;     // Symbol base: alice
-   
-   {
-	               // Symbol name: c::main::1::alice
-       int alice = 0;  // Symbol base: alice
-   }
-}</code></pre>
-
-<h4>Symbol Table</h4>
-
-<p class="justified">
-A symbol table is an object of class <code>contextt</code>. This class
-is declared in "util/context.h". The code below shows a partial
-declaration of the interface:
-</p>
-
-<pre><code class="c++">class symbol_tablett
-{
-public:
-                                 // Insert the symbol
-  bool add(const symbolt &amp;symb);
-                                 // Insert symb into the
-                                 // table and erase it.
-                                 // New_symbol points to the
-                                 // newly inserted element.
-  bool move(symbolt &amp;symbol, symbolt *&amp;new_symbol);
-
-                                 // Insert symb into the
-                                 // table. Then symb is erased.
-  bool move(symbolt &amp;syb);
-
-                                 // Return the entry of the
-                                 // symbol with given name.
-  const irept &amp;value(const std::string &amp;name) const;
-};
-</code></pre>
-
-<h2>Goto Programs</h2>
-
-<p class="justified">
-Goto programs are a representation of the control flow graph of a program
-that uses only guarded goto and assume statements to model non-sequential
-flow.  The main definition can be found in
-"src/goto-programs/goto_program_template.h", which is a template class.  The
-concrete instantiation of the template that is used in the framework can be
-found in "src/goto-programs/goto_program.h".  A single instruction in a goto
-program is represented by the class <i>goto_programt::instructiont</i>
-whose definition can be found again in
-"goto-programs/goto_program_template.h".
-</p>
-
-<p class="justified">
-In the class <code>goto_programt</code>, the control flow graph is represented
-as a mixture of sequential transitions between nodes, and non-sequential
-transitions at goto-nodes.  The sequential flow of the program is captured
-by the list <code>instructions</code> that is a field of the class
-<code>goto_programt</code>.  Transitions via goto statements are represented in
-the list <code>targets</code>, which is a field of the class
-<code>goto_programt::instructiont</code>, i.e., each goto-instruction carries a
-list of possible jump destinations.  The latter list <code>targets</code> is a
-list of iterators which point to elements of the list <code>instructions</code>. 
-An illustration is given in the figure below.
-</p>
-
-<center><img src="goto_program.svg" width=500></center>
-<center>Representation of program flow in <i>goto_programt</i></center>
-
-<p class="justified">
-Instructions can have a number of different types as represented by
-<code>enum goto_program_instruction_typet</code> and can be accessed via the
-field <code>type</code> in <code>instructiont</code>.  These include:
-</p>
-
-<table>
-<tr><td valign=top><code>GOTO</code></td>
-<td>Represents a non-deterministic branch to the instructions given in the
-list <code>targets</code>.  Goto statements are guarded, i.e., the
-non-deterministic branch is only taken if the expression in
-<code>guard</code> evaluates to true, otherwise the program continues
-sequentially.  Guarded gotos can be used, for example, to model if
-statements.  The guard is then set to the negated condition of the
-statement, and goto target is set to bypass the conditionally executed code
-if this guard evaluates to true.
-</td>
-</tr>
-
-<tr><td valign=top><code>ASSUME</code></td>
-<td>An assumption statement that restricts viable paths reaching the
-instruction location to the ones that make the expression <code>guard</code>
-evaluate to true.</td>
-</tr>
-
-<tr><td valign=top><code>ASSERT</code></td>
-<td>An assertion whose <code>guard</code> is checked for validity when the instruction is
-reached.</td>
-</tr>
-
-<tr><td valign=top><code>RETURN</code></td>
-<td>A return statement in a function.</td>
-</tr>
-
-<tr><td valign=top><code>END_FUNCTION</code></td>
-<td>Denotes the end of a function.</td>
-</tr>
-
-<tr><td valign=top><code>ASSIGN</code></td>
-<td>A variable assignment.</td>
-</tr>
-
-<tr><td valign=top><code>SKIP</code></td>
-<td>No operation.</td>
-</tr>
-
-<tr><td valign=top><code>OTHER</code></td>
-<td>Any operation not covered by <code>enum
-goto_program_instruction_typet</code>.</td>
-</tr>
-
-</table>
-
-<p class="justified">
-A number of convenience functions in <code>instructiont</code>, such as
-<code>is_goto()</code>, <code>is_assume()</code>, etc., simplify type queries. 
-The following code segment gives a partial interface declaration of
-<code>goto_program_template</code> and <code>instructiont</code>.
-</p>
-
-<pre><code class="c++">template &lt;class codeT, class guardT&gt;
-class goto_program_templatet
-{
-public:
-  //list of instruction type
-  typedef std::list&lt;class instructiont&gt; instructionst;
-
-  //a reference to an instruction in the list
-  typedef typename 
-    std::list<class instructiont>::iterator targett;
-
-  //Sequential list of instructions, 
-  //representing sequential program flow
-  instructionst instructions;
-
-  typedef typename 
-    std::map&lt;const_targett, unsigned&gt; target_numberst;
-
-  //A map containing the unique number of each target
-  target_numberst target_numbers;
-
-  //Get the successors of a given instruction 
-  void get_successors(targett target, targetst &amp;successors); 
-
-  ...
-
- 
-  class instructiont
-  {
-  public:
-    codeT code;
-    
-    //identifier of enclosing function
-    irep_idt function;
-    
-    //location in the source file
-    locationt location;
-    
-    //type of instruction?
-    goto_program_instruction_typet type;
-
-    //Guard statement for gotos, assume, assert 
-    guardT guard;
-    
-    //targets for gotos
-    targetst targets;
-   
-    //set of all predecessors (sequential, and gotos)
-    std::set&lt;targett&gt; incoming_edges;
-    
-    // a globally unique number to identify a 
-    // program location. It is guaranteed to be 
-    // ordered in program order within one 
-    // goto_program
-    unsigned location_number;
-    
-    // a globally unique number to identify loops
-    unsigned loop_number;
-    
-    // true if this is a goto jumping back to an 
-    // earlier instruction in the sequential program 
-    // flow
-    bool is_backwards_goto() const;
-  };
-
-}
-</code></pre>
-
-<!--
-<h3>Data Structures</h3>
--->
-
-<!-- <h3>APIs</h3>
--->
-
-<!--#include virtual="footer.inc" -->

doc/html-manual/footer.inc

@@ -1,5 +0,0 @@
-</div> <!-- main -->
-</div> <!-- wrap -->
-
-</body>
-</html>

doc/html-manual/goto-cc-apache.shtml

@@ -1,69 +0,0 @@
-<!--#include virtual="header.inc" -->
-
-<p><a href="./">CPROVER Manual TOC</a></p>
-
-<h2>Build Systems and Libraries</h2>
-
-<h3>Example: Extracting Models from the Apache HTTPD</h3>
-
-<p class="justified">
-The <a href="http://httpd.apache.org/">Apache HTTPD</a> is still the most
-frequently used web server.  Together with the relevant libraries, it
-consists of around 0.4 million lines of C code.  In the following, we show
-how to extract models from Apache HTTPD 2.4.2.
-</p>
-
-<ol>
-
-<li><p class="justified">
-First of all, we download the sources of Apache HTTPD and two supporting
-libraries and uncompress them:</p>
-
-<p>
-&nbsp;&nbsp;<code>lwp-download http://www.mirrorservice.org/sites/ftp.apache.org/apr/apr-1.4.6.tar.bz2</code><br>
-&nbsp;&nbsp;<code>lwp-download http://www.mirrorservice.org/sites/ftp.apache.org/apr/apr-util-1.4.1.tar.bz2</code><br>
-&nbsp;&nbsp;<code>lwp-download http://mirror.catn.com/pub/apache/httpd/httpd-2.4.2.tar.bz2</code><br>
-<br>
-&nbsp;&nbsp;<code>bunzip2 &lt; apr-1.4.6.tar.bz2 | tar x</code><br>
-&nbsp;&nbsp;<code>bunzip2 &lt; apr-util-1.4.1.tar.bz2 | tar x</code><br>
-&nbsp;&nbsp;<code>bunzip2 &lt; httpd-2.4.2.tar.bz2 | tar x</code>
-</p></li>
-
-<li><p class="justified">Now compile
-<a href="gcc-wrap.c">gcc-wrap.c</a> and put the resulting binary
-into a directory that is in your PATH variable:</p>
-<p>
-&nbsp;&nbsp;<code>lwp-download http://www.cprover.org/cprover-manual/gcc-wrap.c</code><br>
-&nbsp;&nbsp;<code>gcc gcc-wrap.c -o gcc-wrap</code><br>
-&nbsp;&nbsp;<code>cp gcc-wrap ~/bin/</code><br>
-</p>
-<p class="justified">This assumes that the directory <code>~/bin</code>
-exists and is in your PATH variable.</p>
-</li>
-
-<li><p>We now build the sources with gcc:</p>
-
-<p>
-&nbsp;&nbsp;<code>(cd apr-1.4.6; ./configure; make CC=gcc-wrap)</code><br>
-&nbsp;&nbsp;<code>(cd apr-util-1.4.1; ./configure --with-apr=../apr-1.4.6 ; make CC=gcc-wrap)</code><br>
-&nbsp;&nbsp;<code>(cd httpd-2.4.2; ./configure --with-apr=../apr-1.4.6 --with-apr-util=../apr-util-1.4.1 ; make CC=gcc-wrap)</code>
-</p>
-
-<li><p class="justified">You can now compile the preprocessed
-source files with goto-cc as follows:</p>
-<p>
-&nbsp;&nbsp;<code>find ./ -name *.i > source-file-list</code><br>
-&nbsp;&nbsp;<code>for a in `cat source-file-list` ; do</code><br>
-&nbsp;&nbsp;<code>&nbsp;&nbsp;goto-cc -c $a -o $a.gb</code><br>
-&nbsp;&nbsp;<code>done</code></p>
-</li>
-
-</ol>
-
-<p class="justified">
-The resulting <code>.gb</code> files can be passed to any
-of the CPROVER tools.
-</p>
-
-<!--#include virtual="footer.inc" -->
-

doc/html-manual/goto-cc-linux.shtml

@@ -1,97 +0,0 @@
-<!--#include virtual="header.inc" -->
-
-<p><a href="./">CPROVER Manual TOC</a></p>
-
-<h2>Build Systems and Libraries</h2>
-
-<h3>Example: Extracting Models from the Linux Kernel</h3>
-
-<p class="justified">
-
-The Linux kernel code consists of more than 11 million lines of low-level C
-and is frequently used to evaluate static analysis techniques.  In the
-following, we show how to extract models from Linux 2.6.39.
-</p>
-
-<ol>
-<li><p class="justified">
-First of all, you will need to make sure you have around 100 GB
-of free disc space available.</p></li>
-
-<li><p class="justified">Download the Kernel sources at
-<a href="http://www.kernel.org/pub/linux/kernel/v2.6/linux-2.6.39.tar.bz2">
-http://www.kernel.org/pub/linux/kernel/v2.6/linux-2.6.39.tar.bz2
-</a>.
-</p></li>
-
-<li><p class="justified">Now do</p>
-<p>
-&nbsp;&nbsp;<code>bunzip2 linux-2.6.39.tar.bz2</code><br>
-&nbsp;&nbsp;<code>tar xvf linux-2.6.39.tar</code><br>
-&nbsp;&nbsp;<code>cd linux-2.6.39</code>
-</p></li>
-
-<li><p class="justified">Now ensure that you can actually
-compile a kernel by doing</p>
-<p>
-&nbsp;&nbsp;<code>make defconfig</code><br>
-&nbsp;&nbsp;<code>make</code></p>
-<p class="justified">
-These steps need to succeed before you can try to extract
-models from the kernel.
-</p></li>
-
-<li><p class="justified">Now compile
-<a href="gcc-wrap.c">gcc-wrap.c</a> and put the resulting binary
-into a directory that is in your PATH variable:</p>
-<p>
-&nbsp;&nbsp;<code>lwp-download http://www.cprover.org/cprover-manual/gcc-wrap.c</code><br>
-&nbsp;&nbsp;<code>gcc gcc-wrap.c -o gcc-wrap</code><br>
-&nbsp;&nbsp;<code>cp gcc-wrap ~/bin/</code><br>
-</p>
-<p class="justified">This assumes that the directory <code>~/bin</code>
-exists and is in your PATH variable.</p>
-</li>
-
-<li><p class="justified">Now change the variable CC in the kernel
-Makefile as follows:</p>
-<p>
-<code>&nbsp;&nbsp;CC = ~/bin/gcc-wrap</code>
-</p>
-</li>
-
-<li><p class="justified">Now do</p>
-<p>
-&nbsp;&nbsp;<code>make clean</code><br>
-&nbsp;&nbsp;<code>make</code></p>
-<p class="justified">
-This will re-compile the kernel, but this time retaining the
-preprocessed source files.
-</p></li>
-
-<li><p class="justified">You can now compile the preprocessed
-source files with goto-cc as follows:</p>
-<p>
-&nbsp;&nbsp;<code>find ./ -name .tmp_*.i > source-file-list</code><br>
-&nbsp;&nbsp;<code>for a in `cat source-file-list` ; do</code><br>
-&nbsp;&nbsp;<code>&nbsp;&nbsp;goto-cc -c $a -o $a.gb</code><br>
-&nbsp;&nbsp;<code>done</code></p>
-
-<p class="justified">Note that it is important that the
-word-size of the kernel configuration matches that of goto-cc.
-Otherwise, compile-time assertions will fail, generating
-the error message "bit field size is negative". For a kernel
-configured for a 64-bit word-width, pass the option
-<nobr>--64</nobr> to goto-cc.</p>
-
-</li>
-
-</ol>
-
-<p class="justified">
-The resulting <code>.gb</code> files can be passed to any
-of the CPROVER tools.
-</p>
-
-<!--#include virtual="footer.inc" -->
-

doc/html-manual/goto-cc-rockbox.shtml

@@ -1,83 +0,0 @@
-<!--#include virtual="header.inc" -->
-
-<p><a href="./">CPROVER Manual TOC</a></p>
-
-<h2>Build Systems and Libraries</h2>
-
-<h3>Example: Extracting Models from the Rockbox</h3>
-
-<p class="justified">
-The <a href="http://www.rockbox.org/">Rockbox</a> is an open-source software
-package for common MP3 players, with about 1 million lines of code in total.
-</p>
-
-<ol>
-<li><p class="justified">
-First of all, you will need to install one of the cross-compilers. Follow
-the instructions <a href="http://www.rockbox.org/wiki/CrossCompiler">here</a>.
-</p></li>
-
-<li><p>
-You will then need to check out the Rockbox sources with GIT, and
-configure and compile the code. Follow <a href="http://www.rockbox.org/wiki/HowToCompile">
-these instructions</a>. The build must succeed.
-We will assume that one of the ARM-based targets
-is used, and that the ARM cross-compiler is installed
-at /usr/local/bin/arm-elf-eabi-gcc.
-</p></li>
-
-<li><p class="justified">Now download
-<a href="gcc-wrap.c">gcc-wrap.c</a>:</p>
-<p>
-&nbsp;&nbsp;<code>lwp-download http://www.cprover.org/cprover-manual/gcc-wrap.c</code><br>
-</p>
-</li>
-
-<li><p class="justified">Open gcc-wrap.c in your favorite editor,
-and adjust the path to gcc (in the first line) to
-/usr/local/bin/arm-elf-eabi-gcc (it is important that the
-full path is given).
-</p></li>
-
-<li><p class="justified">Now compile gcc-wrap:</p>
-<p>
-&nbsp;&nbsp;<code>gcc gcc-wrap.c -o gcc-wrap-arm-elf-eabi-gcc</code><br>
-&nbsp;&nbsp;<code>cp gcc-wrap-arm-elf-eabi-gcc ~/bin/</code><br>
-</p>
-<p class="justified">This assumes that the directory <code>~/bin</code>
-exists and is in your PATH variable.</p>
-</li>
-
-<li><p class="justified">Now re-compile the Rockbox code as follows:</p>
-<p>
-&nbsp;&nbsp;<code>make clean</code><br>
-&nbsp;&nbsp;<code>make CC=gcc-wrap-arm-elf-eabi-gcc</code></p>
-<p class="justified">
-This will re-compile the Rockbox, but this time retaining the
-preprocessed source files.
-</p></li>
-
-<li><p class="justified">You can now compile the preprocessed
-source files with goto-cc as follows:</p>
-<p>
-&nbsp;&nbsp;<code>find ./ -name \*.i > source-file-list</code><br>
-&nbsp;&nbsp;<code>for a in `cat source-file-list` ; do</code><br>
-&nbsp;&nbsp;<code>&nbsp;&nbsp;goto-cc -std=gnu99 -m32 -c $a -o $a.gb</code><br>
-&nbsp;&nbsp;<code>done</code></p>
-
-<p class="justified">Note that it is important that the
-word-size of the target platform matches that of goto-cc.
-For a 32-bit target, pass the option
-<nobr>-m32</nobr> to goto-cc.</p>
-
-</li>
-
-</ol>
-
-<p class="justified">
-The resulting <code>.gb</code> files can be passed to any
-of the CPROVER tools.
-</p>
-
-<!--#include virtual="footer.inc" -->
-

doc/html-manual/goto-cc-variants.shtml

@@ -1,48 +0,0 @@
-<!--#include virtual="header.inc" -->
-
-<p><a href="./">CPROVER Manual TOC</a></p>
-
-<h2>Build Systems and Libraries</h2>
-
-<h3>Variants of goto-cc</h3>
-
-<p class="justified">
-The goto-cc utility comes in several variants, summarised in the following table.
-</p>
-
-<center>
-<table cellpadding=5 cellspacing=0>
-<tr bgcolor="#e0e0e0">
-<th>Executable</th><th>Environment</th><th>Preprocessor</th></tr>
-<tr bgcolor="#e0f0f0"><td>goto-cc</td>
-  <td><a href="http://gcc.gnu.org/">gcc</a> (control-flow graph only)</td>
-  <td>gcc -E</td></tr>
-<tr bgcolor="#f0f0f0"><td>goto-gcc</td>
-  <td><a href="http://gcc.gnu.org/">gcc</a> ("hybrid" executable)</td>
-  <td>gcc -E</td></tr>
-<tr bgcolor="#e0f0f0"><td>goto-armcc</td>
-  <td><a href="http://arm.com/products/tools/software-tools/rvds/index.php">ARM RVDS</a></td>
-  <td>armcc -E</td></tr>
-<tr bgcolor="#f0f0f0"><td>goto-cl</td>
-  <td><a href="http://www.microsoft.com/visualstudio/">Visual Studio</a></td>
-  <td>cl /E</td></tr>
-<tr bgcolor="#e0f0f0"><td>goto-cw</td>
-  <td><a href="http://www.freescale.com/webapp/sps/site/homepage.jsp?code=CW_HOME">Freescale CodeWarrior</a></td>
-  <td>mwcceppc</td></tr>
-</table>
-</center>
-
-<p class="justified">
-
-The primary difference between the variants is the preprocessor called. 
-Furthermore, the language recognized varies slightly.  The variants can be
-obtained by simply renaming the goto-cc executable.  On Linux/MacOS, the
-variants can be obtained by creating a symbolic link.</p>
-
-<p class="justified">
-The "hybrid"
-executables contain both the control-flow graph for verification purposes
-and the usual, executable machine code.
-</p>
-
-<!--#include virtual="footer.inc" -->

doc/html-manual/goto-cc-visual-studio.shtml

@@ -1,57 +0,0 @@
-<!--#include virtual="header.inc" -->
-
-<p><a href="./">CPROVER Manual TOC</a></p>
-
-<h2>Build Systems and Libraries</h2>
-
-<h3>Integration into Visual Studio 2008 to 2012</h3>
-
-<p class="justified">
-Visual Studio version 2008 onwards comes with a new XML-based
-build system called <a href="http://msdn.microsoft.com/en-us/library/ms171452(v=vs.90).aspx">MSBuild</a>.
-The MSBuild system is also activated when triggering a build from the Visual Studio GUI.
-The project files created by the Visual Studio GUI are used as input by the MSBuild tool.
-</p>
-
-<p class="justified">
-The MSBuild system can be used to generate goto-binaries from your Visual Studio project
-as follows:
-</p>
-
-<ol>
-
-<li><p>
-Install the <code>goto-cl.exe</code> and <code>goto-link.exe</code> binaries
-in some directory that is contained in the PATH environment
-variable.</p></li>
-
-<li><p>Add a configuration for the goto-cc build for your project
-in the configuration manager, named "goto-cc".</p></li>
-
-<li><p>Open the Visual Studio Command Prompt (in the Tools menu).</p></li>
-
-<li><p>Locate the directory that contains the project. Change into this
-directory using "CD".</p></li>
-
-<li><p>Type</p>
-<p>
-<code>
-msbuild /p:CLToolExe=goto-cl.exe /p:LinkToolExe=goto-link.exe<br>
-&nbsp;&nbsp; /p:Flavor=goto-cc /p:Platform=x86
-</code>
-</p>
-
-<p>
-The platform can be adjusted as required; the "Flavor" given should match
-the configuration that was created earlier.
-</p></li>
-
-</ol>
-
-<p class="justified">
-Note that the recent versions of goto-cc also support file names with
-non-ASCII (Unicode) characters on Windows platforms.
-</p>
-
-<!--#include virtual="footer.inc" -->
-

doc/html-manual/goto-cc.shtml

@@ -1,144 +0,0 @@
-<!--#include virtual="header.inc" -->
-
-<p><a href="./">CPROVER Manual TOC</a></p>
-
-<h2>Build Systems and Libraries</h2>
-
-<h3>Integration into Build Systems with goto-cc</h3>
-
-<p class="justified">
-Existing software projects usually do not come in a single source file that
-may simply be passed to a model checker.  They rather come in a multitude of
-source files in different directories and refer to external libraries and
-system-wide options.  A <i>build system</i> then collects the configuration options
-from the system and compiles the software according to build rules.
-</p>
-
-<p class="justified">
-The most prevalent build tool on Unix (-based) systems surely is the
-<code>make</code> utility. This tool uses build rules given in a
-<i>Makefile</i> that comes with the software sources. Running software
-verification tools on projects like these is greatly simplified by a
-compiler that first collects all the necessary models into a single
-model file. <a href="http://www.cprover.org/goto-cc/">goto-cc</a>
-is such a model file extractor, which can seamlessly replace <code>gcc</code>
-and <code>cl.exe</code> in Makefiles. The normal build system for the
-project may be used to build the software, but the outcome will be a
-model file with suitable detail for verification, as opposed to a
-flat executable program. Note that goto-cc comes in different variants
-depending on the compilation environment. These variants
-are described <a href="goto-cc-variants.shtml">here</a>.
-</p>
-
-<h4>Example: Building wu-ftpd</h4>
-
-<p class="justified">This example assumes a Unix-like machine.</p>
-
-<ol>
-
-<li><p class="justified"> Download the sources of wu-ftpd from
-  <a href="ftp://ftp.wu-ftpd.org/pub/wu-ftpd/wu-ftpd-current.tar.gz">
-  here</a>.
-</p></li>
-
-<li><p class="justified"> Unpack the sources by running
-  <code> tar xfz wu-ftpd-current.tar.gz</code>
-</p></li>
-
-<li><p class="justified"> Change to the source directory, by entering, e.g.,
-  <code> cd wu-ftpd-2.6.2</code>
-</p></li>
-
-<li><p class="justified"> Configure the project for verification by running
-</p>
-<center>
-  <code>./configure YACC=byacc CC=goto-cc --host=none-none-none</code>
-</center>
-</li>
-
-<li><p class="justified"> Build the project by running
-  <code>make</code>.
-  This creates multiple model files in the <code>src</code> directory. Among
-  them is a model for the main executable <code>ftpd</code>.
-</p></li>
-
-<li><p class="justified"> Run a model-checker, e.g., <a href="cbmc.shtml">CBMC</a>,
-  on the model file:
-</p>
-<center>
-  <code>cbmc src/ftpd</code>
-</center>
-<p class="justified">CBMC automatically recognizes that the file
-is a goto binary.
-</p>
-</li>
-
-</ol>
-
-<h4>Important Notes</h4>
-
-<p class="justified">
-More elaborate build or configuration scripts often make use of
-features of the compiler or the system library to detect configuration
-options automatically, e.g., in a <code>configure</code> script. 
-Replacing <code>gcc</code> by goto-cc at this stage may confuse the script,
-or detect wrong options. For example, missing library functions do not
-cause goto-cc to throw an error (only to issue a warning). Because of
-this, configuration scripts sometimes falsely assume the availability
-of a system function or library.
-</p>
-
-<p class="justified">
-In the case of this or similar problems, it is more advisable to
-configure the project using the normal routine, and replacing the
-compiler setting manually in the generated Makefiles, e.g., by
-replacing lines like <code>CC=gcc</code> by <code>CC=goto-cc</code>.
-</p>
-
-<p class="justified">
-A helpful command that accomplishes this task successfully for many
-projects is the following: 
-</p>
-
-<code>
-for i in `find . -name Makefile`; do<br>
-&nbsp;&nbsp;sed -e 's/^\(\s*CC[ \t]*=\)\(.*$\)/\1goto-cc/g' -i $i<br>
-done
-</code>
-
-<p class="justified">Here are additional examples on how to use goto-cc:</p>
-
-<ul>
-<li><a href="goto-cc-linux.shtml">Linux Kernel</a></li>
-<li><a href="goto-cc-apache.shtml">Apache HTTPD</a></li>
-</ul>
-
-<p class="justified">A description
-of how to integrate goto-cc into Microsoft's Visual Studio
-is <a href="goto-cc-visual-studio.shtml">here</a>.</p>
-
-<h4>Linking Libraries</h4>
-
-<p class="justified">
-Some software projects come with their own libraries; also, the goal may be
-to analyze a library by itself. For this purpose it is possible to use
-goto-cc to link multiple model files into a library of model files. An
-object file can then be linked against this model library. For this purpose,
-goto-cc also features a linker mode.
-</p>
-
-<p class="justified">
-To enable this linker mode, create a link to the goto-cc binary by the
-name of goto-ld (Linux and Mac) or copy the goto-cc binary to goto-link.exe
-(Windows). The goto-ld tool can now be used as a seamless replacement
-for the <code>ld</code> tool present on most Unix (-based) systems and
-for the <code>link</code> tool on Windows.
-</p>
-
-<p class="justified">
-The default linker may need to be replaced by <code>goto-ld</code> or
-<code>goto-link.exe</code> in the build
-script, which can be achieved in much the same way as replacing the compiler.
-</p>
-
-<!--#include virtual="footer.inc" -->

doc/html-manual/header.inc

@@ -1,23 +0,0 @@
-<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
-"http://www.w3.org/TR/html4/loose.dtd">
-
-<html><head>
-<meta http-equiv="content-type" content="text/html; charset=ISO-8859-1">
-<link rel="stylesheet" type="text/css" href="/style/cprover.css">
-<title>CPROVER Manual</title>
-</head>
-
-<body>
-
-<!--#include virtual="../style/full-sidebar.html" -->
-
-<div id="wrap">
-<div id="main">
-
-<div id="nav">
-<ul>
-<li>SV Group Home</li>
-<li><a href="/software/">Software Verification</a></li>
-<li><a href="/hardware/">Hardware Verification</a></li>
-</ul>
-</div>

doc/html-manual/highlight/LICENSE

@@ -1,24 +0,0 @@
-Copyright (c) 2006, Ivan Sagalaev
-All rights reserved.
-Redistribution and use in source and binary forms, with or without
-modification, are permitted provided that the following conditions are met:
-
-    * Redistributions of source code must retain the above copyright
-      notice, this list of conditions and the following disclaimer.
-    * Redistributions in binary form must reproduce the above copyright
-      notice, this list of conditions and the following disclaimer in the
-      documentation and/or other materials provided with the distribution.
-    * Neither the name of highlight.js nor the names of its contributors 
-      may be used to endorse or promote products derived from this software 
-      without specific prior written permission.
-
-THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND ANY
-EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
-WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
-DISCLAIMED. IN NO EVENT SHALL THE REGENTS AND CONTRIBUTORS BE LIABLE FOR ANY
-DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
-(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
-LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
-ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
-(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
-SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

doc/html-manual/highlight/README.md

@@ -1,150 +0,0 @@
-# Highlight.js
-
-[![Build Status](https://travis-ci.org/isagalaev/highlight.js.svg?branch=master)](https://travis-ci.org/isagalaev/highlight.js)
-
-Highlight.js is a syntax highlighter written in JavaScript. It works in
-the browser as well as on the server. It works with pretty much any
-markup, doesn’t depend on any framework and has automatic language
-detection.
-
-## Getting Started
-
-The bare minimum for using highlight.js on a web page is linking to the
-library along with one of the styles and calling
-[`initHighlightingOnLoad`][1]:
-
-```html
-<link rel="stylesheet" href="/path/to/styles/default.css">
-<script src="/path/to/highlight.pack.js"></script>
-<script>hljs.initHighlightingOnLoad();</script>
-```
-
-This will find and highlight code inside of `<pre><code>` tags; it tries
-to detect the language automatically. If automatic detection doesn’t
-work for you, you can specify the language in the `class` attribute:
-
-```html
-<pre><code class="html">...</code></pre>
-```
-
-The list of supported language classes is available in the [class
-reference][2].  Classes can also be prefixed with either `language-` or
-`lang-`.
-
-To disable highlighting altogether use the `nohighlight` class:
-
-```html
-<pre><code class="nohighlight">...</code></pre>
-```
-
-## Custom Initialization
-
-When you need a bit more control over the initialization of
-highlight.js, you can use the [`highlightBlock`][3] and [`configure`][4]
-functions. This allows you to control *what* to highlight and *when*.
-
-Here’s an equivalent way to calling [`initHighlightingOnLoad`][1] using
-jQuery:
-
-```javascript
-$(document).ready(function() {
-  $('pre code').each(function(i, block) {
-    hljs.highlightBlock(block);
-  });
-});
-```
-
-You can use any tags instead of `<pre><code>` to mark up your code. If
-you don't use a container that preserve line breaks you will need to
-configure highlight.js to use the `<br>` tag:
-
-```javascript
-hljs.configure({useBR: true});
-
-$('div.code').each(function(i, block) {
-  hljs.highlightBlock(block);
-});
-```
-
-For other options refer to the documentation for [`configure`][4].
-
-
-## Web Workers
-
-You can run highlighting inside a web worker to avoid freezing the browser
-window while dealing with very big chunks of code.
-
-In your main script:
-
-```javascript
-addEventListener('load', function() {
-  var code = document.querySelector('#code');
-  var worker = new Worker('worker.js');
-  worker.onmessage = function(event) { code.innerHTML = event.data; }
-  worker.postMessage(code.textContent);
-})
-```
-
-In worker.js:
-
-```javascript
-onmessage = function(event) {
-  importScripts('<path>/highlight.pack.js');
-  var result = self.hljs.highlightAuto(event.data);
-  postMessage(result.value);
-}
-```
-
-
-## Getting the Library
-
-You can get highlight.js as a hosted, or custom-build, browser script or
-as a server module. Right out of the box the browser script supports
-both AMD and CommonJS, so if you wish you can use RequireJS or
-Browserify without having to build from source. The server module also
-works perfectly fine with Browserify, but there is the option to use a
-build specific to browsers rather than something meant for a server.
-Head over to the [download page][5] for all the options.
-
-**Don't link to GitHub directly.** The library is not supposed to work straight
-from the source, it requires building. If none of the pre-packaged options
-work for you refer to the [building documentation][6].
-
-**The CDN-hosted package doesn't have all the languages.** Otherwise it'd be
-too big. If you don't see the language you need in the ["Common" section][5],
-it can be added manually:
-
-```html
-<script src="//cdnjs.cloudflare.com/ajax/libs/highlight.js/9.4.0/languages/go.min.js"></script>
-```
-
-**On Almond.** You need to use the optimizer to give the module a name. For
-example:
-
-```
-r.js -o name=hljs paths.hljs=/path/to/highlight out=highlight.js
-```
-
-
-## License
-
-Highlight.js is released under the BSD License. See [LICENSE][7] file
-for details.
-
-## Links
-
-The official site for the library is at <https://highlightjs.org/>.
-
-Further in-depth documentation for the API and other topics is at
-<http://highlightjs.readthedocs.io/>.
-
-Authors and contributors are listed in the [AUTHORS.en.txt][8] file.
-
-[1]: http://highlightjs.readthedocs.io/en/latest/api.html#inithighlightingonload
-[2]: http://highlightjs.readthedocs.io/en/latest/css-classes-reference.html
-[3]: http://highlightjs.readthedocs.io/en/latest/api.html#highlightblock-block
-[4]: http://highlightjs.readthedocs.io/en/latest/api.html#configure-options
-[5]: https://highlightjs.org/download/
-[6]: http://highlightjs.readthedocs.io/en/latest/building-testing.html
-[7]: https://github.com/isagalaev/highlight.js/blob/master/LICENSE
-[8]: https://github.com/isagalaev/highlight.js/blob/master/AUTHORS.en.txt

doc/html-manual/highlight/README.ru.md

@@ -1,142 +0,0 @@
-# Highlight.js
-
-Highlight.js — это инструмент для подсветки синтаксиса, написанный на JavaScript. Он работает
-и в браузере, и на сервере. Он работает с практически любой HTML разметкой, не
-зависит от каких-либо фреймворков и умеет автоматически определять язык.
-
-
-## Начало работы
-
-Минимум, что нужно сделать для использования highlight.js на веб-странице — это
-подключить библиотеку, CSS-стили и вызывать [`initHighlightingOnLoad`][1]:
-
-```html
-<link rel="stylesheet" href="/path/to/styles/default.css">
-<script src="/path/to/highlight.pack.js"></script>
-<script>hljs.initHighlightingOnLoad();</script>
-```
-
-Библиотека найдёт и раскрасит код внутри тегов `<pre><code>`, попытавшись
-автоматически определить язык. Когда автоопределение не срабатывает, можно явно
-указать язык в атрибуте class:
-
-```html
-<pre><code class="html">...</code></pre>
-```
-
-Список поддерживаемых классов языков доступен в [справочнике по классам][2].
-Класс также можно предварить префиксами `language-` или `lang-`.
-
-Чтобы отключить подсветку для какого-то блока, используйте класс `nohighlight`:
-
-```html
-<pre><code class="nohighlight">...</code></pre>
-```
-
-## Инициализация вручную
-
-Чтобы иметь чуть больше контроля за инициализацией подсветки, вы можете
-использовать функции [`highlightBlock`][3] и [`configure`][4]. Таким образом
-можно управлять тем, *что* и *когда* подсвечивать.
-
-Вот пример инициализации, эквивалентной вызову [`initHighlightingOnLoad`][1], но
-с использованием jQuery:
-
-```javascript
-$(document).ready(function() {
-  $('pre code').each(function(i, block) {
-    hljs.highlightBlock(block);
-  });
-});
-```
-
-Вы можете использовать любые теги разметки вместо `<pre><code>`. Если
-используете контейнер, не сохраняющий переводы строк, вам нужно сказать
-highlight.js использовать для них тег `<br>`:
-
-```javascript
-hljs.configure({useBR: true});
-
-$('div.code').each(function(i, block) {
-  hljs.highlightBlock(block);
-});
-```
-
-Другие опции можно найти в документации функции [`configure`][4].
-
-
-## Web Workers
-
-Подсветку можно запустить внутри web worker'а, чтобы окно
-браузера не подтормаживало при работе с большими кусками кода.
-
-В основном скрипте:
-
-```javascript
-addEventListener('load', function() {
-  var code = document.querySelector('#code');
-  var worker = new Worker('worker.js');
-  worker.onmessage = function(event) { code.innerHTML = event.data; }
-  worker.postMessage(code.textContent);
-})
-```
-
-В worker.js:
-
-```javascript
-onmessage = function(event) {
-  importScripts('<path>/highlight.pack.js');
-  var result = self.hljs.highlightAuto(event.data);
-  postMessage(result.value);
-}
-```
-
-
-## Установка библиотеки
-
-Highlight.js можно использовать в браузере прямо с CDN хостинга или скачать
-индивидуальную сборку, а также установив модуль на сервере. На
-[странице загрузки][5] подробно описаны все варианты.
-
-**Не подключайте GitHub напрямую.** Библиотека не предназначена для
-использования в виде исходного кода, а требует отдельной сборки. Если вам не
-подходит ни один из готовых вариантов, читайте [документацию по сборке][6].
-
-**Файл на CDN содержит не все языки.** Иначе он будет слишком большого размера.
-Если нужного вам языка нет в [категории "Common"][5], можно дообавить его
-вручную:
-
-```html
-<script src="//cdnjs.cloudflare.com/ajax/libs/highlight.js/9.4.0/languages/go.min.js"></script>
-```
-
-**Про Almond.** Нужно задать имя модуля в оптимизаторе, например:
-
-```
-r.js -o name=hljs paths.hljs=/path/to/highlight out=highlight.js
-```
-
-
-## Лицензия
-
-Highlight.js распространяется под лицензией BSD. Подробнее читайте файл
-[LICENSE][7].
-
-
-## Ссылки
-
-Официальный сайт билиотеки расположен по адресу <https://highlightjs.org/>.
-
-Более подробная документация по API и другим темам расположена на
-<http://highlightjs.readthedocs.io/>.
-
-Авторы и контрибьюторы перечислены в файле [AUTHORS.ru.txt][8] file.
-
-[1]: http://highlightjs.readthedocs.io/en/latest/api.html#inithighlightingonload
-[2]: http://highlightjs.readthedocs.io/en/latest/css-classes-reference.html
-[3]: http://highlightjs.readthedocs.io/en/latest/api.html#highlightblock-block
-[4]: http://highlightjs.readthedocs.io/en/latest/api.html#configure-options
-[5]: https://highlightjs.org/download/
-[6]: http://highlightjs.readthedocs.io/en/latest/building-testing.html
-[7]: https://github.com/isagalaev/highlight.js/blob/master/LICENSE
-[8]: https://github.com/isagalaev/highlight.js/blob/master/AUTHORS.ru.txt

doc/html-manual/highlight/styles/agate.css

@@ -1,108 +0,0 @@
-/*!
- * Agate by Taufik Nurrohman <https://github.com/tovic>
- * ----------------------------------------------------
- *
- * #ade5fc
- * #a2fca2
- * #c6b4f0
- * #d36363
- * #fcc28c
- * #fc9b9b
- * #ffa
- * #fff
- * #333
- * #62c8f3
- * #888
- *
- */
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  padding: 0.5em;
-  background: #333;
-  color: white;
-}
-
-.hljs-name,
-.hljs-strong {
-  font-weight: bold;
-}
-
-.hljs-code,
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-tag {
-  color: #62c8f3;
-}
-
-.hljs-variable,
-.hljs-template-variable,
-.hljs-selector-id,
-.hljs-selector-class {
-  color: #ade5fc;
-}
-
-.hljs-string,
-.hljs-bullet {
-  color: #a2fca2;
-}
-
-.hljs-type,
-.hljs-title,
-.hljs-section,
-.hljs-attribute,
-.hljs-quote,
-.hljs-built_in,
-.hljs-builtin-name {
-  color: #ffa;
-}
-
-.hljs-number,
-.hljs-symbol,
-.hljs-bullet {
-  color: #d36363;
-}
-
-.hljs-keyword,
-.hljs-selector-tag,
-.hljs-literal {
-  color: #fcc28c;
-}
-
-.hljs-comment,
-.hljs-deletion,
-.hljs-code {
-  color: #888;
-}
-
-.hljs-regexp,
-.hljs-link {
-  color: #c6b4f0;
-}
-
-.hljs-meta {
-  color: #fc9b9b;
-}
-
-.hljs-deletion {
-  background-color: #fc9b9b;
-  color: #333;
-}
-
-.hljs-addition {
-  background-color: #a2fca2;
-  color: #333;
-}
-
-.hljs a {
-  color: inherit;
-}
-
-.hljs a:focus,
-.hljs a:hover {
-  color: inherit;
-  text-decoration: underline;
-}

doc/html-manual/highlight/styles/androidstudio.css

@@ -1,66 +0,0 @@
-/*
-Date: 24 Fev 2015
-Author: Pedro Oliveira <kanytu@gmail . com>
-*/
-
-.hljs {
-  color: #a9b7c6;
-  background: #282b2e;
-  display: block;
-  overflow-x: auto;
-  padding: 0.5em;
-}
-
-.hljs-number,
-.hljs-literal,
-.hljs-symbol,
-.hljs-bullet {
-  color: #6897BB;
-}
-
-.hljs-keyword,
-.hljs-selector-tag,
-.hljs-deletion {
-  color: #cc7832;
-}
-
-.hljs-variable,
-.hljs-template-variable,
-.hljs-link {
-  color: #629755;
-}
-
-.hljs-comment,
-.hljs-quote {
-  color: #808080;
-}
-
-.hljs-meta {
-  color: #bbb529;
-}
-
-.hljs-string,
-.hljs-attribute,
-.hljs-addition {
-  color: #6A8759;
-}
-
-.hljs-section,
-.hljs-title,
-.hljs-type {
-  color: #ffc66d;
-}
-
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class {
-  color: #e8bf6a;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/arduino-light.css

@@ -1,88 +0,0 @@
-/*
-
-Arduino® Light Theme - Stefania Mellai <s.mellai@arduino.cc>
-
-*/
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  padding: 0.5em;
-  background: #FFFFFF;
-}
-
-.hljs,
-.hljs-subst {
-  color: #434f54;
-}
-
-.hljs-keyword,
-.hljs-attribute,
-.hljs-selector-tag,
-.hljs-doctag,
-.hljs-name {
-  color: #00979D;
-}
-
-.hljs-built_in,
-.hljs-literal,
-.hljs-bullet,
-.hljs-code,
-.hljs-addition {
-  color: #D35400;
-}
-
-.hljs-regexp,
-.hljs-symbol,
-.hljs-variable,
-.hljs-template-variable,
-.hljs-link,
-.hljs-selector-attr,
-.hljs-selector-pseudo {
-  color: #00979D;
-}
-
-.hljs-type,
-.hljs-string,
-.hljs-selector-id,
-.hljs-selector-class,
-.hljs-quote,
-.hljs-template-tag,
-.hljs-deletion {
-  color: #005C5F;
-}
-
-.hljs-title,
-.hljs-section {
-  color: #880000;
-  font-weight: bold;
-}
-
-.hljs-comment {
-  color: rgba(149,165,166,.8);
-}
-
-.hljs-meta-keyword {
-  color: #728E00;
-}
-
-.hljs-meta {
-  color: #728E00;
-  color: #434f54;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}
-
-.hljs-function {
-  color: #728E00;
-}
-
-.hljs-number {
-  color: #8A7B52;  
-}

doc/html-manual/highlight/styles/arta.css

@@ -1,73 +0,0 @@
-/*
-Date: 17.V.2011
-Author: pumbur <pumbur@pumbur.net>
-*/
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  padding: 0.5em;
-  background: #222;
-}
-
-.hljs,
-.hljs-subst {
-  color: #aaa;
-}
-
-.hljs-section {
-  color: #fff;
-}
-
-.hljs-comment,
-.hljs-quote,
-.hljs-meta {
-  color: #444;
-}
-
-.hljs-string,
-.hljs-symbol,
-.hljs-bullet,
-.hljs-regexp {
-  color: #ffcc33;
-}
-
-.hljs-number,
-.hljs-addition {
-  color: #00cc66;
-}
-
-.hljs-built_in,
-.hljs-builtin-name,
-.hljs-literal,
-.hljs-type,
-.hljs-template-variable,
-.hljs-attribute,
-.hljs-link {
-  color: #32aaee;
-}
-
-.hljs-keyword,
-.hljs-selector-tag,
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class {
-  color: #6644aa;
-}
-
-.hljs-title,
-.hljs-variable,
-.hljs-deletion,
-.hljs-template-tag {
-  color: #bb1166;
-}
-
-.hljs-section,
-.hljs-doctag,
-.hljs-strong {
-  font-weight: bold;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}

doc/html-manual/highlight/styles/ascetic.css

@@ -1,45 +0,0 @@
-/*
-
-Original style from softwaremaniacs.org (c) Ivan Sagalaev <Maniac@SoftwareManiacs.Org>
-
-*/
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  padding: 0.5em;
-  background: white;
-  color: black;
-}
-
-.hljs-string,
-.hljs-variable,
-.hljs-template-variable,
-.hljs-symbol,
-.hljs-bullet,
-.hljs-section,
-.hljs-addition,
-.hljs-attribute,
-.hljs-link {
-  color: #888;
-}
-
-.hljs-comment,
-.hljs-quote,
-.hljs-meta,
-.hljs-deletion {
-  color: #ccc;
-}
-
-.hljs-keyword,
-.hljs-selector-tag,
-.hljs-section,
-.hljs-name,
-.hljs-type,
-.hljs-strong {
-  font-weight: bold;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}

doc/html-manual/highlight/styles/atelier-cave-dark.css

@@ -1,83 +0,0 @@
-/* Base16 Atelier Cave Dark - Theme */
-/* by Bram de Haan (http://atelierbram.github.io/syntax-highlighting/atelier-schemes/cave) */
-/* Original Base16 color scheme by Chris Kempson (https://github.com/chriskempson/base16) */
-
-/* Atelier-Cave Comment */
-.hljs-comment,
-.hljs-quote {
-  color: #7e7887;
-}
-
-/* Atelier-Cave Red */
-.hljs-variable,
-.hljs-template-variable,
-.hljs-attribute,
-.hljs-regexp,
-.hljs-link,
-.hljs-tag,
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class {
-  color: #be4678;
-}
-
-/* Atelier-Cave Orange */
-.hljs-number,
-.hljs-meta,
-.hljs-built_in,
-.hljs-builtin-name,
-.hljs-literal,
-.hljs-type,
-.hljs-params {
-  color: #aa573c;
-}
-
-/* Atelier-Cave Green */
-.hljs-string,
-.hljs-symbol,
-.hljs-bullet {
-  color: #2a9292;
-}
-
-/* Atelier-Cave Blue */
-.hljs-title,
-.hljs-section {
-  color: #576ddb;
-}
-
-/* Atelier-Cave Purple */
-.hljs-keyword,
-.hljs-selector-tag {
-  color: #955ae7;
-}
-
-.hljs-deletion,
-.hljs-addition {
-  color: #19171c;
-  display: inline-block;
-  width: 100%;
-}
-
-.hljs-deletion {
-  background-color: #be4678;
-}
-
-.hljs-addition {
-  background-color: #2a9292;
-}
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  background: #19171c;
-  color: #8b8792;
-  padding: 0.5em;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/atelier-cave-light.css

@@ -1,85 +0,0 @@
-/* Base16 Atelier Cave Light - Theme */
-/* by Bram de Haan (http://atelierbram.github.io/syntax-highlighting/atelier-schemes/cave) */
-/* Original Base16 color scheme by Chris Kempson (https://github.com/chriskempson/base16) */
-
-/* Atelier-Cave Comment */
-.hljs-comment,
-.hljs-quote {
-  color: #655f6d;
-}
-
-/* Atelier-Cave Red */
-.hljs-variable,
-.hljs-template-variable,
-.hljs-attribute,
-.hljs-tag,
-.hljs-name,
-.hljs-regexp,
-.hljs-link,
-.hljs-name,
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class {
-  color: #be4678;
-}
-
-/* Atelier-Cave Orange */
-.hljs-number,
-.hljs-meta,
-.hljs-built_in,
-.hljs-builtin-name,
-.hljs-literal,
-.hljs-type,
-.hljs-params {
-  color: #aa573c;
-}
-
-/* Atelier-Cave Green */
-.hljs-string,
-.hljs-symbol,
-.hljs-bullet {
-  color: #2a9292;
-}
-
-/* Atelier-Cave Blue */
-.hljs-title,
-.hljs-section {
-  color: #576ddb;
-}
-
-/* Atelier-Cave Purple */
-.hljs-keyword,
-.hljs-selector-tag {
-  color: #955ae7;
-}
-
-.hljs-deletion,
-.hljs-addition {
-  color: #19171c;
-  display: inline-block;
-  width: 100%;
-}
-
-.hljs-deletion {
-  background-color: #be4678;
-}
-
-.hljs-addition {
-  background-color: #2a9292;
-}
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  background: #efecf4;
-  color: #585260;
-  padding: 0.5em;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/atelier-dune-dark.css

@@ -1,69 +0,0 @@
-/* Base16 Atelier Dune Dark - Theme */
-/* by Bram de Haan (http://atelierbram.github.io/syntax-highlighting/atelier-schemes/dune) */
-/* Original Base16 color scheme by Chris Kempson (https://github.com/chriskempson/base16) */
-
-/* Atelier-Dune Comment */
-.hljs-comment,
-.hljs-quote {
-  color: #999580;
-}
-
-/* Atelier-Dune Red */
-.hljs-variable,
-.hljs-template-variable,
-.hljs-attribute,
-.hljs-tag,
-.hljs-name,
-.hljs-regexp,
-.hljs-link,
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class {
-  color: #d73737;
-}
-
-/* Atelier-Dune Orange */
-.hljs-number,
-.hljs-meta,
-.hljs-built_in,
-.hljs-builtin-name,
-.hljs-literal,
-.hljs-type,
-.hljs-params {
-  color: #b65611;
-}
-
-/* Atelier-Dune Green */
-.hljs-string,
-.hljs-symbol,
-.hljs-bullet {
-  color: #60ac39;
-}
-
-/* Atelier-Dune Blue */
-.hljs-title,
-.hljs-section {
-  color: #6684e1;
-}
-
-/* Atelier-Dune Purple */
-.hljs-keyword,
-.hljs-selector-tag {
-  color: #b854d4;
-}
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  background: #20201d;
-  color: #a6a28c;
-  padding: 0.5em;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/atelier-dune-light.css

@@ -1,69 +0,0 @@
-/* Base16 Atelier Dune Light - Theme */
-/* by Bram de Haan (http://atelierbram.github.io/syntax-highlighting/atelier-schemes/dune) */
-/* Original Base16 color scheme by Chris Kempson (https://github.com/chriskempson/base16) */
-
-/* Atelier-Dune Comment */
-.hljs-comment,
-.hljs-quote {
-  color: #7d7a68;
-}
-
-/* Atelier-Dune Red */
-.hljs-variable,
-.hljs-template-variable,
-.hljs-attribute,
-.hljs-tag,
-.hljs-name,
-.hljs-regexp,
-.hljs-link,
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class {
-  color: #d73737;
-}
-
-/* Atelier-Dune Orange */
-.hljs-number,
-.hljs-meta,
-.hljs-built_in,
-.hljs-builtin-name,
-.hljs-literal,
-.hljs-type,
-.hljs-params {
-  color: #b65611;
-}
-
-/* Atelier-Dune Green */
-.hljs-string,
-.hljs-symbol,
-.hljs-bullet {
-  color: #60ac39;
-}
-
-/* Atelier-Dune Blue */
-.hljs-title,
-.hljs-section {
-  color: #6684e1;
-}
-
-/* Atelier-Dune Purple */
-.hljs-keyword,
-.hljs-selector-tag {
-  color: #b854d4;
-}
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  background: #fefbec;
-  color: #6e6b5e;
-  padding: 0.5em;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/atelier-estuary-dark.css

@@ -1,84 +0,0 @@
-/* Base16 Atelier Estuary Dark - Theme */
-/* by Bram de Haan (http://atelierbram.github.io/syntax-highlighting/atelier-schemes/estuary) */
-/* Original Base16 color scheme by Chris Kempson (https://github.com/chriskempson/base16) */
-
-/* Atelier-Estuary Comment */
-.hljs-comment,
-.hljs-quote {
-  color: #878573;
-}
-
-/* Atelier-Estuary Red */
-.hljs-variable,
-.hljs-template-variable,
-.hljs-attribute,
-.hljs-tag,
-.hljs-name,
-.hljs-regexp,
-.hljs-link,
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class {
-  color: #ba6236;
-}
-
-/* Atelier-Estuary Orange */
-.hljs-number,
-.hljs-meta,
-.hljs-built_in,
-.hljs-builtin-name,
-.hljs-literal,
-.hljs-type,
-.hljs-params {
-  color: #ae7313;
-}
-
-/* Atelier-Estuary Green */
-.hljs-string,
-.hljs-symbol,
-.hljs-bullet {
-  color: #7d9726;
-}
-
-/* Atelier-Estuary Blue */
-.hljs-title,
-.hljs-section {
-  color: #36a166;
-}
-
-/* Atelier-Estuary Purple */
-.hljs-keyword,
-.hljs-selector-tag {
-  color: #5f9182;
-}
-
-.hljs-deletion,
-.hljs-addition {
-  color: #22221b;
-  display: inline-block;
-  width: 100%;
-}
-
-.hljs-deletion {
-  background-color: #ba6236;
-}
-
-.hljs-addition {
-  background-color: #7d9726;
-}
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  background: #22221b;
-  color: #929181;
-  padding: 0.5em;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/atelier-estuary-light.css

@@ -1,84 +0,0 @@
-/* Base16 Atelier Estuary Light - Theme */
-/* by Bram de Haan (http://atelierbram.github.io/syntax-highlighting/atelier-schemes/estuary) */
-/* Original Base16 color scheme by Chris Kempson (https://github.com/chriskempson/base16) */
-
-/* Atelier-Estuary Comment */
-.hljs-comment,
-.hljs-quote {
-  color: #6c6b5a;
-}
-
-/* Atelier-Estuary Red */
-.hljs-variable,
-.hljs-template-variable,
-.hljs-attribute,
-.hljs-tag,
-.hljs-name,
-.hljs-regexp,
-.hljs-link,
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class {
-  color: #ba6236;
-}
-
-/* Atelier-Estuary Orange */
-.hljs-number,
-.hljs-meta,
-.hljs-built_in,
-.hljs-builtin-name,
-.hljs-literal,
-.hljs-type,
-.hljs-params {
-  color: #ae7313;
-}
-
-/* Atelier-Estuary Green */
-.hljs-string,
-.hljs-symbol,
-.hljs-bullet {
-  color: #7d9726;
-}
-
-/* Atelier-Estuary Blue */
-.hljs-title,
-.hljs-section {
-  color: #36a166;
-}
-
-/* Atelier-Estuary Purple */
-.hljs-keyword,
-.hljs-selector-tag {
-  color: #5f9182;
-}
-
-.hljs-deletion,
-.hljs-addition {
-  color: #22221b;
-  display: inline-block;
-  width: 100%;
-}
-
-.hljs-deletion {
-  background-color: #ba6236;
-}
-
-.hljs-addition {
-  background-color: #7d9726;
-}
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  background: #f4f3ec;
-  color: #5f5e4e;
-  padding: 0.5em;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/atelier-forest-dark.css

@@ -1,69 +0,0 @@
-/* Base16 Atelier Forest Dark - Theme */
-/* by Bram de Haan (http://atelierbram.github.io/syntax-highlighting/atelier-schemes/forest) */
-/* Original Base16 color scheme by Chris Kempson (https://github.com/chriskempson/base16) */
-
-/* Atelier-Forest Comment */
-.hljs-comment,
-.hljs-quote {
-  color: #9c9491;
-}
-
-/* Atelier-Forest Red */
-.hljs-variable,
-.hljs-template-variable,
-.hljs-attribute,
-.hljs-tag,
-.hljs-name,
-.hljs-regexp,
-.hljs-link,
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class {
-  color: #f22c40;
-}
-
-/* Atelier-Forest Orange */
-.hljs-number,
-.hljs-meta,
-.hljs-built_in,
-.hljs-builtin-name,
-.hljs-literal,
-.hljs-type,
-.hljs-params {
-  color: #df5320;
-}
-
-/* Atelier-Forest Green */
-.hljs-string,
-.hljs-symbol,
-.hljs-bullet {
-  color: #7b9726;
-}
-
-/* Atelier-Forest Blue */
-.hljs-title,
-.hljs-section {
-  color: #407ee7;
-}
-
-/* Atelier-Forest Purple */
-.hljs-keyword,
-.hljs-selector-tag {
-  color: #6666ea;
-}
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  background: #1b1918;
-  color: #a8a19f;
-  padding: 0.5em;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/atelier-forest-light.css

@@ -1,69 +0,0 @@
-/* Base16 Atelier Forest Light - Theme */
-/* by Bram de Haan (http://atelierbram.github.io/syntax-highlighting/atelier-schemes/forest) */
-/* Original Base16 color scheme by Chris Kempson (https://github.com/chriskempson/base16) */
-
-/* Atelier-Forest Comment */
-.hljs-comment,
-.hljs-quote {
-  color: #766e6b;
-}
-
-/* Atelier-Forest Red */
-.hljs-variable,
-.hljs-template-variable,
-.hljs-attribute,
-.hljs-tag,
-.hljs-name,
-.hljs-regexp,
-.hljs-link,
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class {
-  color: #f22c40;
-}
-
-/* Atelier-Forest Orange */
-.hljs-number,
-.hljs-meta,
-.hljs-built_in,
-.hljs-builtin-name,
-.hljs-literal,
-.hljs-type,
-.hljs-params {
-  color: #df5320;
-}
-
-/* Atelier-Forest Green */
-.hljs-string,
-.hljs-symbol,
-.hljs-bullet {
-  color: #7b9726;
-}
-
-/* Atelier-Forest Blue */
-.hljs-title,
-.hljs-section {
-  color: #407ee7;
-}
-
-/* Atelier-Forest Purple */
-.hljs-keyword,
-.hljs-selector-tag {
-  color: #6666ea;
-}
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  background: #f1efee;
-  color: #68615e;
-  padding: 0.5em;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/atelier-heath-dark.css

@@ -1,69 +0,0 @@
-/* Base16 Atelier Heath Dark - Theme */
-/* by Bram de Haan (http://atelierbram.github.io/syntax-highlighting/atelier-schemes/heath) */
-/* Original Base16 color scheme by Chris Kempson (https://github.com/chriskempson/base16) */
-
-/* Atelier-Heath Comment */
-.hljs-comment,
-.hljs-quote {
-  color: #9e8f9e;
-}
-
-/* Atelier-Heath Red */
-.hljs-variable,
-.hljs-template-variable,
-.hljs-attribute,
-.hljs-tag,
-.hljs-name,
-.hljs-regexp,
-.hljs-link,
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class {
-  color: #ca402b;
-}
-
-/* Atelier-Heath Orange */
-.hljs-number,
-.hljs-meta,
-.hljs-built_in,
-.hljs-builtin-name,
-.hljs-literal,
-.hljs-type,
-.hljs-params {
-  color: #a65926;
-}
-
-/* Atelier-Heath Green */
-.hljs-string,
-.hljs-symbol,
-.hljs-bullet {
-  color: #918b3b;
-}
-
-/* Atelier-Heath Blue */
-.hljs-title,
-.hljs-section {
-  color: #516aec;
-}
-
-/* Atelier-Heath Purple */
-.hljs-keyword,
-.hljs-selector-tag {
-  color: #7b59c0;
-}
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  background: #1b181b;
-  color: #ab9bab;
-  padding: 0.5em;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/atelier-heath-light.css

@@ -1,69 +0,0 @@
-/* Base16 Atelier Heath Light - Theme */
-/* by Bram de Haan (http://atelierbram.github.io/syntax-highlighting/atelier-schemes/heath) */
-/* Original Base16 color scheme by Chris Kempson (https://github.com/chriskempson/base16) */
-
-/* Atelier-Heath Comment */
-.hljs-comment,
-.hljs-quote {
-  color: #776977;
-}
-
-/* Atelier-Heath Red */
-.hljs-variable,
-.hljs-template-variable,
-.hljs-attribute,
-.hljs-tag,
-.hljs-name,
-.hljs-regexp,
-.hljs-link,
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class {
-  color: #ca402b;
-}
-
-/* Atelier-Heath Orange */
-.hljs-number,
-.hljs-meta,
-.hljs-built_in,
-.hljs-builtin-name,
-.hljs-literal,
-.hljs-type,
-.hljs-params {
-  color: #a65926;
-}
-
-/* Atelier-Heath Green */
-.hljs-string,
-.hljs-symbol,
-.hljs-bullet {
-  color: #918b3b;
-}
-
-/* Atelier-Heath Blue */
-.hljs-title,
-.hljs-section {
-  color: #516aec;
-}
-
-/* Atelier-Heath Purple */
-.hljs-keyword,
-.hljs-selector-tag {
-  color: #7b59c0;
-}
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  background: #f7f3f7;
-  color: #695d69;
-  padding: 0.5em;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/atelier-lakeside-dark.css

@@ -1,69 +0,0 @@
-/* Base16 Atelier Lakeside Dark - Theme */
-/* by Bram de Haan (http://atelierbram.github.io/syntax-highlighting/atelier-schemes/lakeside) */
-/* Original Base16 color scheme by Chris Kempson (https://github.com/chriskempson/base16) */
-
-/* Atelier-Lakeside Comment */
-.hljs-comment,
-.hljs-quote {
-  color: #7195a8;
-}
-
-/* Atelier-Lakeside Red */
-.hljs-variable,
-.hljs-template-variable,
-.hljs-attribute,
-.hljs-tag,
-.hljs-name,
-.hljs-regexp,
-.hljs-link,
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class {
-  color: #d22d72;
-}
-
-/* Atelier-Lakeside Orange */
-.hljs-number,
-.hljs-meta,
-.hljs-built_in,
-.hljs-builtin-name,
-.hljs-literal,
-.hljs-type,
-.hljs-params {
-  color: #935c25;
-}
-
-/* Atelier-Lakeside Green */
-.hljs-string,
-.hljs-symbol,
-.hljs-bullet {
-  color: #568c3b;
-}
-
-/* Atelier-Lakeside Blue */
-.hljs-title,
-.hljs-section {
-  color: #257fad;
-}
-
-/* Atelier-Lakeside Purple */
-.hljs-keyword,
-.hljs-selector-tag {
-  color: #6b6bb8;
-}
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  background: #161b1d;
-  color: #7ea2b4;
-  padding: 0.5em;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/atelier-lakeside-light.css

@@ -1,69 +0,0 @@
-/* Base16 Atelier Lakeside Light - Theme */
-/* by Bram de Haan (http://atelierbram.github.io/syntax-highlighting/atelier-schemes/lakeside) */
-/* Original Base16 color scheme by Chris Kempson (https://github.com/chriskempson/base16) */
-
-/* Atelier-Lakeside Comment */
-.hljs-comment,
-.hljs-quote {
-  color: #5a7b8c;
-}
-
-/* Atelier-Lakeside Red */
-.hljs-variable,
-.hljs-template-variable,
-.hljs-attribute,
-.hljs-tag,
-.hljs-name,
-.hljs-regexp,
-.hljs-link,
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class {
-  color: #d22d72;
-}
-
-/* Atelier-Lakeside Orange */
-.hljs-number,
-.hljs-meta,
-.hljs-built_in,
-.hljs-builtin-name,
-.hljs-literal,
-.hljs-type,
-.hljs-params {
-  color: #935c25;
-}
-
-/* Atelier-Lakeside Green */
-.hljs-string,
-.hljs-symbol,
-.hljs-bullet {
-  color: #568c3b;
-}
-
-/* Atelier-Lakeside Blue */
-.hljs-title,
-.hljs-section {
-  color: #257fad;
-}
-
-/* Atelier-Lakeside Purple */
-.hljs-keyword,
-.hljs-selector-tag {
-  color: #6b6bb8;
-}
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  background: #ebf8ff;
-  color: #516d7b;
-  padding: 0.5em;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/atelier-plateau-dark.css

@@ -1,84 +0,0 @@
-/* Base16 Atelier Plateau Dark - Theme */
-/* by Bram de Haan (http://atelierbram.github.io/syntax-highlighting/atelier-schemes/plateau) */
-/* Original Base16 color scheme by Chris Kempson (https://github.com/chriskempson/base16) */
-
-/* Atelier-Plateau Comment */
-.hljs-comment,
-.hljs-quote {
-  color: #7e7777;
-}
-
-/* Atelier-Plateau Red */
-.hljs-variable,
-.hljs-template-variable,
-.hljs-attribute,
-.hljs-tag,
-.hljs-name,
-.hljs-regexp,
-.hljs-link,
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class {
-  color: #ca4949;
-}
-
-/* Atelier-Plateau Orange */
-.hljs-number,
-.hljs-meta,
-.hljs-built_in,
-.hljs-builtin-name,
-.hljs-literal,
-.hljs-type,
-.hljs-params {
-  color: #b45a3c;
-}
-
-/* Atelier-Plateau Green */
-.hljs-string,
-.hljs-symbol,
-.hljs-bullet {
-  color: #4b8b8b;
-}
-
-/* Atelier-Plateau Blue */
-.hljs-title,
-.hljs-section {
-  color: #7272ca;
-}
-
-/* Atelier-Plateau Purple */
-.hljs-keyword,
-.hljs-selector-tag {
-  color: #8464c4;
-}
-
-.hljs-deletion,
-.hljs-addition {
-  color: #1b1818;
-  display: inline-block;
-  width: 100%;
-}
-
-.hljs-deletion {
-  background-color: #ca4949;
-}
-
-.hljs-addition {
-  background-color: #4b8b8b;
-}
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  background: #1b1818;
-  color: #8a8585;
-  padding: 0.5em;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/atelier-plateau-light.css

@@ -1,84 +0,0 @@
-/* Base16 Atelier Plateau Light - Theme */
-/* by Bram de Haan (http://atelierbram.github.io/syntax-highlighting/atelier-schemes/plateau) */
-/* Original Base16 color scheme by Chris Kempson (https://github.com/chriskempson/base16) */
-
-/* Atelier-Plateau Comment */
-.hljs-comment,
-.hljs-quote {
-  color: #655d5d;
-}
-
-/* Atelier-Plateau Red */
-.hljs-variable,
-.hljs-template-variable,
-.hljs-attribute,
-.hljs-tag,
-.hljs-name,
-.hljs-regexp,
-.hljs-link,
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class {
-  color: #ca4949;
-}
-
-/* Atelier-Plateau Orange */
-.hljs-number,
-.hljs-meta,
-.hljs-built_in,
-.hljs-builtin-name,
-.hljs-literal,
-.hljs-type,
-.hljs-params {
-  color: #b45a3c;
-}
-
-/* Atelier-Plateau Green */
-.hljs-string,
-.hljs-symbol,
-.hljs-bullet {
-  color: #4b8b8b;
-}
-
-/* Atelier-Plateau Blue */
-.hljs-title,
-.hljs-section {
-  color: #7272ca;
-}
-
-/* Atelier-Plateau Purple */
-.hljs-keyword,
-.hljs-selector-tag {
-  color: #8464c4;
-}
-
-.hljs-deletion,
-.hljs-addition {
-  color: #1b1818;
-  display: inline-block;
-  width: 100%;
-}
-
-.hljs-deletion {
-  background-color: #ca4949;
-}
-
-.hljs-addition {
-  background-color: #4b8b8b;
-}
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  background: #f4ecec;
-  color: #585050;
-  padding: 0.5em;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/atelier-savanna-dark.css

@@ -1,84 +0,0 @@
-/* Base16 Atelier Savanna Dark - Theme */
-/* by Bram de Haan (http://atelierbram.github.io/syntax-highlighting/atelier-schemes/savanna) */
-/* Original Base16 color scheme by Chris Kempson (https://github.com/chriskempson/base16) */
-
-/* Atelier-Savanna Comment */
-.hljs-comment,
-.hljs-quote {
-  color: #78877d;
-}
-
-/* Atelier-Savanna Red */
-.hljs-variable,
-.hljs-template-variable,
-.hljs-attribute,
-.hljs-tag,
-.hljs-name,
-.hljs-regexp,
-.hljs-link,
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class {
-  color: #b16139;
-}
-
-/* Atelier-Savanna Orange */
-.hljs-number,
-.hljs-meta,
-.hljs-built_in,
-.hljs-builtin-name,
-.hljs-literal,
-.hljs-type,
-.hljs-params {
-  color: #9f713c;
-}
-
-/* Atelier-Savanna Green */
-.hljs-string,
-.hljs-symbol,
-.hljs-bullet {
-  color: #489963;
-}
-
-/* Atelier-Savanna Blue */
-.hljs-title,
-.hljs-section {
-  color: #478c90;
-}
-
-/* Atelier-Savanna Purple */
-.hljs-keyword,
-.hljs-selector-tag {
-  color: #55859b;
-}
-
-.hljs-deletion,
-.hljs-addition {
-  color: #171c19;
-  display: inline-block;
-  width: 100%;
-}
-
-.hljs-deletion {
-  background-color: #b16139;
-}
-
-.hljs-addition {
-  background-color: #489963;
-}
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  background: #171c19;
-  color: #87928a;
-  padding: 0.5em;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/atelier-savanna-light.css

@@ -1,84 +0,0 @@
-/* Base16 Atelier Savanna Light - Theme */
-/* by Bram de Haan (http://atelierbram.github.io/syntax-highlighting/atelier-schemes/savanna) */
-/* Original Base16 color scheme by Chris Kempson (https://github.com/chriskempson/base16) */
-
-/* Atelier-Savanna Comment */
-.hljs-comment,
-.hljs-quote {
-  color: #5f6d64;
-}
-
-/* Atelier-Savanna Red */
-.hljs-variable,
-.hljs-template-variable,
-.hljs-attribute,
-.hljs-tag,
-.hljs-name,
-.hljs-regexp,
-.hljs-link,
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class {
-  color: #b16139;
-}
-
-/* Atelier-Savanna Orange */
-.hljs-number,
-.hljs-meta,
-.hljs-built_in,
-.hljs-builtin-name,
-.hljs-literal,
-.hljs-type,
-.hljs-params {
-  color: #9f713c;
-}
-
-/* Atelier-Savanna Green */
-.hljs-string,
-.hljs-symbol,
-.hljs-bullet {
-  color: #489963;
-}
-
-/* Atelier-Savanna Blue */
-.hljs-title,
-.hljs-section {
-  color: #478c90;
-}
-
-/* Atelier-Savanna Purple */
-.hljs-keyword,
-.hljs-selector-tag {
-  color: #55859b;
-}
-
-.hljs-deletion,
-.hljs-addition {
-  color: #171c19;
-  display: inline-block;
-  width: 100%;
-}
-
-.hljs-deletion {
-  background-color: #b16139;
-}
-
-.hljs-addition {
-  background-color: #489963;
-}
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  background: #ecf4ee;
-  color: #526057;
-  padding: 0.5em;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/atelier-seaside-dark.css

@@ -1,69 +0,0 @@
-/* Base16 Atelier Seaside Dark - Theme */
-/* by Bram de Haan (http://atelierbram.github.io/syntax-highlighting/atelier-schemes/seaside) */
-/* Original Base16 color scheme by Chris Kempson (https://github.com/chriskempson/base16) */
-
-/* Atelier-Seaside Comment */
-.hljs-comment,
-.hljs-quote {
-  color: #809980;
-}
-
-/* Atelier-Seaside Red */
-.hljs-variable,
-.hljs-template-variable,
-.hljs-attribute,
-.hljs-tag,
-.hljs-name,
-.hljs-regexp,
-.hljs-link,
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class {
-  color: #e6193c;
-}
-
-/* Atelier-Seaside Orange */
-.hljs-number,
-.hljs-meta,
-.hljs-built_in,
-.hljs-builtin-name,
-.hljs-literal,
-.hljs-type,
-.hljs-params {
-  color: #87711d;
-}
-
-/* Atelier-Seaside Green */
-.hljs-string,
-.hljs-symbol,
-.hljs-bullet {
-  color: #29a329;
-}
-
-/* Atelier-Seaside Blue */
-.hljs-title,
-.hljs-section {
-  color: #3d62f5;
-}
-
-/* Atelier-Seaside Purple */
-.hljs-keyword,
-.hljs-selector-tag {
-  color: #ad2bee;
-}
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  background: #131513;
-  color: #8ca68c;
-  padding: 0.5em;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/atelier-seaside-light.css

@@ -1,69 +0,0 @@
-/* Base16 Atelier Seaside Light - Theme */
-/* by Bram de Haan (http://atelierbram.github.io/syntax-highlighting/atelier-schemes/seaside) */
-/* Original Base16 color scheme by Chris Kempson (https://github.com/chriskempson/base16) */
-
-/* Atelier-Seaside Comment */
-.hljs-comment,
-.hljs-quote {
-  color: #687d68;
-}
-
-/* Atelier-Seaside Red */
-.hljs-variable,
-.hljs-template-variable,
-.hljs-attribute,
-.hljs-tag,
-.hljs-name,
-.hljs-regexp,
-.hljs-link,
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class {
-  color: #e6193c;
-}
-
-/* Atelier-Seaside Orange */
-.hljs-number,
-.hljs-meta,
-.hljs-built_in,
-.hljs-builtin-name,
-.hljs-literal,
-.hljs-type,
-.hljs-params {
-  color: #87711d;
-}
-
-/* Atelier-Seaside Green */
-.hljs-string,
-.hljs-symbol,
-.hljs-bullet {
-  color: #29a329;
-}
-
-/* Atelier-Seaside Blue */
-.hljs-title,
-.hljs-section {
-  color: #3d62f5;
-}
-
-/* Atelier-Seaside Purple */
-.hljs-keyword,
-.hljs-selector-tag {
-  color: #ad2bee;
-}
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  background: #f4fbf4;
-  color: #5e6e5e;
-  padding: 0.5em;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/atelier-sulphurpool-dark.css

@@ -1,69 +0,0 @@
-/* Base16 Atelier Sulphurpool Dark - Theme */
-/* by Bram de Haan (http://atelierbram.github.io/syntax-highlighting/atelier-schemes/sulphurpool) */
-/* Original Base16 color scheme by Chris Kempson (https://github.com/chriskempson/base16) */
-
-/* Atelier-Sulphurpool Comment */
-.hljs-comment,
-.hljs-quote {
-  color: #898ea4;
-}
-
-/* Atelier-Sulphurpool Red */
-.hljs-variable,
-.hljs-template-variable,
-.hljs-attribute,
-.hljs-tag,
-.hljs-name,
-.hljs-regexp,
-.hljs-link,
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class {
-  color: #c94922;
-}
-
-/* Atelier-Sulphurpool Orange */
-.hljs-number,
-.hljs-meta,
-.hljs-built_in,
-.hljs-builtin-name,
-.hljs-literal,
-.hljs-type,
-.hljs-params {
-  color: #c76b29;
-}
-
-/* Atelier-Sulphurpool Green */
-.hljs-string,
-.hljs-symbol,
-.hljs-bullet {
-  color: #ac9739;
-}
-
-/* Atelier-Sulphurpool Blue */
-.hljs-title,
-.hljs-section {
-  color: #3d8fd1;
-}
-
-/* Atelier-Sulphurpool Purple */
-.hljs-keyword,
-.hljs-selector-tag {
-  color: #6679cc;
-}
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  background: #202746;
-  color: #979db4;
-  padding: 0.5em;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/atelier-sulphurpool-light.css

@@ -1,69 +0,0 @@
-/* Base16 Atelier Sulphurpool Light - Theme */
-/* by Bram de Haan (http://atelierbram.github.io/syntax-highlighting/atelier-schemes/sulphurpool) */
-/* Original Base16 color scheme by Chris Kempson (https://github.com/chriskempson/base16) */
-
-/* Atelier-Sulphurpool Comment */
-.hljs-comment,
-.hljs-quote {
-  color: #6b7394;
-}
-
-/* Atelier-Sulphurpool Red */
-.hljs-variable,
-.hljs-template-variable,
-.hljs-attribute,
-.hljs-tag,
-.hljs-name,
-.hljs-regexp,
-.hljs-link,
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class {
-  color: #c94922;
-}
-
-/* Atelier-Sulphurpool Orange */
-.hljs-number,
-.hljs-meta,
-.hljs-built_in,
-.hljs-builtin-name,
-.hljs-literal,
-.hljs-type,
-.hljs-params {
-  color: #c76b29;
-}
-
-/* Atelier-Sulphurpool Green */
-.hljs-string,
-.hljs-symbol,
-.hljs-bullet {
-  color: #ac9739;
-}
-
-/* Atelier-Sulphurpool Blue */
-.hljs-title,
-.hljs-section {
-  color: #3d8fd1;
-}
-
-/* Atelier-Sulphurpool Purple */
-.hljs-keyword,
-.hljs-selector-tag {
-  color: #6679cc;
-}
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  background: #f5f7ff;
-  color: #5e6687;
-  padding: 0.5em;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/brown-paper.css

@@ -1,64 +0,0 @@
-/*
-
-Brown Paper style from goldblog.com.ua (c) Zaripov Yura <yur4ik7@ukr.net>
-
-*/
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  padding: 0.5em;
-  background:#b7a68e url(./brown-papersq.png);
-}
-
-.hljs-keyword,
-.hljs-selector-tag,
-.hljs-literal {
-  color:#005599;
-  font-weight:bold;
-}
-
-.hljs,
-.hljs-subst {
-  color: #363c69;
-}
-
-.hljs-string,
-.hljs-title,
-.hljs-section,
-.hljs-type,
-.hljs-attribute,
-.hljs-symbol,
-.hljs-bullet,
-.hljs-built_in,
-.hljs-addition,
-.hljs-variable,
-.hljs-template-tag,
-.hljs-template-variable,
-.hljs-link,
-.hljs-name {
-  color: #2c009f;
-}
-
-.hljs-comment,
-.hljs-quote,
-.hljs-meta,
-.hljs-deletion {
-  color: #802022;
-}
-
-.hljs-keyword,
-.hljs-selector-tag,
-.hljs-literal,
-.hljs-doctag,
-.hljs-title,
-.hljs-section,
-.hljs-type,
-.hljs-name,
-.hljs-strong {
-  font-weight: bold;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}

doc/html-manual/highlight/styles/codepen-embed.css

@@ -1,60 +0,0 @@
-/*
-  codepen.io Embed Theme
-  Author: Justin Perry <http://github.com/ourmaninamsterdam>
-  Original theme - https://github.com/chriskempson/tomorrow-theme
-*/
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  padding: 0.5em;
-  background: #222;
-  color: #fff;
-}
-
-.hljs-comment,
-.hljs-quote {
-  color: #777;
-}
-
-.hljs-variable,
-.hljs-template-variable,
-.hljs-tag,
-.hljs-regexp,
-.hljs-meta,
-.hljs-number,
-.hljs-built_in,
-.hljs-builtin-name,
-.hljs-literal,
-.hljs-params,
-.hljs-symbol,
-.hljs-bullet,
-.hljs-link,
-.hljs-deletion {
-  color: #ab875d;
-}
-
-.hljs-section,
-.hljs-title,
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class,
-.hljs-type,
-.hljs-attribute {
-  color: #9b869b;
-}
-
-.hljs-string,
-.hljs-keyword,
-.hljs-selector-tag,
-.hljs-addition {
-  color: #8f9c6c;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/color-brewer.css

@@ -1,71 +0,0 @@
-/*
-
-Colorbrewer theme
-Original: https://github.com/mbostock/colorbrewer-theme (c) Mike Bostock <mike@ocks.org>
-Ported by Fabrício Tavares de Oliveira
-
-*/
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  padding: 0.5em;
-  background: #fff;
-}
-
-.hljs,
-.hljs-subst {
-  color: #000;
-}
-
-.hljs-string,
-.hljs-meta,
-.hljs-symbol,
-.hljs-template-tag,
-.hljs-template-variable,
-.hljs-addition {
-  color: #756bb1;
-}
-
-.hljs-comment,
-.hljs-quote {
-  color: #636363;
-}
-
-.hljs-number,
-.hljs-regexp,
-.hljs-literal,
-.hljs-bullet,
-.hljs-link {
-  color: #31a354;
-}
-
-.hljs-deletion,
-.hljs-variable {
-  color: #88f;
-}
-
-
-
-.hljs-keyword,
-.hljs-selector-tag,
-.hljs-title,
-.hljs-section,
-.hljs-built_in,
-.hljs-doctag,
-.hljs-type,
-.hljs-tag,
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class,
-.hljs-strong {
-  color: #3182bd;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-attribute {
-  color: #e6550d;
-}

doc/html-manual/highlight/styles/dark.css

@@ -1,63 +0,0 @@
-/*
-
-Dark style from softwaremaniacs.org (c) Ivan Sagalaev <Maniac@SoftwareManiacs.Org>
-
-*/
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  padding: 0.5em;
-  background: #444;
-}
-
-.hljs-keyword,
-.hljs-selector-tag,
-.hljs-literal,
-.hljs-section,
-.hljs-link {
-  color: white;
-}
-
-.hljs,
-.hljs-subst {
-  color: #ddd;
-}
-
-.hljs-string,
-.hljs-title,
-.hljs-name,
-.hljs-type,
-.hljs-attribute,
-.hljs-symbol,
-.hljs-bullet,
-.hljs-built_in,
-.hljs-addition,
-.hljs-variable,
-.hljs-template-tag,
-.hljs-template-variable {
-  color: #d88;
-}
-
-.hljs-comment,
-.hljs-quote,
-.hljs-deletion,
-.hljs-meta {
-  color: #777;
-}
-
-.hljs-keyword,
-.hljs-selector-tag,
-.hljs-literal,
-.hljs-title,
-.hljs-section,
-.hljs-doctag,
-.hljs-type,
-.hljs-name,
-.hljs-strong {
-  font-weight: bold;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}

doc/html-manual/highlight/styles/darkula.css

@@ -1,6 +0,0 @@
-/*
-  Deprecated due to a typo in the name and left here for compatibility purpose only.
-  Please use darcula.css instead.
-*/
-
-@import url('darcula.css');

doc/html-manual/highlight/styles/default.css

@@ -1,99 +0,0 @@
-/*
-
-Original highlight.js style (c) Ivan Sagalaev <maniac@softwaremaniacs.org>
-
-*/
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  padding: 0.5em;
-  background: #F0F0F0;
-}
-
-
-/* Base color: saturation 0; */
-
-.hljs,
-.hljs-subst {
-  color: #444;
-}
-
-.hljs-comment {
-  color: #888888;
-}
-
-.hljs-keyword,
-.hljs-attribute,
-.hljs-selector-tag,
-.hljs-meta-keyword,
-.hljs-doctag,
-.hljs-name {
-  font-weight: bold;
-}
-
-
-/* User color: hue: 0 */
-
-.hljs-type,
-.hljs-string,
-.hljs-number,
-.hljs-selector-id,
-.hljs-selector-class,
-.hljs-quote,
-.hljs-template-tag,
-.hljs-deletion {
-  color: #880000;
-}
-
-.hljs-title,
-.hljs-section {
-  color: #880000;
-  font-weight: bold;
-}
-
-.hljs-regexp,
-.hljs-symbol,
-.hljs-variable,
-.hljs-template-variable,
-.hljs-link,
-.hljs-selector-attr,
-.hljs-selector-pseudo {
-  color: #BC6060;
-}
-
-
-/* Language color: hue: 90; */
-
-.hljs-literal {
-  color: #78A960;
-}
-
-.hljs-built_in,
-.hljs-bullet,
-.hljs-code,
-.hljs-addition {
-  color: #397300;
-}
-
-
-/* Meta color: hue: 200 */
-
-.hljs-meta {
-  color: #1f7199;
-}
-
-.hljs-meta-string {
-  color: #4d99bf;
-}
-
-
-/* Misc effects */
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/docco.css

@@ -1,97 +0,0 @@
-/*
-Docco style used in http://jashkenas.github.com/docco/ converted by Simon Madine (@thingsinjars)
-*/
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  padding: 0.5em;
-  color: #000;
-  background: #f8f8ff;
-}
-
-.hljs-comment,
-.hljs-quote {
-  color: #408080;
-  font-style: italic;
-}
-
-.hljs-keyword,
-.hljs-selector-tag,
-.hljs-literal,
-.hljs-subst {
-  color: #954121;
-}
-
-.hljs-number {
-  color: #40a070;
-}
-
-.hljs-string,
-.hljs-doctag {
-  color: #219161;
-}
-
-.hljs-selector-id,
-.hljs-selector-class,
-.hljs-section,
-.hljs-type {
-  color: #19469d;
-}
-
-.hljs-params {
-  color: #00f;
-}
-
-.hljs-title {
-  color: #458;
-  font-weight: bold;
-}
-
-.hljs-tag,
-.hljs-name,
-.hljs-attribute {
-  color: #000080;
-  font-weight: normal;
-}
-
-.hljs-variable,
-.hljs-template-variable {
-  color: #008080;
-}
-
-.hljs-regexp,
-.hljs-link {
-  color: #b68;
-}
-
-.hljs-symbol,
-.hljs-bullet {
-  color: #990073;
-}
-
-.hljs-built_in,
-.hljs-builtin-name {
-  color: #0086b3;
-}
-
-.hljs-meta {
-  color: #999;
-  font-weight: bold;
-}
-
-.hljs-deletion {
-  background: #fdd;
-}
-
-.hljs-addition {
-  background: #dfd;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/dracula.css

@@ -1,76 +0,0 @@
-/*
-
-Dracula Theme v1.2.0
-
-https://github.com/zenorocha/dracula-theme
-
-Copyright 2015, All rights reserved
-
-Code licensed under the MIT license
-http://zenorocha.mit-license.org
-
-@author Éverton Ribeiro <nuxlli@gmail.com>
-@author Zeno Rocha <hi@zenorocha.com>
-
-*/
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  padding: 0.5em;
-  background: #282a36;
-}
-
-.hljs-keyword,
-.hljs-selector-tag,
-.hljs-literal,
-.hljs-section,
-.hljs-link {
-  color: #8be9fd;
-}
-
-.hljs-function .hljs-keyword {
-  color: #ff79c6;
-}
-
-.hljs,
-.hljs-subst {
-  color: #f8f8f2;
-}
-
-.hljs-string,
-.hljs-title,
-.hljs-name,
-.hljs-type,
-.hljs-attribute,
-.hljs-symbol,
-.hljs-bullet,
-.hljs-addition,
-.hljs-variable,
-.hljs-template-tag,
-.hljs-template-variable {
-  color: #f1fa8c;
-}
-
-.hljs-comment,
-.hljs-quote,
-.hljs-deletion,
-.hljs-meta {
-  color: #6272a4;
-}
-
-.hljs-keyword,
-.hljs-selector-tag,
-.hljs-literal,
-.hljs-title,
-.hljs-section,
-.hljs-doctag,
-.hljs-type,
-.hljs-name,
-.hljs-strong {
-  font-weight: bold;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}

doc/html-manual/highlight/styles/far.css

@@ -1,71 +0,0 @@
-/*
-
-FAR Style (c) MajestiC <majestic2k@gmail.com>
-
-*/
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  padding: 0.5em;
-  background: #000080;
-}
-
-.hljs,
-.hljs-subst {
-  color: #0ff;
-}
-
-.hljs-string,
-.hljs-attribute,
-.hljs-symbol,
-.hljs-bullet,
-.hljs-built_in,
-.hljs-builtin-name,
-.hljs-template-tag,
-.hljs-template-variable,
-.hljs-addition {
-  color: #ff0;
-}
-
-.hljs-keyword,
-.hljs-selector-tag,
-.hljs-section,
-.hljs-type,
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class,
-.hljs-variable {
-  color: #fff;
-}
-
-.hljs-comment,
-.hljs-quote,
-.hljs-doctag,
-.hljs-deletion {
-  color: #888;
-}
-
-.hljs-number,
-.hljs-regexp,
-.hljs-literal,
-.hljs-link {
-  color: #0f0;
-}
-
-.hljs-meta {
-  color: #008080;
-}
-
-.hljs-keyword,
-.hljs-selector-tag,
-.hljs-title,
-.hljs-section,
-.hljs-name,
-.hljs-strong {
-  font-weight: bold;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}

doc/html-manual/highlight/styles/foundation.css

@@ -1,88 +0,0 @@
-/*
-Description: Foundation 4 docs style for highlight.js
-Author: Dan Allen <dan.j.allen@gmail.com>
-Website: http://foundation.zurb.com/docs/
-Version: 1.0
-Date: 2013-04-02
-*/
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  padding: 0.5em;
-  background: #eee; color: black;
-}
-
-.hljs-link,
-.hljs-emphasis,
-.hljs-attribute,
-.hljs-addition {
-  color: #070;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong,
-.hljs-string,
-.hljs-deletion {
-  color: #d14;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}
-
-.hljs-quote,
-.hljs-comment {
-  color: #998;
-  font-style: italic;
-}
-
-.hljs-section,
-.hljs-title {
-  color: #900;
-}
-
-.hljs-class .hljs-title,
-.hljs-type {
-  color: #458;
-}
-
-.hljs-variable,
-.hljs-template-variable {
-  color: #336699;
-}
-
-.hljs-bullet {
-  color: #997700;
-}
-
-.hljs-meta {
-  color: #3344bb;
-}
-
-.hljs-code,
-.hljs-number,
-.hljs-literal,
-.hljs-keyword,
-.hljs-selector-tag {
-  color: #099;
-}
-
-.hljs-regexp {
-  background-color: #fff0ff;
-  color: #880088;
-}
-
-.hljs-symbol {
-  color: #990073;
-}
-
-.hljs-tag,
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class {
-  color: #007700;
-}

doc/html-manual/highlight/styles/github-gist.css

@@ -1,71 +0,0 @@
-/**
- * GitHub Gist Theme
- * Author : Louis Barranqueiro - https://github.com/LouisBarranqueiro
- */
-
-.hljs {
-  display: block;
-  background: white;
-  padding: 0.5em;
-  color: #333333;
-  overflow-x: auto;
-}
-
-.hljs-comment,
-.hljs-meta {
-  color: #969896;
-}
-
-.hljs-string,
-.hljs-variable,
-.hljs-template-variable,
-.hljs-strong,
-.hljs-emphasis,
-.hljs-quote {
-  color: #df5000;
-}
-
-.hljs-keyword,
-.hljs-selector-tag,
-.hljs-type {
-  color: #a71d5d;
-}
-
-.hljs-literal,
-.hljs-symbol,
-.hljs-bullet,
-.hljs-attribute {
-  color: #0086b3;
-}
-
-.hljs-section,
-.hljs-name {
-  color: #63a35c;
-}
-
-.hljs-tag {
-  color: #333333;
-}
-
-.hljs-title,
-.hljs-attr,
-.hljs-selector-id,
-.hljs-selector-class,
-.hljs-selector-attr,
-.hljs-selector-pseudo {
-  color: #795da3;
-}
-
-.hljs-addition {
-  color: #55a532;
-  background-color: #eaffea;
-}
-
-.hljs-deletion {
-  color: #bd2c00;
-  background-color: #ffecec;
-}
-
-.hljs-link {
-  text-decoration: underline;
-}

doc/html-manual/highlight/styles/github.css

@@ -1,99 +0,0 @@
-/*
-
-github.com style (c) Vasily Polovnyov <vast@whiteants.net>
-
-*/
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  padding: 0.5em;
-  color: #333;
-  background: #f8f8f8;
-}
-
-.hljs-comment,
-.hljs-quote {
-  color: #998;
-  font-style: italic;
-}
-
-.hljs-keyword,
-.hljs-selector-tag,
-.hljs-subst {
-  color: #333;
-  font-weight: bold;
-}
-
-.hljs-number,
-.hljs-literal,
-.hljs-variable,
-.hljs-template-variable,
-.hljs-tag .hljs-attr {
-  color: #008080;
-}
-
-.hljs-string,
-.hljs-doctag {
-  color: #d14;
-}
-
-.hljs-title,
-.hljs-section,
-.hljs-selector-id {
-  color: #900;
-  font-weight: bold;
-}
-
-.hljs-subst {
-  font-weight: normal;
-}
-
-.hljs-type,
-.hljs-class .hljs-title {
-  color: #458;
-  font-weight: bold;
-}
-
-.hljs-tag,
-.hljs-name,
-.hljs-attribute {
-  color: #000080;
-  font-weight: normal;
-}
-
-.hljs-regexp,
-.hljs-link {
-  color: #009926;
-}
-
-.hljs-symbol,
-.hljs-bullet {
-  color: #990073;
-}
-
-.hljs-built_in,
-.hljs-builtin-name {
-  color: #0086b3;
-}
-
-.hljs-meta {
-  color: #999;
-  font-weight: bold;
-}
-
-.hljs-deletion {
-  background: #fdd;
-}
-
-.hljs-addition {
-  background: #dfd;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/googlecode.css

@@ -1,89 +0,0 @@
-/*
-
-Google Code style (c) Aahan Krish <geekpanth3r@gmail.com>
-
-*/
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  padding: 0.5em;
-  background: white;
-  color: black;
-}
-
-.hljs-comment,
-.hljs-quote {
-  color: #800;
-}
-
-.hljs-keyword,
-.hljs-selector-tag,
-.hljs-section,
-.hljs-title,
-.hljs-name {
-  color: #008;
-}
-
-.hljs-variable,
-.hljs-template-variable {
-  color: #660;
-}
-
-.hljs-string,
-.hljs-selector-attr,
-.hljs-selector-pseudo,
-.hljs-regexp {
-  color: #080;
-}
-
-.hljs-literal,
-.hljs-symbol,
-.hljs-bullet,
-.hljs-meta,
-.hljs-number,
-.hljs-link {
-  color: #066;
-}
-
-.hljs-title,
-.hljs-doctag,
-.hljs-type,
-.hljs-attr,
-.hljs-built_in,
-.hljs-builtin-name,
-.hljs-params {
-  color: #606;
-}
-
-.hljs-attribute,
-.hljs-subst {
-  color: #000;
-}
-
-.hljs-formula {
-  background-color: #eee;
-  font-style: italic;
-}
-
-.hljs-selector-id,
-.hljs-selector-class {
-  color: #9B703F
-}
-
-.hljs-addition {
-  background-color: #baeeba;
-}
-
-.hljs-deletion {
-  background-color: #ffc8bd;
-}
-
-.hljs-doctag,
-.hljs-strong {
-  font-weight: bold;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}

doc/html-manual/highlight/styles/grayscale.css

@@ -1,101 +0,0 @@
-/*
-
-grayscale style (c) MY Sun <simonmysun@gmail.com>
-
-*/
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  padding: 0.5em;
-  color: #333;
-  background: #fff;
-}
-
-.hljs-comment,
-.hljs-quote {
-  color: #777;
-  font-style: italic;
-}
-
-.hljs-keyword,
-.hljs-selector-tag,
-.hljs-subst {
-  color: #333;
-  font-weight: bold;
-}
-
-.hljs-number,
-.hljs-literal {
-  color: #777;
-}
-
-.hljs-string,
-.hljs-doctag,
-.hljs-formula {
-  color: #333;
-  background: url(data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAAQAAAAECAYAAACp8Z5+AAAAJ0lEQVQIW2O8e/fufwYGBgZBQUEQxcCIIfDu3Tuwivfv30NUoAsAALHpFMMLqZlPAAAAAElFTkSuQmCC) repeat;
-}
-
-.hljs-title,
-.hljs-section,
-.hljs-selector-id {
-  color: #000;
-  font-weight: bold;
-}
-
-.hljs-subst {
-  font-weight: normal;
-}
-
-.hljs-class .hljs-title,
-.hljs-type,
-.hljs-name {
-  color: #333;
-  font-weight: bold;
-}
-
-.hljs-tag {
-  color: #333;
-}
-
-.hljs-regexp {
-    color: #333;
-    background: url(data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAAoAAAAICAYAAADA+m62AAAAPUlEQVQYV2NkQAN37979r6yszIgujiIAU4RNMVwhuiQ6H6wQl3XI4oy4FMHcCJPHcDS6J2A2EqUQpJhohQDexSef15DBCwAAAABJRU5ErkJggg==) repeat;
-}
-
-.hljs-symbol,
-.hljs-bullet,
-.hljs-link {
-  color: #000;
-  background: url(data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAAUAAAAFCAYAAACNbyblAAAAKElEQVQIW2NkQAO7d+/+z4gsBhJwdXVlhAvCBECKwIIwAbhKZBUwBQA6hBpm5efZsgAAAABJRU5ErkJggg==) repeat;
-}
-
-.hljs-built_in,
-.hljs-builtin-name {
-  color: #000;
-  text-decoration: underline;
-}
-
-.hljs-meta {
-  color: #999;
-  font-weight: bold;
-}
-
-.hljs-deletion {
-  color: #fff;
-  background:url(data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAAEAAAADCAYAAABS3WWCAAAAE0lEQVQIW2MMDQ39zzhz5kwIAQAyxweWgUHd1AAAAABJRU5ErkJggg==) repeat;
-}
-
-.hljs-addition {
-  color: #000;
-  background: url(data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAAkAAAAJCAYAAADgkQYQAAAALUlEQVQYV2N89+7dfwYk8P79ewZBQUFkIQZGOiu6e/cuiptQHAPl0NtNxAQBAM97Oejj3Dg7AAAAAElFTkSuQmCC) repeat;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/gruvbox-dark.css

@@ -1,108 +0,0 @@
-/*
-
-Gruvbox style (dark) (c) Pavel Pertsev (original style at https://github.com/morhetz/gruvbox)
-
-*/
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  padding: 0.5em;
-  background: #282828;
-}
-
-.hljs,
-.hljs-subst {
-  color: #ebdbb2;
-}
-
-/* Gruvbox Red */
-.hljs-deletion,
-.hljs-formula,
-.hljs-keyword,
-.hljs-link,
-.hljs-selector-tag {
-  color: #fb4934;
-}
-
-/* Gruvbox Blue */
-.hljs-built_in,
-.hljs-emphasis,
-.hljs-name,
-.hljs-quote,
-.hljs-strong,
-.hljs-title,
-.hljs-variable {
-  color: #83a598;
-}
-
-/* Gruvbox Yellow */
-.hljs-attr,
-.hljs-params,
-.hljs-template-tag,
-.hljs-type {
-  color: #fabd2f;
-}
-
-/* Gruvbox Purple */
-.hljs-builtin-name,
-.hljs-doctag,
-.hljs-literal,
-.hljs-number {
-  color: #8f3f71;
-}
-
-/* Gruvbox Orange */
-.hljs-code,
-.hljs-meta,
-.hljs-regexp,
-.hljs-selector-id,
-.hljs-template-variable {
-  color: #fe8019;
-}
-
-/* Gruvbox Green */
-.hljs-addition,
-.hljs-meta-string,
-.hljs-section,
-.hljs-selector-attr,
-.hljs-selector-class,
-.hljs-string,
-.hljs-symbol {
-  color: #b8bb26;
-}
-
-/* Gruvbox Aqua */
-.hljs-attribute,
-.hljs-bullet,
-.hljs-class,
-.hljs-function,
-.hljs-function .hljs-keyword,
-.hljs-meta-keyword,
-.hljs-selector-pseudo,
-.hljs-tag {
-  color: #8ec07c;
-}
-
-/* Gruvbox Gray */
-.hljs-comment {
-  color: #928374;
-}
-
-/* Gruvbox Purple */
-.hljs-link_label,
-.hljs-literal,
-.hljs-number {
-  color: #d3869b;
-}
-
-.hljs-comment,
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-section,
-.hljs-strong,
-.hljs-tag {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/gruvbox-light.css

@@ -1,108 +0,0 @@
-/*
-
-Gruvbox style (light) (c) Pavel Pertsev (original style at https://github.com/morhetz/gruvbox)
-
-*/
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  padding: 0.5em;
-  background: #fbf1c7;
-}
-
-.hljs,
-.hljs-subst {
-  color: #3c3836;
-}
-
-/* Gruvbox Red */
-.hljs-deletion,
-.hljs-formula,
-.hljs-keyword,
-.hljs-link,
-.hljs-selector-tag {
-  color: #9d0006;
-}
-
-/* Gruvbox Blue */
-.hljs-built_in,
-.hljs-emphasis,
-.hljs-name,
-.hljs-quote,
-.hljs-strong,
-.hljs-title,
-.hljs-variable {
-  color: #076678;
-}
-
-/* Gruvbox Yellow */
-.hljs-attr,
-.hljs-params,
-.hljs-template-tag,
-.hljs-type {
-  color: #b57614;
-}
-
-/* Gruvbox Purple */
-.hljs-builtin-name,
-.hljs-doctag,
-.hljs-literal,
-.hljs-number {
-  color: #8f3f71;
-}
-
-/* Gruvbox Orange */
-.hljs-code,
-.hljs-meta,
-.hljs-regexp,
-.hljs-selector-id,
-.hljs-template-variable {
-  color: #af3a03;
-}
-
-/* Gruvbox Green */
-.hljs-addition,
-.hljs-meta-string,
-.hljs-section,
-.hljs-selector-attr,
-.hljs-selector-class,
-.hljs-string,
-.hljs-symbol {
-  color: #79740e;
-}
-
-/* Gruvbox Aqua */
-.hljs-attribute,
-.hljs-bullet,
-.hljs-class,
-.hljs-function,
-.hljs-function .hljs-keyword,
-.hljs-meta-keyword,
-.hljs-selector-pseudo,
-.hljs-tag {
-  color: #427b58;
-}
-
-/* Gruvbox Gray */
-.hljs-comment {
-  color: #928374;
-}
-
-/* Gruvbox Purple */
-.hljs-link_label,
-.hljs-literal,
-.hljs-number {
-  color: #8f3f71;
-}
-
-.hljs-comment,
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-section,
-.hljs-strong,
-.hljs-tag {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/hopscotch.css

@@ -1,83 +0,0 @@
-/*
- * Hopscotch
- * by Jan T. Sott
- * https://github.com/idleberg/Hopscotch
- *
- * This work is licensed under the Creative Commons CC0 1.0 Universal License
- */
-
-/* Comment */
-.hljs-comment,
-.hljs-quote {
-  color: #989498;
-}
-
-/* Red */
-.hljs-variable,
-.hljs-template-variable,
-.hljs-attribute,
-.hljs-tag,
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class,
-.hljs-regexp,
-.hljs-link,
-.hljs-deletion {
-  color: #dd464c;
-}
-
-/* Orange */
-.hljs-number,
-.hljs-built_in,
-.hljs-builtin-name,
-.hljs-literal,
-.hljs-type,
-.hljs-params {
-  color: #fd8b19;
-}
-
-/* Yellow */
-.hljs-class .hljs-title {
-  color: #fdcc59;
-}
-
-/* Green */
-.hljs-string,
-.hljs-symbol,
-.hljs-bullet,
-.hljs-addition {
-  color: #8fc13e;
-}
-
-/* Aqua */
-.hljs-meta {
-  color: #149b93;
-}
-
-/* Blue */
-.hljs-function,
-.hljs-section,
-.hljs-title {
-  color: #1290bf;
-}
-
-/* Purple */
-.hljs-keyword,
-.hljs-selector-tag {
-  color: #c85e7c;
-}
-
-.hljs {
-  display: block;
-  background: #322931;
-  color: #b9b5b8;
-  padding: 0.5em;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/hybrid.css

@@ -1,102 +0,0 @@
-/*
-
-vim-hybrid theme by w0ng (https://github.com/w0ng/vim-hybrid)
-
-*/
-
-/*background color*/
-.hljs {
-  display: block;
-  overflow-x: auto;
-  padding: 0.5em;
-  background: #1d1f21;
-}
-
-/*selection color*/
-.hljs::selection,
-.hljs span::selection {
-  background: #373b41;
-}
-
-.hljs::-moz-selection,
-.hljs span::-moz-selection {
-  background: #373b41;
-}
-
-/*foreground color*/
-.hljs {
-  color: #c5c8c6;
-}
-
-/*color: fg_yellow*/
-.hljs-title,
-.hljs-name {
-  color: #f0c674;
-}
-
-/*color: fg_comment*/
-.hljs-comment,
-.hljs-meta,
-.hljs-meta .hljs-keyword {
-  color: #707880;
-}
-
-/*color: fg_red*/
-.hljs-number,
-.hljs-symbol,
-.hljs-literal,
-.hljs-deletion,
-.hljs-link {
- color: #cc6666
-}
-
-/*color: fg_green*/
-.hljs-string,
-.hljs-doctag,
-.hljs-addition,
-.hljs-regexp,
-.hljs-selector-attr,
-.hljs-selector-pseudo {
-  color: #b5bd68;
-}
-
-/*color: fg_purple*/
-.hljs-attribute,
-.hljs-code,
-.hljs-selector-id {
- color: #b294bb;
-}
-
-/*color: fg_blue*/
-.hljs-keyword,
-.hljs-selector-tag,
-.hljs-bullet,
-.hljs-tag {
- color: #81a2be;
-}
-
-/*color: fg_aqua*/
-.hljs-subst,
-.hljs-variable,
-.hljs-template-tag,
-.hljs-template-variable {
-  color: #8abeb7;
-}
-
-/*color: fg_orange*/
-.hljs-type,
-.hljs-built_in,
-.hljs-builtin-name,
-.hljs-quote,
-.hljs-section,
-.hljs-selector-class {
-  color: #de935f;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/idea.css

@@ -1,97 +0,0 @@
-/*
-
-Intellij Idea-like styling (c) Vasily Polovnyov <vast@whiteants.net>
-
-*/
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  padding: 0.5em;
-  color: #000;
-  background: #fff;
-}
-
-.hljs-subst,
-.hljs-title {
-  font-weight: normal;
-  color: #000;
-}
-
-.hljs-comment,
-.hljs-quote {
-  color: #808080;
-  font-style: italic;
-}
-
-.hljs-meta {
-  color: #808000;
-}
-
-.hljs-tag {
-  background: #efefef;
-}
-
-.hljs-section,
-.hljs-name,
-.hljs-literal,
-.hljs-keyword,
-.hljs-selector-tag,
-.hljs-type,
-.hljs-selector-id,
-.hljs-selector-class {
-  font-weight: bold;
-  color: #000080;
-}
-
-.hljs-attribute,
-.hljs-number,
-.hljs-regexp,
-.hljs-link {
-  font-weight: bold;
-  color: #0000ff;
-}
-
-.hljs-number,
-.hljs-regexp,
-.hljs-link {
-  font-weight: normal;
-}
-
-.hljs-string {
-  color: #008000;
-  font-weight: bold;
-}
-
-.hljs-symbol,
-.hljs-bullet,
-.hljs-formula {
-  color: #000;
-  background: #d0eded;
-  font-style: italic;
-}
-
-.hljs-doctag {
-  text-decoration: underline;
-}
-
-.hljs-variable,
-.hljs-template-variable {
-  color: #660e7a;
-}
-
-.hljs-addition {
-  background: #baeeba;
-}
-
-.hljs-deletion {
-  background: #ffc8bd;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/ir-black.css

@@ -1,73 +0,0 @@
-/*
-  IR_Black style (c) Vasily Mikhailitchenko <vaskas@programica.ru>
-*/
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  padding: 0.5em;
-  background: #000;
-  color: #f8f8f8;
-}
-
-.hljs-comment,
-.hljs-quote,
-.hljs-meta {
-  color: #7c7c7c;
-}
-
-.hljs-keyword,
-.hljs-selector-tag,
-.hljs-tag,
-.hljs-name {
-  color: #96cbfe;
-}
-
-.hljs-attribute,
-.hljs-selector-id {
-  color: #ffffb6;
-}
-
-.hljs-string,
-.hljs-selector-attr,
-.hljs-selector-pseudo,
-.hljs-addition {
-  color: #a8ff60;
-}
-
-.hljs-subst {
-  color: #daefa3;
-}
-
-.hljs-regexp,
-.hljs-link {
-  color: #e9c062;
-}
-
-.hljs-title,
-.hljs-section,
-.hljs-type,
-.hljs-doctag {
-  color: #ffffb6;
-}
-
-.hljs-symbol,
-.hljs-bullet,
-.hljs-variable,
-.hljs-template-variable,
-.hljs-literal {
-  color: #c6c5fe;
-}
-
-.hljs-number,
-.hljs-deletion {
-  color:#ff73fd;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}

doc/html-manual/highlight/styles/kimbie.dark.css

@@ -1,74 +0,0 @@
-/*
-    Name:     Kimbie (dark)
-    Author:   Jan T. Sott
-    License:  Creative Commons Attribution-ShareAlike 4.0 Unported License
-    URL:      https://github.com/idleberg/Kimbie-highlight.js
-*/
-
-/* Kimbie Comment */
-.hljs-comment,
-.hljs-quote {
-  color: #d6baad;
-}
-
-/* Kimbie Red */
-.hljs-variable,
-.hljs-template-variable,
-.hljs-tag,
-.hljs-name,
-.hljs-selector-id,
-.hljs-selector-class,
-.hljs-regexp,
-.hljs-meta {
-  color: #dc3958;
-}
-
-/* Kimbie Orange */
-.hljs-number,
-.hljs-built_in,
-.hljs-builtin-name,
-.hljs-literal,
-.hljs-type,
-.hljs-params,
-.hljs-deletion,
-.hljs-link {
-  color: #f79a32;
-}
-
-/* Kimbie Yellow */
-.hljs-title,
-.hljs-section,
-.hljs-attribute {
-  color: #f06431;
-}
-
-/* Kimbie Green */
-.hljs-string,
-.hljs-symbol,
-.hljs-bullet,
-.hljs-addition {
-  color: #889b4a;
-}
-
-/* Kimbie Purple */
-.hljs-keyword,
-.hljs-selector-tag,
-.hljs-function {
-  color: #98676a;
-}
-
-.hljs {
-  display: block;
-  overflow-x: auto;
-  background: #221a0f;
-  color: #d3af86;
-  padding: 0.5em;
-}
-
-.hljs-emphasis {
-  font-style: italic;
-}
-
-.hljs-strong {
-  font-weight: bold;
-}