Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ with two technology supplements (Object-Oriented Technology and Formal
Methods).

.. index:: GNATcheck
.. index:: GNAT Static Analysis Suite (GNAT SAS)
.. index:: CodeSonar for Ada
.. index:: GNATcheck
.. index:: GNATstack
.. index:: GNAT Dynamic Analysis Suite (GNAT DAS)
Expand All @@ -74,9 +74,8 @@ toolchains, including support for Ada, C, C++, and Rust.
Complementary tools support several verification activities for Ada:

* GNATstack for stack checking (which also supports C),
* the GNAT Static Analysis Suite, or GNAT SAS, for defect and
vulnerability detection, code standard checking (GNATcheck), and
code metrics generation (GNATmetric)
* CodeSonar for Ada, providing defect and vulnerability detection, code
standard checking (GNATcheck), and code metrics generation (GNATmetric)
* the GNAT Dynamic Analysis Suite, or GNAT DAS, for testing (GNATtest,
TGen), structural code coverage analysis (GNATcoverage, which also
supports C and C++), processor emulation (GNATemulator), and fuzzing
Expand Down Expand Up @@ -1233,9 +1232,8 @@ possible activities:
requirements should define the expected behavior in case a pre- or
postcondition is violated, for example to reset the application to a
known safe state as soon as an inconsistency is detected.
* **Static analysis or formal proof**. The :ref:`GNAT Static Analysis
Suite technology<Airborn_SW_GNAT_Static_Analysis_Suite>`) takes
preconditions into account as part of its analysis in detecting
* **Static analysis or formal proof**. :ref:`Airborn_SW_CodeSonar_for_Ada`
takes preconditions into account as part of its analysis in detecting
potential errors. It can be tuned based on whether the priority is
on finding as many errors as possible, at the expense of false
positives, or on "picking the low-hanging fruit": detecting defects
Expand Down Expand Up @@ -1352,12 +1350,12 @@ justification would then appear in the tool's report.

.. index:: single: Use Case 1a: Traditional development process
excluding OOT; Checking source code accuracy and
consistency with GNAT SAS
consistency with CodeSonar for Ada

.. _Airborn_SW_Checking_source_code_accuracy_and_consistency_with_GNAT_SAS:
.. _Airborn_SW_Checking_source_code_accuracy_and_consistency_with_CodeSonar_for_Ada:

Checking source code accuracy and consistency with GNAT SAS
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Checking source code accuracy and consistency with CodeSonar for Ada
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

