===================
QGen Model Verifier
===================

The QGen Model Verifier performs checks for MISRA violations, and verifies
that the code generated for the model does not suffer from one of the 
following possible run-time issues:

1. Possible run-time errors, including:

   a. Integer overflow

   b. Signal out of range

   c. Division by zero

2. Logic errors, including:

   a. Conditions that are always true, or always false

   b. Expressions that always return the same value

3. Other functional or safety property violations, including:

   a. Simulink Assertion blocks that might fail

Using ``qgenv``
===============

Similarly to code generation, model verification is performed by the executable
``qgenv`` which can be invoked in three methods:

1. From the Simulink GUI

2. From the MATLAB Command Line

3. From the System Command Line

From the Simulink GUI
=====================

QGen model verification can be invoked from the Simulink user interface. This
requires QGen to be correctly setup in MATLAB following the instructions in
:ref:`qgen-setup-in-matlab`.

Model verification is invoked from the window of a Simulink model by clicking on
the **QGen** menu and then **Verify**.

From the MATLAB Command Line
============================

QGen model verification can be invoked from the MATLAB command line using the
``qgen_verify`` function. This requires QGen to be correctly setup in MATLAB
following the instructions in :ref:`qgen-setup-in-matlab`.

``qgen_verify`` has two required inputs and a number of optional parameters:

.. code-block:: text

   qgen_verify (<mdl_path>, <mode> [, <options>]);

* ``mdl_path``
  
  Name of the mdl or slx file optionally with path (absolute or relative).

* ``mode``
  
  Verification mode. The accepted values are

  * ``--bug-finder``
    
    Executes a faster but less complete verification.

  * ``--proof``
    
    Executes a slower but more complete verification.

``<options>`` are all string values. Each option is either a single boolean
switch or a switch followed by a value. Options can be passed in an arbitrary
order.

.. note:: Several options correspond to identical or similar options of the
          ``qgenv`` executable. As a result, more details on options will be
          provided in :ref:`qgenv-from-command-line`.

.. note:: Options can be passed either as function arguments, or as a cell array
          of length 1 where the value of the first element is also a cell array
          containing the list of options.

The accepted boolean switches are:

* ``--wmisra``
  
  Treat violations to MISRA Simulink as warnings.

* ``--no-misra``
  
  Allow violations to MISRA Simulink.

* ``--export-ws, -w``
  
  Export workspace contents to m-file and ignore any MATLAB files passed in the
  function input.

* ``-v``
  
  Print verbose output when exporting the decoration file

* ``--clean, -c``
  
  Instructs QGen to delete all the content of the output directory before
  starting the code generation.

* ``--incremental, -i``
  
  Instructs QGen to leave the content of the output directory as is. Generated
  files will overwrite existing files with the same name, but other existing
  files will remain untouched.

Switch-value pairs shall be passed as two arguments. First is the key and the
second is value. It is assumed that the value does not start with ``'-'`` to
distinguish it from other switches

* ``--subsys``
  
  Generate code for the subsystem identified by the name in argument (the name
  is a `/`-separated path of subsystem names starting from the model root)

* ``--output, -o``
  
  Specify the code generation target directory. By default the files are placed
  in ``<modelname>_generated``.

* ``--matlab, -m``
  
  Provide a MATLAB file containing the constant, Bus and Signal definitions.

Example command:

.. code-block:: text

   qgen_verify ('test.mdl', '--proof', '-m', 'test_def.m')

.. _qgenv-from-command-line:

From the System Command Line
============================

``qgenv`` is invoked on the system command line as follows:

.. code-block:: text

 qgenv FILE [switches]

The arguments of the ``qgenv`` executable are:

* ``FILE``
  
  An slx or mdl Simulink model.

* ``--bug-finder``
  
  Executes ``qgenv`` in bug-finding mode, which perform a faster but less complete
  verification using Codepeer. This switch cannot be passed simultaneously with
  the ``--proof`` switch.

* ``--proof``
  
  Formally verify the model. This implies a slower but more complete verification.
  Cannot be passed together with ``--bug-finder`` switch.

* ``--version, -V``
  
  Output version and exit.

* ``--from-simulink``
  
  Display error messages as hyperlinks in the Simulink console.

* ``--help, -h``
  
  Display the list of supported switches.

* ``--matlab, -m FILE``
  
  Provide MATLAB file containing the definitions of variables used by the
  Simulink model.

* ``--wmisra``
  
  Treat violations to MISRA Simulink as warnings.

* ``--no-misra``
  
  Allow violations to MISRA Simulink.

* ``--subsys PATH``
  
  Provide the path to the subsystem to verify.

* ``--typing, -t FILE``
  
  Provide the decoration file.

* ``--lib, -b FILE``
  
  Specifies directories where library models can be found. The switch can be
  used multiple times to specify multiple directories.
  
  .. note:: The ``--lib`` switch is required only in case the relative location
   of the libraries is different than at the time of generating the decoration
   file.  The new location given with the ``--lib`` switch will override the
   original location which is stored in the decoration file.