diff --git a/src/sphinx/genc.rst b/src/sphinx/genc.rst
new file mode 100644
index 0000000000000000000000000000000000000000..faac1f142f843e4014dbac4603784c4fa37ebe16
--- /dev/null
+++ b/src/sphinx/genc.rst
@@ -0,0 +1,122 @@
+.. _genc:
+
+Safe C Code
+===========
+
+Leon can generate from Scala code an equivalent and safe C99 code. Using the verification, repair and
+synthesis features of Leon this conversion can be made safely. Additionally, the produced code can be
+compiled with any standard-compliant C99 compiler to target the desired hardware architecture
+without extra dependencies.
+
+To convert a Scala program, one can use the ``--genc`` and ``--o=<output.c>`` command line options
+of Leon.
+
+.. NOTE::
+ Currently the memory model is limited to stack-allocated memory. Hence, no dynamic allocation
+ is done using ``malloc`` function family.
+
+
+Supported Features
+------------------
+
+The supported subset of Scala includes part of the core languages features, as well as some
+extensions from :ref:`XLang <xlang>`, while ensuring the same expression execution order in both
+languages.
+
+Currently all type and function definitions need to be included in one top level object.
+
+
+Types
+*****
+
+The following raw types and their corresponding literals are supported:
+
+.. list-table::
+ :header-rows: 1
+
+ * - Scala
+ - C99
+ * - ``Unit``
+ - ``void``
+ * - ``Boolean``
+ - ``bool``
+ * - ``Int`` (32-bit Integer)
+ - ``int32_t``
+
+Tuples
+^^^^^^
+
+Using ``TupleN[T1, ..., TN]`` results in the creation of a C structure with the same
+fields and types for every combination of any supported type ``T1, ..., TN``. The name of the
+generated structure will be unique and reflect the sequence of types.
+
+
+Arrays
+^^^^^^
+
+``Array[T]`` are implemented using regular C array when the array size is known at compile time, or
+using Variable Length Array (VLA) when the size is only available at runtime. Both types of array
+use the same unique structure type to keep track of the length of the array and its allocated
+memory.
+
+.. NOTE::
+
+ Arrays live on the stack and therefore cannot be returned by functions. This limitation is
+ extended to other types having an array as field.
+
+
+Arrays can be created using the companion object, e.g. ``Array(1, 2, 3)``, or using the
+``Array.fill`` method, e.g. ``Array.fill(size)(value)``.
+
+
+Case Classes
+^^^^^^^^^^^^
+
+The support for classes is restricted to non-recursive case classes for which fields are immutable.
+Instances of such data-types live on the stack.
+
+
+Functions
+*********
+
+Functions and nested functions are supported, with access to the variables in their respective
+scopes. However, higher order functions are as of this moment not supported.
+
+Since strings of characters are currently not available, to generate an executable program, one has
+to define a main function without any argument that returns an integer: ``def main: Int = ...``.
+
+Both ``val`` and ``var`` are supported with the limitations imposed by the :ref:`XLang <xlang>`
+extensions.
+
+
+Constructs
+**********
+
+The idiomatic ``if`` statements such as ``val b = if (x >= 0) true else false`` are converted into
+a sequence of equivalent statements.
+
+Imperative ``while`` loops are also supported.
+
+Assertions, invariant, pre- and post-conditions are not translated into C99 and are simply ignored.
+
+
+Operators
+*********
+
+The following operators are supported:
+
+.. list-table::
+ :header-rows: 1
+
+ * - Category
+ - Operators
+ * - Boolean operators
+ - ``&&``, ``||``, ``!``, ``!=``, ``==``
+ * - Comparision operators over integers
+ - ``<``, ``<=``, ``==``, ``!=``, ``>=``, ``>``
+ * - Arithmetic operators over integers
+ - ``+``, ``-`` (unary & binary), ``*``, ``/``, ``%``
+ * - Bitwise operators over integers
+ - ``&``, ``|``, ``^``, ``~``, ``<<``, ``>>``
+
+
diff --git a/src/sphinx/index.rst b/src/sphinx/index.rst
index a20401170d34be2ef293878e72b678aaac462598..cf46d2c300d3821a4cb987d657bded60597ce534 100644
--- a/src/sphinx/index.rst
+++ b/src/sphinx/index.rst
@@ -25,6 +25,7 @@ Contents:
limitations
synthesis
repair
+ genc
options
faq
references
diff --git a/src/sphinx/options.rst b/src/sphinx/options.rst
index 1c929cd29cdc5281378cd322389b867902f0ff2b..a5be01e35269e12864cd6716947727209497b337 100644
--- a/src/sphinx/options.rst
+++ b/src/sphinx/options.rst
@@ -20,41 +20,46 @@ Choosing which Leon feature to use
The first group of options determine which feature of Leon will be used.
These options are mutually exclusive (except when noted). By default, ``--verify`` is chosen.
-* ``--eval``
-
+* ``--eval``
+
Evaluates parameterless functions and value definitions.
-
+
* ``--verify``
-
+
Proves or disproves function contracts, as explained in the :ref:`verification` section.
* ``--repair``
-
+
Runs program :ref:`repair <repair>`.
-
+
* ``--synthesis``
-
+
Partially synthesizes ``choose()`` constructs (see :ref:`synthesis` section).
* ``--termination``
-
+
Runs termination analysis. Can be used along ``--verify``.
-* ``--inferInv``
+* ``--inferInv``
+
+ Infer invariants from the (instrumented) code (using Orb).
- Infer invariants from the (instrumented) code (using Orb)
+* ``--instrument``
-* ``--instrument``
+ Instrument the code for inferring time/depth/stack bounds (using Orb).
- Instrument the code for inferring time/depth/stack bounds (using Orb)
+* ``--genc``
+
+ Translate a Scala program into C99 equivalent code (see :ref:`genc` section); requires
+ ``--xlang``.
* ``--noop``
-
+
Runs the program through the extraction and preprocessing phases, then outputs it in the specified
directory. Used mostly for debugging purposes.
* ``--help``
-
+
Prints a helpful message, then exits.
@@ -65,44 +70,46 @@ Additional top-level options
These options are available to all Leon components:
* ``--debug=d1,d2,...``
-
+
Enables printing detailed messages for the components d1,d2,... .
- Available components are:
+ Available components are:
* ``datagen`` (Data generators)
-
+
* ``eval`` (Evaluators)
-
+
+ * ``genc`` (C code generation)
+
* ``isabelle`` (:ref:`The Isabelle-based solver <isabelle>`)
* ``leon`` (The top-level component)
-
+
* ``options`` (Options parsed by Leon)
-
+
* ``positions`` (When printing, attach positions to trees)
* ``repair`` (Program repair)
-
+
* ``solver`` (SMT solvers and their wrappers)
-
+
* ``synthesis`` (Program synthesis)
-
+
* ``termination`` (Termination analysis)
-
+
* ``timers`` (Timers, timer pools)
-
+
* ``trees`` (Manipulation of trees)
-
+
* ``types`` (When printing, attach types to expressions)
* ``verification`` (Verification)
-
+
* ``xlang`` (Transformation of XLang into Pure Scala programs)
* ``--functions=f1,f2,...``
-
- Only consider functions f1, f2, ... . This applies to all functionalities
+
+ Only consider functions f1, f2, ... . This applies to all functionalities
where Leon manipulates the input in a per-function basis.
Leon will match against suffixes of qualified names. For instance:
@@ -111,22 +118,22 @@ These options are available to all Leon components:
This option supports ``_`` as wildcard: ``--functions=List._`` will
match all ``List`` methods.
-* ``--solvers=s1,s2,...``
-
- Use solvers s1, s2,... . If more than one solver is chosen, all chosen
+* ``--solvers=s1,s2,...``
+
+ Use solvers s1, s2,... . If more than one solver is chosen, all chosen
solvers will be used in parallel, and the best result will be presented.
By default, the ``fairz3`` solver is picked.
-
- Some solvers are specialized in proving verification conditions
- and will have hard time finding a counterexample in case of an invalid
+
+ Some solvers are specialized in proving verification conditions
+ and will have hard time finding a counterexample in case of an invalid
verification condition, whereas some are specialized in finding
counterexamples, and some provide a compromise between the two.
Also, some solvers do not as of now support higher-order functions.
Available solvers include:
-
- * ``enum``
-
+
+ * ``enum``
+
Uses enumeration-based techniques to discover counterexamples.
This solver does not actually invoke an SMT solver,
and operates entirely on the level of Leon trees.
@@ -134,50 +141,50 @@ These options are available to all Leon components:
* ``fairz3``
Native Z3 with z3-templates for unfolding recursive functions (default).
-
+
* ``smt-cvc4``
-
- CVC4 through SMT-LIB. An algorithm within Leon takes up the unfolding
- of recursive functions, handling of lambdas etc. To use this or any
+
+ CVC4 through SMT-LIB. An algorithm within Leon takes up the unfolding
+ of recursive functions, handling of lambdas etc. To use this or any
of the following CVC4-based solvers, you need to have the ``cvc4``
executable in your system path (the latest unstable version is recommended).
-
+
* ``smt-cvc4-cex``
-
+
CVC4 through SMT-LIB, in-solver finite-model-finding, for counter-examples only.
Recursive functions are not unrolled, but encoded through the
``define-funs-rec`` construct available in the new SMTLIB-2.5 standard.
Currently, this solver does not handle higher-order functions.
-
+
* ``smt-cvc4-proof``
-
- CVC4 through SMT-LIB, for proofs only. Functions are encoded as in
+
+ CVC4 through SMT-LIB, for proofs only. Functions are encoded as in
``smt-cvc4-cex``.
Currently, this solver does not handle higher-order functions.
-
+
* ``smt-z3``
-
- Z3 through SMT-LIB. To use this or the next solver, you need to
+
+ Z3 through SMT-LIB. To use this or the next solver, you need to
have the ``z3`` executable in your program path (the latest stable version
is recommended). Inductive reasoning happens on the Leon side
(similarly to ``smt-cvc4``).
-
+
* ``smt-z3-q``
-
- Z3 through SMT-LIB, but (recursive) functions are not unrolled and are
+
+ Z3 through SMT-LIB, but (recursive) functions are not unrolled and are
instead encoded with universal quantification.
For example, ``def foo(x:A) = e`` would be encoded by asserting
-
+
.. math::
-
+
\forall (x:A). foo(x) = e
even if ``e`` contains an invocation to ``foo``.
Currently, this solver does not handle higher-order functions.
-
+
* ``unrollz3``
-
+
Native Z3, but inductive reasoning happens within Leon (similarly to ``smt-z3``).
* ``ground``
@@ -187,21 +194,23 @@ These options are available to all Leon components:
* ``isabelle``
Solve verification conditions via Isabelle.
-
+
* ``--strict``
- Terminate Leon after each phase if a non-fatal error is encountered
+ Terminate Leon after each phase if a non-fatal error is encountered
(such as a failed verification condition). By default, this option is activated.
* ``--timeout=t``
Set a timeout for each attempt to prove one verification condition/
repair one function (in sec.)
-
+
* ``--xlang``
-
+
Support for additional language constructs described in :ref:`xlang`.
- These constructs are desugared into :ref:`purescala` before other operations.
+ These constructs are desugared into :ref:`purescala` before other operations,
+ except for the ``--genc`` option which uses the original constructs to generate
+ :ref:`genc`.
Additional Options (by component)
---------------------------------
@@ -222,10 +231,12 @@ File Output
***********
* ``--o=dir``
-
+
Output files to the directory ``dir`` (default: leon.out).
Used when ``--noop`` is selected.
+ When used with ``--genc`` this option designates the output *file*.
+
Code Extraction
***************
@@ -245,21 +256,21 @@ Synthesis
Shrink non-deterministic programs when tests pruning works well.
* ``--cegis:vanuatoo``
-
+
Generate inputs using new korat-style generator.
-
+
* ``--costmodel=cm``
-
+
Use a specific cost model for this search.
Available: ``Naive``, ``WeightedBranches``
* ``--derivtrees``
-
+
Generate a derivation tree for every synthesized function.
The trees will be output in ``*.dot`` files.
* ``--manual=cmd``
-
+
Override Leon's automated search through the space of programs during synthesis.
Instead, the user can navigate the program space manually
by choosing which deductive synthesis rules is instantiated each time.
@@ -277,26 +288,26 @@ Fair-z3 Solver
Double-check counter-examples with evaluator.
* ``--codegen``
-
+
Use compiled evaluator instead of interpreter.
* ``--evalground``
-
+
Use evaluator on functions applied to ground arguments.
-
+
* ``--feelinglucky``
-
+
Use evaluator to find counter-examples early.
* ``--unrollcores``
-
+
Use unsat-cores to drive unrolling while remaining fair.
-
+
CVC4 Solver
***********
* ``--solver:cvc4=<cvc4-opt>``
-
+
Pass extra command-line arguments to CVC4.
Isabelle