.. list-table::
:header-rows: 1
Expand All @@ -1376,8 +1374,7 @@ Checking source code accuracy and consistency with GNAT SAS
identifying a range of development errors that need to be
prevented. Satisfying this objective requires a combination of
reviews, analyses and tests, and tools may be used for some of these
activities. The :ref:`GNAT Static Analysis Suite (GNAT SAS)
<Airborn_SW_GNAT_Static_Analysis_Suite>` specifically targets issues
activities. :ref:`Airborn_SW_CodeSonar_for_Ada` specifically targets issues
that correspond to Ada exceptions, such as scalar overflow, range
constraint violations, and array indexing errors. It also detects
other errors including reads of uninitialized variables, useless
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -35,9 +35,9 @@ Mapping of AdaCore's Technologies to DO-178C/ED-12C Objectives
Programming Language, "SPARK (GNATprove)", "3, 5", "3, 4, 5, 6, 7", "FM 14, 15, 16, 17"
GNAT Pro Toolchain, GNAT Pro Assurance, 3, 7
GNAT Pro Toolchain, GNATstack, "3, 4", |blankcell|, |blankcell|
|gnatsas|, Defects & Vulnerability Analysis, "3, 4", |blankcell|, |blankcell|
|gnatsas|, GNATmetric, 3, |blankcell|, |blankcell|
|gnatsas|, GNATcheck, "3, 4, 5", |blankcell|, |blankcell|
|codesonar-for-ada|, Defects & Vulnerability Analysis, "3, 4", |blankcell|, |blankcell|
|codesonar-for-ada|, GNATmetric, 3, |blankcell|, |blankcell|
|codesonar-for-ada|, GNATcheck, "3, 4, 5", |blankcell|, |blankcell|
|gnatdas|, GNATtest, "3, 4", |blankcell|, |blankcell|
|gnatdas|, GNATemulator, 3, |blankcell|, |blankcell|
|gnatdas|, GNATcoverage, "3, 4", |blankcell|, |blankcell|
Expand All @@ -54,9 +54,9 @@ Mapping of AdaCore's Technologies to DO-178C/ED-12C Objectives
Programming Language, "SPARK (GNATprove)", "FM 10, 11, 12, 13", "3, 4", "FM 1-10"
GNAT Pro Toolchain, GNAT Pro Assurance, 7, |blankcell|, |blankcell|
GNAT Pro Toolchain, GNATstack, 6, |blankcell|, |blankcell|
|gnatsas|, Defects & Vulnerability Analysis, "3, 4, 6", |blankcell|, |blankcell|
|gnatsas|, GNATmetric, 4, |blankcell|, |blankcell|
|gnatsas|, GNATcheck, 4, |blankcell|, |blankcell|
|codesonar-for-ada|, Defects & Vulnerability Analysis, "3, 4, 6", |blankcell|, |blankcell|
|codesonar-for-ada|, GNATmetric, 4, |blankcell|, |blankcell|
|codesonar-for-ada|, GNATcheck, 4, |blankcell|, |blankcell|
|gnatdas|, GNATtest, |blankcell|, "3, 4", "1, 2"
|gnatdas|, GNATemulator, "3, 4", |blankcell|, |blankcell|
|gnatdas|, GNATcoverage, |blankcell|, |blankcell|, "5, 6, 7, 8"
Expand Down Expand Up @@ -177,7 +177,7 @@ Table A-5 Verification of Outputs of Software Requirement Process
3, "Source Code is verifiable.", 6.3.4, "See :ref:`Airborn_SW_Benefits_of_the_Ada_language`", "See :ref:`Airborn_SW_Benefits_of_the_Ada_language`", "See :ref:`Airborn_SW_Contributions_to_source_code_reviews`"
4, "Source Code conforms to standards.", 6.3.4, "See :ref:`Airborn_SW_Defining_and_Verifying_a_Code_Standard_with_GNATcheck`", |blankcell|
5, "Source Code is traceable to low-level requirements.", 6.3.4, "See :ref:`Airborn_SW_Using_Ada_during_the_design_process`", |blankcell|, "See :ref:`Airborn_SW_Contributions_to_source_code_reviews`"
6, "Source Code is accurate and consistent.", 6.3.4, "See :ref:`Airborn_SW_Benefits_of_the_Ada_language`, :ref:`Airborn_SW_Robustness_defensive_programming`, :ref:`Airborn_SW_Checking_worst-case_stack_consumption_with_GNATstack`, :ref:`Airborn_SW_Checking_source_code_accuracy_and_consistency_with_GNAT_SAS`", "See :ref:`Airborn_SW_Benefits_of_the_Ada_language`, :ref:`Airborn_SW_Robustness_defensive_programming`, :ref:`Airborn_SW_Checking_worst-case_stack_consumption_with_GNATstack`, :ref:`Airborn_SW_Checking_source_code_accuracy_and_consistency_with_GNAT_SAS`, :ref:`Airborn_SW_Overloading_and_type_conversion_vulnerabilities`, :ref:`Airborn_SW_Accounting_for_dispatching_in_performing_resource_ analysis`", "See :ref:`Airborn_SW_Checking_worst-case_stack_consumption_with_GNATstack`"
6, "Source Code is accurate and consistent.", 6.3.4, "See :ref:`Airborn_SW_Benefits_of_the_Ada_language`, :ref:`Airborn_SW_Robustness_defensive_programming`, :ref:`Airborn_SW_Checking_worst-case_stack_consumption_with_GNATstack`, :ref:`Airborn_SW_Checking_source_code_accuracy_and_consistency_with_CodeSonar_for_Ada`", "See :ref:`Airborn_SW_Benefits_of_the_Ada_language`, :ref:`Airborn_SW_Robustness_defensive_programming`, :ref:`Airborn_SW_Checking_worst-case_stack_consumption_with_GNATstack`, :ref:`Airborn_SW_Checking_source_code_accuracy_and_consistency_with_CodeSonar_for_Ada`, :ref:`Airborn_SW_Overloading_and_type_conversion_vulnerabilities`, :ref:`Airborn_SW_Accounting_for_dispatching_in_performing_resource_ analysis`", "See :ref:`Airborn_SW_Checking_worst-case_stack_consumption_with_GNATstack`"
7, "Output of software integration process is complete and correct.", 6.3.5, "See :ref:`Airborn_SW_Compiling_with_the_GNAT_Pro_compiler`", "Same as #1a", "Same as #1a"
8, "Parameter Data Item File is complete and correct.", 6.6, "See :ref:`Airborn_SW_Parameter_Data_Items`", "Same as #1a", "Same as #1a"
9, "Verification of Parameter Data Item File is achieved.", 6.6, "See :ref:`Airborn_SW_Parameter_Data_Items`", "Same as #1a", "Same as #1a"
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -719,35 +719,35 @@ unbounded frames.

