From 2a8c01f0ea0381f9f80cf1e3f1f8ac2d5216e742 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Mon, 6 Apr 2020 11:41:56 -0500 Subject: [PATCH] Link all post-analyses in JSON/XML output section --- doc/usr/source/3_output/2_machine_readable.rst | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/doc/usr/source/3_output/2_machine_readable.rst b/doc/usr/source/3_output/2_machine_readable.rst index 8d228cbc1..866363061 100644 --- a/doc/usr/source/3_output/2_machine_readable.rst +++ b/doc/usr/source/3_output/2_machine_readable.rst @@ -137,7 +137,7 @@ The list of properties of an ``AnalysisStart`` object are: ``scope``, ``string``, "Name of the component where the property was analyzed." ``line``, ``integer``, "Associated line in the input file, if any." ``column``, ``integer``, "Associated column in the input file, if any." - ``source``, ``string``, "Origin of the property. Can be ``Assumption`` if it comes from an assumption check, ``Guarantee`` if it comes from the check of a guarantee, ``Ensure`` if it comes from a check of an ensure clause in a contract mode, ``OneModeActive`` if it comes from an exhaustiveness check of the state space covered by the modes of a contract, and ``PropAnnot`` if it comes from the check of a property annotation." + ``source``, ``string``, "Origin of the property. Can be ``Assumption`` if it comes from an assumption check, ``Guarantee`` if it comes from the check of a guarantee, ``Ensure`` if it comes from a check of a require-ensure clause in a contract mode, ``OneModeActive`` if it comes from an exhaustiveness check of the state space covered by the modes of a contract, and ``PropAnnot`` if it comes from the check of a property annotation." ``runtime``, ``object``, "The runtime of the analysis (in seconds), and whether the timeout expired" ``k``, ``integer``, "The value of ``k`` in a k-inductive proof, if any." ``trueFor``, ``integer``, "The largest value of ``k`` for which the property was proved to be true, if any." @@ -191,8 +191,12 @@ The list of properties of an ``PostAnalysisStart`` object are: ``name``, ``string``, "Name of the post-analysis" -The post-analyses currently available are ``testgen``, ``contractgen``, -``rustgen``, ``invlog``, ``invprint``, and ``certification``. +The post-analyses currently available are :ref:`9_other/3_test_generation` (``testgen``), +:ref:`9_other/5_proofs` (``certification``), +:ref:`9_other/6_contract_generation` (``contractgen``), +:ref:`9_other/4_rust_compilation` (``rustgen``), +:ref:`9_other/7_invariant_logging` (``invlog``), and +:ref:`9_other/9_invariant_printing` (``invprint``). .. _PostAnalysisEnd Object: @@ -355,8 +359,12 @@ PostAnalysisStart Element An ``PostAnalysisStart`` element is an empty element that indicates the beginning of a post-analysis. It has only one attribute of type ``xs:string``, the ``name`` of the post-analysis. -The post-analyses currently available are ``testgen``, ``contractgen``, -``rustgen``, ``invlog``, ``invprint``, and ``certification``. +The post-analyses currently available are :ref:`9_other/3_test_generation` (``testgen``), +:ref:`9_other/5_proofs` (``certification``), +:ref:`9_other/6_contract_generation` (``contractgen``), +:ref:`9_other/4_rust_compilation` (``rustgen``), +:ref:`9_other/7_invariant_logging` (``invlog``), and +:ref:`9_other/9_invariant_printing` (``invprint``). .. _PostAnalysisEnd Element: