.. SPARK 2014 User's Guide documentation master file, created by
   sphinx-quickstart on Mon Apr  4 14:49:11 2011.
   You can adapt this file completely to your liking, but it should at least
   contain the root `toctree` directive.

SPARK User's Guide
==================

.. Copyright notice for latex is in gfdl.tex. It is included specifically
   before the table of contents in LaTeX output (see conf.py), to avoid having
   it appear after the TOC in the generated PDF.

.. only:: html

   Copyright (C) 2011-2022, AdaCore and Capgemini Engineering

   Permission is granted to copy, distribute and/or modify this document
   under the terms of the GNU Free Documentation License, Version 1.1
   or any later version published by the Free Software Foundation;
   with no Invariant Sections, with no Front-Cover Texts, and with no
   Back-Cover Texts.
   A copy of the license is included in the section entitled 'GNU
   Free Documentation License'.

   .. only:: core_ja

      Translation to Japanese by Mr. Masao Ito (NIL)

.. only : : core

   .. toctree::
      :maxdepth: 3
      :numbered: 4

      en/getting_started
      en/introduction
      en/install
      en/spark_mode
      en/spark_2014
      en/gnatprove
      gfdl

.. only:: full

   .. toctree::
      :maxdepth: 3
      :numbered: 4

      en/getting_started
      en/introduction
      en/install
      en/spark_mode
      en/spark_2014
      en/tutorial
      en/gnatprove
      en/usage_scenarios

.. raw:: latex

   \appendix

.. toctree::
   :maxdepth: 3

   A. Command Line Invocation <en/appendix/command_line_invocation>
   B. Alternative Provers <en/appendix/alternative_provers>
   C. Project Attributes <en/appendix/project_attributes>
   D. Implementation Defined Pragmas <en/appendix/implementation_defined_pragmas>
   E. Additional Annotate Pragmas <en/appendix/additional_annotate_pragmas>
   F. Environment Variable <en/appendix/env_vars>
   G. GNATprove Limitations <en/appendix/gnatprove_limitations>
   H. Portability Issues <en/appendix/portability_issues>
   I. Semantics of Floating Point Operations <en/appendix/semantics_of_floating_point_operations>
   J. SPARK Architecture, Quality Assurance and Maturity <en/appendix/quality_assurance>
   K. GNU Free Documentation License <gfdl>