TQL-5 qualification material can be made available for GNATstack.

.. index:: GNAT Static Analysis Suite (GNAT SAS)
.. index:: CodeSonar for Ada

.. _Airborn_SW_GNAT_Static_Analysis_Suite:
.. _Airborn_SW_CodeSonar_for_Ada:

GNAT Static Analysis Suite (GNAT SAS)
-------------------------------------
CodeSonar for Ada
-----------------

GNAT SAS is a stand-alone tool that runs on Windows and Linux
CodeSonar for Ada is a static analysis toolset that runs on Windows and Linux
platforms and may be used with any standard Ada compiler or fully
integrated into the GNAT Pro development environment.

.. index:: Defects and vulnerability analysis (in GNAT SAS)
.. index:: single: GNAT Static Analysis Suite (GNAT SAS); Defects and
.. index:: Defects and vulnerability analysis (in CodeSonar for Ada)
.. index:: single: CodeSonar for Ada; Defects and
vulnerability analysis

Defects and vulnerability analysis
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

GNAT SAS features an Ada source code analyzer that detects run-time
CodeSonar for Ada features an Ada source code analyzer that detects run-time
and logic errors. It assesses potential bugs and vulnerabilities
before program execution, serving as an automated peer reviewer,
helping to find errors easily at any stage of the development
life-cycle. It helps improve code quality and makes it easier to
perform safety and/or security analysis. GNAT SAS can detect several
perform safety and/or security analysis. CodeSonar for Ada can detect several
of the "Top 25 Most Dangerous Software Errors" in the Common Weakness
Enumeration.

.. index:: GNATmetric
.. index:: single: GNAT Static Analysis Suite (GNAT SAS); GNATmetric
.. index:: single: CodeSonar for Ada; GNATmetric

GNATmetric
~~~~~~~~~~
Expand All @@ -759,7 +759,7 @@ information also facilitates satisfying the requirements of certain
software development frameworks.

.. index:: GNATcheck
.. index:: single: GNAT Static Analysis Suite (GNAT SAS); GNATcheck
.. index:: single: CodeSonar for Ada; GNATcheck

.. _Airborn_SW_GNATcheck:

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -131,14 +131,14 @@ document.

.. rubric:: Foreword to V2.1

This revised booklet reflects the evolution of and enhancements to
AdaCore's products since the earlier edition. Among other updates,
the static analysis tools supplementing the GNAT Pro development
environment have been integrated into a cohesive toolset (the *GNAT
Static Analysis Suite*). The dynamic analysis tools have likewise
been consolidated, and the resulting *GNAT Dynamic Analysis Suite* has
introduced a fuzzing tool |mdash| *GNATfuzz* |mdash| which exercises
the software with invalid input and checks for failsafe behavior.
This revised booklet reflects the evolution of and enhancements to AdaCore's
products since the earlier edition. Among other updates, the static
analysis tools supplementing the GNAT Pro development environment have been
integrated into a cohesive toolset (*CodeSonar for Ada*). The dynamic
analysis tools have likewise been consolidated, and the resulting *GNAT
Dynamic Analysis Suite* has introduced a fuzzing tool |mdash| *GNATfuzz*
|mdash| which exercises the software with invalid input and checks for
failsafe behavior.

I would like to express my appreciation to Olivier Appere (AdaCore)
for his detailed and helpful review of the content for the revised
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -139,10 +139,10 @@ implementation of the following techniques:
* D.38 Modular Approach
* D.57 Object Oriented Programming

GNAT Static Analysis Suite
--------------------------
CodeSonar for Ada
-----------------

See :ref:`Railway_SW_GNAT_Static_Analysis_Suite`.
See :ref:`Railway_SW_CodeSonar_for_Ada`.

Defects and Vulnerability Analysis
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Expand All @@ -154,8 +154,8 @@ Defects and Vulnerability Analysis
Qualification
^^^^^^^^^^^^^

GNAT SAS's defects and vulnerability analysis tool can be qualified at
class T2.
The defects and vulnerability analysis tool in CodeSonar for Ada can be
qualified at class T2.
It has a long cross-industry track record and has been qualified under other
standards in the past, such as DO-178B/C as a verification tool/TQL5.

Expand All @@ -164,8 +164,8 @@ standards in the past, such as DO-178B/C as a verification tool/TQL5.
Annex D References
^^^^^^^^^^^^^^^^^^

GNAT SAS's defects and vulnerability analysis tool can contribute to the
deployment or implementation of the following techniques:
The defects and vulnerability analysis tool in CodeSonar for Ada can
contribute to the deployment or implementation of the following techniques:

* D.2 Analyzable Programs
* D.4 Boundary Value Analysis
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -273,8 +273,8 @@ The entries in Tables A.4 and A.15 show that Ada is a Highly Recommended
language at |sil1| through |sil4| and a Recommended language at the
Basic Integrity level.
Features that should be avoided can be detected and prevented by using
AdaCore's GNATcheck tool in the GNAT Static Analysis Suite;
see :ref:`Railway_SW_GNAT_Static_Analysis_Suite`.
AdaCore's GNATcheck tool in CodeSonar for Ada;
see :ref:`Railway_SW_CodeSonar_for_Ada`.

.. index:: single: EN 50128; Annex B (Key software roles and responsibilities)

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -184,14 +184,14 @@ The following technologies will be presented:
language development environments that is oriented towards projects with
long maintenance cycles or certification requirements

.. index:: GNAT Static Analysis Suite (GNAT SAS)
.. index:: single: GNAT Static Analysis Suite (GNAT SAS); Defects and vulnerability analysis
.. index:: CodeSonar for Ada
.. index:: single: CodeSonar for Ada; Defects and vulnerability analysis
.. index:: GNATmetric
.. index:: single: GNAT Static Analysis Suite (GNAT SAS); GNATmetric
.. index:: single: CodeSonar for Ada; GNATmetric
.. index:: GNATcheck
.. index:: single: GNAT Static Analysis Suite (GNAT SAS); GNATcheck
.. index:: single: CodeSonar for Ada; GNATcheck

* The *GNAT Static Analysis Suite* ("GNAT SAS"), comprising several tools:
* *CodeSonar for Ada*, comprising several tools:

- A "bug finder" engine that identifies potential defects and
vulnerabilities in Ada code
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ component or a programming activity than an architecture activity per se, \
but as it is recorded in this table, it's worth mentioning that the Ada \
language provides several features addressing various objectives of \
defensive programming techniques (e.g., exception handling). In addition, \
the GNAT Static Analysis Suite and SPARK tools help identify pieces of code \
CodeSonar for Ada and the SPARK tools help identify pieces of code \
that should be protected by defensive code."
Fault Detection & Diagnosis,D.26,R,R,No,
Error Correcting Codes,D.19,|mdash|,|mdash|,No,
Expand Down
Original file line number Diff line number Diff line change
@@ -1,22 +1,22 @@
Technique/Measure,Ref,SIL 2,SIL 3/4,Covered,Comment
Boundary Value Analysis,D.4,R,HR,Yes,"GNAT SAS can compute boundary values \
for variables and parameters from the source code. GNAT SAS and SPARK can \
Boundary Value Analysis,D.4,R,HR,Yes,"CodeSonar for Ada can compute boundary values \
for variables and parameters from the source code. CodeSonar for Ada and SPARK can \
verify various properties by analyzing potential values and boundary values \
of variables. This includes detecting errors such as dereferencing a pointer \
that could be null, generating a value outside the bounds of an Ada type or \
subtype, violating a memory safety constraint (`buffer overrun`), \
generating a numeric overflow or wraparound, and dividing by zero. \
GNAT SAS and SPARK also help to confirm expected boundary values of \
CodeSonar for Ada and SPARK also help to confirm expected boundary values of \
variables and parameters coming from the design."
Checklists,D.7,R,R,No,
Control Flow Analysis,D.8,HR,HR,Yes,"GNAT SAS and SPARK can detect \
Control Flow Analysis,D.8,HR,HR,Yes,"CodeSonar for Ada and SPARK can detect \
suspicious and potentially incorrect control flows, such as unreachable \
code, redundant conditionals, loops that either run forever or fail to \
terminate normally, and subprograms that never return. GNATstack can analyze \
control flow and compute the maximum amount of stack memory for each task. \
More generally, GNAT Studio provides visualization for call graphs and \
call trees."
Data Flow Analysis,D.10,HR,HR,Yes,"GNAT SAS and SPARK can detect suspicious \
Data Flow Analysis,D.10,HR,HR,Yes,"CodeSonar for Ada and SPARK can detect suspicious \
and potentially incorrect data flow, such as variables being read before \
they are written (uninitialized variables), and values that are written to \
variables without being read (redundant assignments)."
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ rules."
features to improve program analysis, such as type ranges, parameter modes, \
and encapsulation. Tools such as GNATmetric and GNATcheck can help monitor \
the complexity of the code and prevent the use of overly complex code. \
GNAT SAS allows making an assessment of program analyzability during its \
CodeSonar for Ada allows making an assessment of program analyzability during its \
development. For higher SILs, the use of SPARK ensures that the subset \
of the language used is suitable for most the rigorous analysis."
Strongly Typed Programming Language,D.49,HR,HR,Yes,"Ada is a strongly typed \
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ code size, comment percentage, cyclomatic complexity, unit nesting, and \
loop nesting. These can then be compared with standards."
Traceability,D.58,HR,M,No,
Software Error Effect Analysis,D.25,R,HR,Yes,"GNAT Studio supports code \
display and navigation. GNAT SAS can identify likely error locations in the \
display and navigation. CodeSonar for Ada can identify likely error locations in the \
code. This supports potential software error detection and analysis \
throughout the code."
Test Coverage for code,Table A.21,HR,HR,Yes,See Table A.21
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,6 @@ A.14."
Cause Consequence Diagrams,D.6,R,R,No,
Event Tree Analysis,D.22,R,R,No,
Software Error Effect Analysis,D.25,R,HR,Yes,"GNAT Studio supports code \
display and navigation. GNAT SAS can identify likely error locations in the \
display and navigation. CodeSonar for Ada can identify likely error locations in the \
code. These tools support both detection of potential software errors and \
analysis throughout the code."
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
Technique/Measure,Ref,SIL 2,SIL 3/4,Covered,Comment
Impact Analysis,D.32,HR,M,Yes,"GNAT SAS contributes to identifying the \
Impact Analysis,D.32,HR,M,Yes,"CodeSonar for Ada contributes to identifying the \
impact of a code change between two baselines."
Data Recording and Analysis,D.12,HR,M,Yes,"AdaCore tools can be invoked \
from the command line. They produce result files including the date and \
Expand Down
Loading
Loading