diff --git a/content/booklets/adacore-technologies-for-airborne-software/chapters/analysis.rst b/content/booklets/adacore-technologies-for-airborne-software/chapters/analysis.rst index 4b18cedd0..23e798157 100644 --- a/content/booklets/adacore-technologies-for-airborne-software/chapters/analysis.rst +++ b/content/booklets/adacore-technologies-for-airborne-software/chapters/analysis.rst @@ -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) @@ -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 @@ -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`) 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 @@ -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 @@ -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) -` 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 diff --git a/content/booklets/adacore-technologies-for-airborne-software/chapters/summary.rst b/content/booklets/adacore-technologies-for-airborne-software/chapters/summary.rst index b3e2c50d5..c26fbb2bd 100644 --- a/content/booklets/adacore-technologies-for-airborne-software/chapters/summary.rst +++ b/content/booklets/adacore-technologies-for-airborne-software/chapters/summary.rst @@ -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| @@ -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" @@ -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" diff --git a/content/booklets/adacore-technologies-for-airborne-software/chapters/tools.rst b/content/booklets/adacore-technologies-for-airborne-software/chapters/tools.rst index 6f163b9c5..169273bc4 100644 --- a/content/booklets/adacore-technologies-for-airborne-software/chapters/tools.rst +++ b/content/booklets/adacore-technologies-for-airborne-software/chapters/tools.rst @@ -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 ~~~~~~~~~~ @@ -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: diff --git a/content/booklets/adacore-technologies-for-airborne-software/index.rst b/content/booklets/adacore-technologies-for-airborne-software/index.rst index 45a55e712..2c7d5264f 100644 --- a/content/booklets/adacore-technologies-for-airborne-software/index.rst +++ b/content/booklets/adacore-technologies-for-airborne-software/index.rst @@ -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 diff --git a/content/booklets/adacore-technologies-for-railway-software/chapters/annex.rst b/content/booklets/adacore-technologies-for-railway-software/chapters/annex.rst index 62d80742f..b18918de3 100644 --- a/content/booklets/adacore-technologies-for-railway-software/chapters/annex.rst +++ b/content/booklets/adacore-technologies-for-railway-software/chapters/annex.rst @@ -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 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -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. @@ -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 diff --git a/content/booklets/adacore-technologies-for-railway-software/chapters/cenelec.rst b/content/booklets/adacore-technologies-for-railway-software/chapters/cenelec.rst index e6db067b7..a01a12ae1 100644 --- a/content/booklets/adacore-technologies-for-railway-software/chapters/cenelec.rst +++ b/content/booklets/adacore-technologies-for-railway-software/chapters/cenelec.rst @@ -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) diff --git a/content/booklets/adacore-technologies-for-railway-software/chapters/introduction.rst b/content/booklets/adacore-technologies-for-railway-software/chapters/introduction.rst index 4dc97f6fd..9ace09f83 100644 --- a/content/booklets/adacore-technologies-for-railway-software/chapters/introduction.rst +++ b/content/booklets/adacore-technologies-for-railway-software/chapters/introduction.rst @@ -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 diff --git a/content/booklets/adacore-technologies-for-railway-software/chapters/table4-1.csv b/content/booklets/adacore-technologies-for-railway-software/chapters/table4-1.csv index f291e7f16..b0a20b37e 100644 --- a/content/booklets/adacore-technologies-for-railway-software/chapters/table4-1.csv +++ b/content/booklets/adacore-technologies-for-railway-software/chapters/table4-1.csv @@ -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, diff --git a/content/booklets/adacore-technologies-for-railway-software/chapters/table4-16.csv b/content/booklets/adacore-technologies-for-railway-software/chapters/table4-16.csv index 247135c4e..00a2e1b0d 100644 --- a/content/booklets/adacore-technologies-for-railway-software/chapters/table4-16.csv +++ b/content/booklets/adacore-technologies-for-railway-software/chapters/table4-16.csv @@ -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)." diff --git a/content/booklets/adacore-technologies-for-railway-software/chapters/table4-2.csv b/content/booklets/adacore-technologies-for-railway-software/chapters/table4-2.csv index 8829416f7..0598a6f49 100644 --- a/content/booklets/adacore-technologies-for-railway-software/chapters/table4-2.csv +++ b/content/booklets/adacore-technologies-for-railway-software/chapters/table4-2.csv @@ -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 \ diff --git a/content/booklets/adacore-technologies-for-railway-software/chapters/table4-3.csv b/content/booklets/adacore-technologies-for-railway-software/chapters/table4-3.csv index dfcb202b0..9c43b8ed4 100644 --- a/content/booklets/adacore-technologies-for-railway-software/chapters/table4-3.csv +++ b/content/booklets/adacore-technologies-for-railway-software/chapters/table4-3.csv @@ -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 diff --git a/content/booklets/adacore-technologies-for-railway-software/chapters/table4-6.csv b/content/booklets/adacore-technologies-for-railway-software/chapters/table4-6.csv index f86092f5a..d187cd333 100644 --- a/content/booklets/adacore-technologies-for-railway-software/chapters/table4-6.csv +++ b/content/booklets/adacore-technologies-for-railway-software/chapters/table4-6.csv @@ -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." \ No newline at end of file diff --git a/content/booklets/adacore-technologies-for-railway-software/chapters/table4-8.csv b/content/booklets/adacore-technologies-for-railway-software/chapters/table4-8.csv index db53f173a..a84a03686 100644 --- a/content/booklets/adacore-technologies-for-railway-software/chapters/table4-8.csv +++ b/content/booklets/adacore-technologies-for-railway-software/chapters/table4-8.csv @@ -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 \ diff --git a/content/booklets/adacore-technologies-for-railway-software/chapters/technology.rst b/content/booklets/adacore-technologies-for-railway-software/chapters/technology.rst index 70a9c1a48..14131cfef 100644 --- a/content/booklets/adacore-technologies-for-railway-software/chapters/technology.rst +++ b/content/booklets/adacore-technologies-for-railway-software/chapters/technology.rst @@ -37,13 +37,14 @@ and quality of the code and identifying potentially problematic constructs. This is accomplished through techniques such as basic code size metrics, cyclomatic complexity computation, and coupling analysis. -.. index:: single: GNAT Static Analysis Suite (GNAT SAS); Support for Analyzable Programs (D.2) +.. index:: single: CodeSonar for Ada; Support for Analyzable Programs (D.2) -GNAT SAS identifies potential run-time errors in the code. The number of -false positive results depends on the code complexity. A high number of -false positives is often a symptom of overly-complicated code. Using GNAT SAS -during development allows finding locations in the code that are -overly complex and provides information on what needs to be improved. +CodeSonar for Ada identifies potential run-time errors in the code. The +number of false positive results depends on the code complexity. A high +number of false positives is often a symptom of overly-complicated code. +Using CodeSonar for Ada during development allows finding locations in the +code that are overly complex and provides information on what needs to be +improved. .. index:: single: SPARK technology; Support for Analyzable Programs (D.2) @@ -103,25 +104,26 @@ assertions) or formally proven with SPARK. Further discussion of input partitioning can be found in the context of :ref:`Railway_SW_Equivalence_Classes_and_Input_Partition_Testing`. -.. index:: single: GNAT Static Analysis Suite (GNAT SAS); Support for Boundary Value Analysis (D.4) +.. index:: single: CodeSonar for Ada; Support for Boundary Value Analysis (D.4) -Another possibility is to use GNAT SAS to identify possible values for -variables, and propagate those values from call to call, constructing -lists and/or ranges of potential values for each variable at each point -of the program. These are used as the input to run-time error analysis. -When used in full-soundness mode, GNAT SAS provides guarantees that the +Another possibility is to use CodeSonar for Ada to identify possible values +for variables, and propagate those values from call to call, constructing +lists and/or ranges of potential values for each variable at each point of +the program. These are used as the input to run-time error analysis. When +used in full-soundness mode, CodeSonar for Ada provides guarantees that the locations it reports on the code are the only ones that may have run-time -errors, thus allowing a reduction of the scope of testing and review to -only these places. +errors, thus allowing a reduction of the scope of testing and review to only +these places. -However, it's important to stress that GNAT SAS is only performing this -boundary value analysis with respect to potential exceptions and robustness. -No information is provided regarding the correctness of the values -produced by subprograms. +However, it's important to stress that CodeSonar for Ada is only performing +this boundary value analysis with respect to potential exceptions and +robustness. No information is provided regarding the correctness of the +values produced by subprograms. -GNAT SAS also has the capacity to display the possible values of variables -and parameters. This can be used as a mechanism to increase confidence -that testing has taken into account all possible boundaries for values. +CodeSonar for Ada also has the capacity to display the possible values of +variables and parameters. This can be used as a mechanism to increase +confidence that testing has taken into account all possible boundaries for +values. .. index:: single: SPARK technology; Support for Boundary Value Analysis (D.4) .. index:: Absence of Run-Time Errors (AORTE) @@ -146,13 +148,13 @@ that are always true). GNAT Studio can display call graphs between subprograms, allowing visualization and analysis of control flow in the application. -.. index:: single: GNAT Static Analysis Suite (GNAT SAS); Support for Control Flow Analysis (D.8) +.. index:: single: CodeSonar for Ada; Support for Control Flow Analysis (D.8) -GNAT SAS contributes to control flow analysis by identifying unreachable code, -as well as conditions being always true or always false. This analysis is -partial and needs to be completed with other techniques such as code review or -code coverage analysis, which together will allow reaching higher levels of -confidence. +CodeSonar for Ada contributes to control flow analysis by identifying +unreachable code, as well as conditions being always true or always false. +This analysis is partial and needs to be completed with other techniques +such as code review or code coverage analysis, which together will allow +reaching higher levels of confidence. .. index:: single: GNATmetric; Support for Control Flow Analysis (D.8) @@ -179,9 +181,9 @@ out-of-range value (if there is one) or to an *unusual* value (either the largest or smallest). This significantly improves detection at test time. -.. index:: single: GNAT Static Analysis Suite (GNAT SAS); Support for Data Flow Analysis (D.10) +.. index:: single: CodeSonar for Ada; Support for Data Flow Analysis (D.10) -GNAT SAS can detect suspicious and potentially incorrect data +CodeSonar for Ada can detect suspicious and potentially incorrect data flows, such as variables that are read before they are written (uninitialized variables), variables written more than once without being read (redundant assignments), and variables that are written but never read. @@ -284,8 +286,8 @@ an element of an array. In this case, Ada allows expressing constraints in the specification, through preconditions, postconditions or predicates. Beyond this, Ada provides specific support for a subset of what's specified -in the D.14 annex. GNAT SAS and SPARK will allow the development of defensive -programming in places where it makes the most sense. +in the D.14 annex. CodeSonar for Ada and SPARK will allow the development of +defensive programming in places where it makes the most sense. .. index:: single: GNATcheck; Support for Defensive Programming (D.14) @@ -327,11 +329,11 @@ ensure that the expression is within its boundary: ... -- Respond to out-of-range result end if; -.. index:: single: GNAT Static Analysis Suite (GNAT SAS); Support for Defensive Programming (D.14) +.. index:: single: CodeSonar for Ada; Support for Defensive Programming (D.14) .. index:: single: SPARK technology; Support for Defensive Programming (D.14) Another way to proactively ensure the absence of range check failure is -to use tools such as GNAT SAS or SPARK, which statically identify the +to use tools such as CodeSonar for Ada or SPARK, which statically identify the only possible locations in the code where such failures can happen. Note that run-time checks can be deactivated if needed for performance @@ -418,15 +420,15 @@ as an :ada:`out` or :ada:`in out` parameter would be illegal. Note that :ada:`Greeting` is a variable and can be assigned to, but the literal :ada:`"Hello"` is immutable. -.. index:: single: GNAT Static Analysis Suite (GNAT SAS); Support for Defensive Programming (D.14) +.. index:: single: CodeSonar for Ada; Support for Defensive Programming (D.14) .. index:: single: SPARK technology; Support for Defensive Programming (D.14) -Using GNAT SAS and SPARK to drive defensive programming -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Using CodeSonar for Ada and SPARK to drive defensive programming +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -GNAT SAS and SPARK identify locations where there are potential run-time -errors |mdash| in other words, places where code is either wrong or where -defensive programming should be deployed. This helps guide the writing +CodeSonar for Ada and SPARK identify locations where there are potential +run-time errors |mdash| in other words, places where code is either wrong or +where defensive programming should be deployed. This helps guide the writing of defensive code. For example: .. code-block:: ada @@ -439,10 +441,10 @@ of defensive code. For example: ... end P; -In the above code, there's a use of :ada:`V` as an index into the -String :ada:`S`. -GNAT SAS and SPARK will detect the potential for a run-time error. Protection -of the code to prevent the error can take several forms: +In the above code, there's a use of :ada:`V` as an index into the String +:ada:`S`. CodeSonar for Ada and SPARK will detect the potential for a +run-time error. Protection of the code to prevent the error can take several +forms: .. rubric:: Explicit test @@ -481,11 +483,11 @@ is raised. ... end P; -The main difference between GNAT SAS and SPARK is that GNAT SAS may miss some -potential run-time errors (except when run only on small pieces of code if -configured in "sound" mode), while SPARK requires the use of the appropriate -Ada subset but is a sound technology (i.e., it will detect all potential -run-time errors). +The main difference between CodeSonar for Ada and SPARK is that +CodeSonar for Ada may miss some potential run-time errors (except when run +only on small pieces of code if configured in "sound" mode), while SPARK +requires the use of the appropriate Ada subset but is a sound technology +(i.e., it will detect all potential run-time errors). In general, the recommended Ada style is to use contracts instead of defensive code. @@ -604,7 +606,7 @@ software. .. index:: single: SPARK technology; Support for Failure Assertion Programming (D.24) The contracts can be used by the static analysis and formal proof tools. -GNAT SAS uses contracts to refine its analysis and exploits them as +CodeSonar for Ada uses contracts to refine its analysis and exploits them as assertions, even if it may not be able to demonstrate that they are correct. In this manner, contracts provide the tool with additional information on the code behavior. SPARK can go further and either prove their @@ -674,7 +676,7 @@ the correctness of these properties can then be simplified, if not entirely removed. .. index:: single: Annex D; Impact Analysis (D.32) -.. index:: single: GNAT Static Analysis Suite (GNAT SAS); Support for Impact Analysis (D.32) +.. index:: single: CodeSonar for Ada; Support for Impact Analysis (D.32) Impact Analysis (D.32) @@ -682,10 +684,11 @@ Impact Analysis (D.32) Identifying the effect of a change on an entire software component requires the combination of various techniques, including reviews, testing and static -analysis. GNAT SAS has specific features to identify the impact of a change -from the perspective of potential run-time errors. It can establish a baseline -with regard to potential failure analysis and filter only the potential -defects that have been introduced or repaired following a change in the code. +analysis. CodeSonar for Ada has specific features to identify the impact of +a change from the perspective of potential run-time errors. It can establish +a baseline with regard to potential failure analysis and filter only the +potential defects that have been introduced or repaired following a change +in the code. .. index:: single: GNAT Studio IDE; Support for Impact Analysis (D.32) diff --git a/content/booklets/adacore-technologies-for-railway-software/chapters/tools.rst b/content/booklets/adacore-technologies-for-railway-software/chapters/tools.rst index e9ea7c85f..76ec0cafc 100644 --- a/content/booklets/adacore-technologies-for-railway-software/chapters/tools.rst +++ b/content/booklets/adacore-technologies-for-railway-software/chapters/tools.rst @@ -745,25 +745,24 @@ such as the potential targets for indirect calls, the stack requirements for external calls, and the maximal size for unbounded frames. -.. index:: GNAT Static Analysis Suite (GNAT SAS) +.. index:: CodeSonar for Ada -.. _Railway_SW_GNAT_Static_Analysis_Suite: +.. _Railway_SW_CodeSonar_for_Ada: -GNAT Static Analysis Suite (GNAT SAS) -------------------------------------- +CodeSonar for Ada +----------------- -.. index:: Defects and vulnerability analysis (in GNAT SAS) -.. index:: single: GNAT Static Analysis Suite (GNAT SAS); Defects and vulnerability analysis +.. index:: Defects and vulnerability analysis (in CodeSonar for Ada) +.. index:: single: CodeSonar for Ada; Defects and vulnerability analysis Defects and Vulnerability Analyzer ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -GNAT SAS 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. +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. The defects and vulnerability analyzer can detect several of the "Top 25 Most Dangerous Software Errors" in the Common Weakness Enumeration. @@ -773,7 +772,7 @@ GNAT Pro development environment. .. index:: GNATmetric -.. index:: single: GNAT Static Analysis Suite (GNAT SAS); GNATmetric +.. index:: single: CodeSonar for Ada; GNATmetric GNATmetric ~~~~~~~~~~ @@ -785,7 +784,7 @@ 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 .. _Railway_SW_GNATcheck: diff --git a/content/booklets/adacore-technologies-for-railway-software/index.rst b/content/booklets/adacore-technologies-for-railway-software/index.rst index f7a541c6e..a1f2d9d8d 100644 --- a/content/booklets/adacore-technologies-for-railway-software/index.rst +++ b/content/booklets/adacore-technologies-for-railway-software/index.rst @@ -124,7 +124,7 @@ assurance in mission-critical real-time software. This revised edition reflects the current (2025) versions of |en-50128| and AdaCore's offerings. Among other updates and enhancements to the company's products, the static analysis tools supplementing the |gnatpro| development environment have been -integrated into a cohesive toolset (the *GNAT Static Analysis Suite*). +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 diff --git a/content/booklets/adacore-technologies-for-space-systems-software/chapters/compliance-e40c.rst b/content/booklets/adacore-technologies-for-space-systems-software/chapters/compliance-e40c.rst index 4c50806a9..6c47f618f 100644 --- a/content/booklets/adacore-technologies-for-space-systems-software/chapters/compliance-e40c.rst +++ b/content/booklets/adacore-technologies-for-space-systems-software/chapters/compliance-e40c.rst @@ -204,7 +204,7 @@ Detailed design of real-time software {§5.5.2.5} cannot change between the time that a task evaluates the state condition and when it executes the code based on that state. Other race conditions can be detected by the Defects and Vulnerability - Analyzer in the GNAT Static Analysis Suite. + Analyzer in CodeSonar for Ada. * "The supplier shall document and justify the use of dynamic allocation of resources." {§5.5.2.5d} @@ -226,9 +226,8 @@ Detailed design of real-time software {§5.5.2.5} pragma :ada:`Restrictions` produces a run-time check that detects attempts to perform allocations from a standard storage pool after elaboration (initialization). Depending on the program structure, - static analysis by the GNAT Static Analysis Suite's Defects and - Vulnerability Analyzer may be able to determine that this check - will never fail. + static analysis by the Defects and Vulnerability Analyzer in CodeSonar + for Ada may be able to determine that this check will never fail. Utilization of description techniques for the software behaviour {§5.5.2.6} ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ @@ -329,7 +328,7 @@ Development and documentation of a software validation specification with respec * The Defects and Vulnerability Analyzer (see :ref:`Space_Systems_SW_Defects_and_Vulnerability_Analyzer`) in - the GNAT Static Analysis Suite and/or SPARK Pro may be able to + CodeSonar for Ada and/or SPARK Pro may be able to show that a run-time check will always succeed and that no test case will trigger a failure. @@ -360,7 +359,7 @@ Development and documentation of a software validation specification with respec * The Defects and Vulnerability Analyzer (see :ref:`Space_Systems_SW_Defects_and_Vulnerability_Analyzer`) in - the GNAT Static Analysis Suite and/or SPARK Pro may be able to + CodeSonar for Ada and/or SPARK Pro may be able to show that a run-time check will always succeed and that no test case will trigger a failure. @@ -429,19 +428,19 @@ Verification of code {§5.8.3.5} help meet criterion 2. * For criterion 3, the Defects and Vulnerability Analyzer (see :ref:`Space_Systems_SW_Defects_and_Vulnerability_Analyzer`) in - the GNAT Static Analysis Suite and/or SPARK Pro can help verify - correctness, and the GNATcheck utility included in the GNAT - Static Analysis Suite (see :ref:`Space_Systems_SW_GNATcheck`) - can enforce conformance with a coding standard. + CodeSonar for Ada and/or SPARK Pro can help verify + correctness, and the GNATcheck utility included in CodeSonar for Ada + (see :ref:`Space_Systems_SW_GNATcheck`) can enforce conformance with a + coding standard. * For criterion 5, Ada's strong typing and interface checks, as well as SPARK and GNATprove, can help show consistent interfaces and correct data flow. * The Defects and Vulnerability Analyzer (see :ref:`Space_Systems_SW_Defects_and_Vulnerability_Analyzer`) in - the GNAT Static Analysis Suite, SPARK Pro, and the standard + CodeSonar for Ada, SPARK Pro, and the standard semantic checks performed by the GNAT Pro compiler can help meet criterion 6. - * The GNAT Static Analysis Suite and SPARK / GNATprove can statically + * CodeSonar for Ada and SPARK / GNATprove can statically detect potential run-time errors and thereby help meet criterion 7. * Ada's exception handling facility can help meet criterion 8. @@ -509,7 +508,7 @@ Verification of code {§5.8.3.5} * The Defects and Vulnerability Analyzer (see :ref:`Space_Systems_SW_Defects_and_Vulnerability_Analyzer`) in - the GNAT Static Analysis Suite will detect such errors as well as + CodeSonar for Ada will detect such errors as well as many others, including suspicious constructs that, although legitimate Ada, are likely logic errors. @@ -641,8 +640,9 @@ Invoking of software engineering processes for modification implementation {§5. GNAT Pro for Ada and SPARK Pro, the developer can localize the impact of maintenance changes. - * The GNAT Static and Dynamic Analysis Suites can ensure that any modifications - meet the verification criteria applicable to the original software. + * CodeSonar for Ada and the GNAT Dynamic Analysis Suite can ensure that + any modifications meet the verification criteria applicable to the + original software. .. index:: single: ECSS-E-ST-40C compliance; §5.11 Software security process @@ -655,8 +655,8 @@ Process implementation {|sect| 5.11.2} * "A software security management plan shall be produced documenting: ... 7. the tools, methods and procedures to be used...." {|sect| 5.11.2a} - * The Ada and SPARK languages, GNAT Pro for Ada, the GNAT Static and - Dynamic Analysis Suites, and the SPARK Pro toolset support the + * The Ada and SPARK languages, GNAT Pro for Ada, CodeSonar for Ada, the + GNAT Dynamic Analysis Suite, and the SPARK Pro toolset support the software security management plan. .. _Space_Systems_SW_Software_security_analysis: @@ -667,16 +667,16 @@ Software security analysis {|sect| 5.11.3} * "The methods to be used for the security analysis shall be identified as part of the planning of the project." {|sect| 5.11.3b} - * The Ada and SPARK languages, GNAT Pro for Ada, the GNAT Static and - Dynamic Analysis Suites, and the SPARK Pro toolset help meet this + * The Ada and SPARK languages, GNAT Pro for Ada, CodeSonar for Ada, the + GNAT Dynamic Analysis Suite, and the SPARK Pro toolset help meet this requirement. For example: * Ada's compile-time checks prevent unsafe practices such as treating an integer value as a pointer. - * The Defects and Vulnerability Analyzer in the GNAT Static Analysis - Suite can detect a number of dangerous software errors in the - MITRE Corporation's Common Weakness Enumeration. + * The Defects and Vulnerability Analyzer in CodeSonar for Ada can detect + a number of dangerous software errors in the MITRE Corporation's + Common Weakness Enumeration. * The SPARK language and SPARK Pro can enforce security-related properties such as correct information flows and absence of @@ -696,8 +696,8 @@ Security in the requirements baseline {|sect| 5.11.5.1} to be conducted.... Security verification and validation activities can include, for example, fuzzing tests...." {|sect| 5.11.5.1c} - * The Ada and SPARK languages, GNAT Pro for Ada, the GNAT Static and - Dynamic Analysis Suites, and the SPARK Pro toolset help meet this + * The Ada and SPARK languages, GNAT Pro for Ada, CodeSonar for Ada, the + GNAT Dynamic Analysis Suite, and the SPARK Pro toolset help meet this requirement. Security in the detailed design and implementation engineering {|sect| 5.11.5.3} @@ -707,9 +707,9 @@ Security in the detailed design and implementation engineering {|sect| 5.11.5.3} validation activities to evaluate iteratively residual vulnerabilities and to reassess security risks." {|sect| 5.11.5.3b} - * The Ada and SPARK languages, the GNAT Static and Dynamic Analysis - Suites, and the SPARK Pro toolset help meet this requirement. For - examples, see :ref:`Space_Systems_SW_Software_security_analysis`. + * The Ada and SPARK languages, CodeSonar for Ada, the GNAT Dynamic Analysis + Suite, and the SPARK Pro toolset help meet this requirement. For examples, + see :ref:`Space_Systems_SW_Software_security_analysis`. .. index:: single: ECSS-E-ST-40C compliance; Annex U: Software code verification @@ -772,32 +772,32 @@ technologies help meet these requirements: | | SPARK language, SPARK Pro | Static check | | +---------------------------------------------------------------+----------------------------------------+ | | Defects and Vulnerability Analyzer | Static check [#stcheck]_ | - | | (in GNAT Static Analysis Suite) | | + | | (in CodeSonar for Ada) | | +-------------------------+---------------------------------------------------------------+----------------------------------------+ | 2 | Ada language, GNAT Pro for Ada, GNAT Pro Assurance | Run-time check [#rtcheck]_ | | +---------------------------------------------------------------+----------------------------------------+ | | SPARK language, SPARK Pro | Static check | | +---------------------------------------------------------------+----------------------------------------+ | | Defects and Vulnerability Analyzer | Static check [#stcheck]_ | - | | (in GNAT Static Analysis Suite) | | + | | (in CodeSonar for Ada) | | +-------------------------+---------------------------------------------------------------+----------------------------------------+ | 3 | Defects and Vulnerability Analyzer | Static check [#stcheck]_ | - | | (in GNAT Static Analysis Suite) | | + | | (in CodeSonar for Ada) | | | +---------------------------------------------------------------+----------------------------------------+ - | | GNATcheck (in GNAT Static Analysis Suite) | User-defined rule | + | | GNATcheck (in CodeSonar for Ada) | User-defined rule | | +---------------------------------------------------------------+----------------------------------------+ | | SPARK language, SPARK Pro | Static check | +-------------------------+---------------------------------------------------------------+----------------------------------------+ | 4 | Ada language, GNAT Pro for Ada, GNAT Pro Assurance | Static check | | | SPARK language, SPARK Pro | | | +---------------------------------------------------------------+----------------------------------------+ - | | GNATcheck (in GNAT Static Analysis Suite) | User-defined rule | + | | GNATcheck (in CodeSonar for Ada) | User-defined rule | +-------------------------+---------------------------------------------------------------+----------------------------------------+ | 5 | Ada language, GNAT Pro for Ada, GNAT Pro Assurance | Static check | | | SPARK language, SPARK Pro | | | +---------------------------------------------------------------+----------------------------------------+ | | Defects and Vulnerability Analyzer | Static check [#stcheck]_ | - | | (in GNAT Static Analysis Suite) | | + | | (in CodeSonar for Ada) | | +-------------------------+---------------------------------------------------------------+----------------------------------------+ | 6 | Ada language, GNAT Pro for Ada, GNAT Pro Assurance | Static check | | | SPARK language, SPARK Pro | | @@ -806,25 +806,25 @@ technologies help meet these requirements: | | SPARK language, SPARK Pro | | +-------------------------+---------------------------------------------------------------+----------------------------------------+ | 8 | Defects and Vulnerability Analyzer | Static check [#stcheck]_ | - | | (in GNAT Static Analysis Suite) | | + | | (in CodeSonar for Ada) | | +-------------------------+---------------------------------------------------------------+----------------------------------------+ | 9 | Ada language, GNAT Pro for Ada, GNAT Pro Assurance | Run-time check [#rtcheck]_ | | +---------------------------------------------------------------+----------------------------------------+ | | SPARK language, SPARK Pro | Static check | | +---------------------------------------------------------------+----------------------------------------+ | | Defects and Vulnerability Analyzer | Static check [#stcheck]_ | - | | (in GNAT Static Analysis Suite) | | + | | (in CodeSonar for Ada) | | +-------------------------+---------------------------------------------------------------+----------------------------------------+ | 10 | SPARK language, SPARK Pro | Static check | | +---------------------------------------------------------------+----------------------------------------+ | | Defects and Vulnerability Analyzer | Static check [#stcheck]_ | - | | (in GNAT Static Analysis Suite) | | + | | (in CodeSonar for Ada) | | +-------------------------+---------------------------------------------------------------+----------------------------------------+ | 11 | Defects and Vulnerability Analyzer | Static check [#stcheck]_ | - | | (in GNAT Static Analysis Suite) | | + | | (in CodeSonar for Ada) | | +-------------------------+---------------------------------------------------------------+----------------------------------------+ | 12 | Defects and Vulnerability Analyzer | Static check [#stcheck]_ | - | | (in GNAT Static Analysis Suite) | | + | | (in CodeSonar for Ada) | | | +---------------------------------------------------------------+----------------------------------------+ | | Ada Language, GNAT Pro for Ada, GNAT Pro Assurance | Run-time check [#memleak]_ | | +---------------------------------------------------------------+----------------------------------------+ @@ -834,7 +834,7 @@ technologies help meet these requirements: | | SPARK language, SPARK Pro | | +-------------------------+---------------------------------------------------------------+----------------------------------------+ | 14 | Defects and Vulnerability Analyzer | Static check [#stcheck]_ | - | | (in GNAT Static Analysis Suite) | | + | | (in CodeSonar for Ada) | | +-------------------------+---------------------------------------------------------------+----------------------------------------+ .. [#rtcheck] Depending on the source code, the GNAT Pro compiler may be @@ -884,7 +884,7 @@ AdaCore's technologies support the requirements in ECSS-E-ST-40C: +-----------------------------+-------------+------------+-------------+-------------+-------------+-------------+--------------+--------------+---------+ | SPARK Pro | |check| | |check| | |check| | | |check| | | |check| | |check| | |check| | +-----------------------------+-------------+------------+-------------+-------------+-------------+-------------+--------------+--------------+---------+ - | GNAT Static Analysis Suite | | |check| | |check| | | |check| | | |check| | |check| | |check| | + | CodeSonar for Ada | | |check| | |check| | | |check| | | |check| | |check| | |check| | +-----------------------------+-------------+------------+-------------+-------------+-------------+-------------+--------------+--------------+---------+ | GNAT Dynamic Analysis Suite | | |check| | |check| | | |check| | | |check| | |check| | | +-----------------------------+-------------+------------+-------------+-------------+-------------+-------------+--------------+--------------+---------+ diff --git a/content/booklets/adacore-technologies-for-space-systems-software/chapters/compliance-q80c.rst b/content/booklets/adacore-technologies-for-space-systems-software/chapters/compliance-q80c.rst index 6cdbcd766..945a16165 100644 --- a/content/booklets/adacore-technologies-for-space-systems-software/chapters/compliance-q80c.rst +++ b/content/booklets/adacore-technologies-for-space-systems-software/chapters/compliance-q80c.rst @@ -26,7 +26,7 @@ Quality requirements and quality models {§5.2.7} requirements" {§5.2.7.1a} * The GNATmetric tool (see :ref:`Space_Systems_SW_GNATmetric`) in - the GNAT Static Analysis Suite can show quality metrics related + CodeSonar for Ada can show quality metrics related to the source code structure. * The GNATdashboard IDE tool (see @@ -44,7 +44,7 @@ Methods and tools {§5.6.1} {§5.6.1.1a} * The GNAT Pro for Ada environment and any supplemental tools that are - selected (e.g., GNAT Static and Dynamic Analysis Suites, SPARK Pro) + selected (e.g., CodeSonar for Ada, GNAT Dynamic Analysis Suite, SPARK Pro) should be listed. * "The choice of development methods and tools shall be justified by @@ -100,7 +100,7 @@ Development environment selection {§5.6.2} *sustained branch* service for GNAT Pro for Ada Assurance supports criteria 4, 7 and 10. AdaCore tools come with source code and flexible licensing, mitigating the issues noted in criteria 11 and 12. - The GNAT Static Analysis Suite, SPARK, and the GNATfuzz tool in + CodeSonar for Ada, SPARK, and the GNATfuzz tool in the GNAT Dynamic Analysis Suite facilitate demonstrating the relevant security properties (criteria 13 and 14). @@ -126,7 +126,7 @@ Handling of critical software {§6.2.3} {§6.2.3.2a} * Ada's pragma :ada:`Restrictions` and pragma :ada:`Profile`, - together with the GNAT Static Analysis Suite tool GNATcheck, can + together with GNATcheck from CodeSonar for Ada, can enforce a coding standard for Ada (in effect a 'safe subset'). See :ref:`Space_Systems_SW_GNAT_Pro_Enterprise` and :ref:`Space_Systems_SW_GNATcheck`. @@ -139,7 +139,7 @@ Handling of critical software {§6.2.3} * GNATcoverage can report code coverage up to MC/DC at the source level. - * The Defects and Vulnerability Analyzer in the GNAT Static Analysis Suite + * The Defects and Vulnerability Analyzer in CodeSonar for Ada can detect unreachable code, including deactivated code. * The Ada language and the GNAT Pro Ada development environment allow @@ -159,7 +159,7 @@ Verification {§6.2.6} ensure that the deactivated code cannot be activated or that its accidental activation cannot harm the operation of the system." {§6.2.6.5a} - * The Defects and Vulnerability Analyzer in the GNAT Static Analysis Suite + * The Defects and Vulnerability Analyzer in CodeSonar for Ada can detect unreachable code, including deactivated code. Software security {§6.2.9} @@ -168,8 +168,9 @@ Software security {§6.2.9} * "The supplier shall identify the methods and techniques for the software security analysis." {|sect| 6.2.9.3a} - * The Ada and SPARK languages, GNAT Pro for Ada, the GNAT Static and Dynamic - Analysis Suites, and the SPARK Pro toolset help meet this requirement. + * The Ada and SPARK languages, GNAT Pro for Ada, CodeSonar for Ada, the + GNAT Dynamic Analysis Suite, and the SPARK Pro toolset help meet this + requirement. * "Based on the results of the software security analysis, the supplier shall apply engineering measures to reduce the number of security sensitive @@ -423,7 +424,7 @@ AdaCore's technologies support the requirements in ECSS-Q-ST-80C: +-----------------------------+-------------+-------------+-------------+-------------+-------------+-------------+ | SPARK Pro | |blankcell| | |check| | |check| | |blankcell| | |check| | |check| | +-----------------------------+-------------+-------------+-------------+-------------+-------------+-------------+ - | GNAT Static Analysis Suite | |blankcell| | |check| | |check| | |check| | |check| | |blankcell| | + | CodeSonar for Ada | |blankcell| | |check| | |check| | |check| | |check| | |blankcell| | +-----------------------------+-------------+-------------+-------------+-------------+-------------+-------------+ | GNAT Dynamic Analysis Suite | |blankcell| | |check| | |check| | |check| | |check| | |check| | +-----------------------------+-------------+-------------+-------------+-------------+-------------+-------------+ diff --git a/content/booklets/adacore-technologies-for-space-systems-software/chapters/programming.rst b/content/booklets/adacore-technologies-for-space-systems-software/chapters/programming.rst index f9d165bf8..be007d2e5 100644 --- a/content/booklets/adacore-technologies-for-space-systems-software/chapters/programming.rst +++ b/content/booklets/adacore-technologies-for-space-systems-software/chapters/programming.rst @@ -564,14 +564,14 @@ problematic features. Several techniques are available: that comprise the Ravenscar tasking subset. .. index:: GNATcheck -.. index: GNAT Static Analysis Suite; GNATcheck +.. index:: single: CodeSonar for Ada; GNATcheck * Static analysis tool (coding standard enforcer) Other restrictions on Ada features can be detected by AdaCore's automated GNATcheck tool (see :ref:`Space_Systems_SW_GNATcheck`) - that is included with the GNAT Pro Ada Static Analysis Suite. The - developer can configure this rule-based and tailorable tool to flag + that is included with CodeSonar for Ada. The developer can configure + this rule-based and tailorable tool to flag violations of the project's coding standard, such as usage of specific prohibited types or subprograms defined in otherwise-permitted packages. diff --git a/content/booklets/adacore-technologies-for-space-systems-software/chapters/table-technology-e40C-compliance-summary.csv b/content/booklets/adacore-technologies-for-space-systems-software/chapters/table-technology-e40C-compliance-summary.csv index f2816aff2..e619fe175 100644 --- a/content/booklets/adacore-technologies-for-space-systems-software/chapters/table-technology-e40C-compliance-summary.csv +++ b/content/booklets/adacore-technologies-for-space-systems-software/chapters/table-technology-e40C-compliance-summary.csv @@ -5,6 +5,6 @@ SPARK language, |check| , |check| , |blankcell|, |blankcell|, |check| , |blankcell|, |check| , |check| , |check| GNAT Pro for Ada, |check| , |check| , |check| , |check| , |check| , |blankcell|, |check| , |check| , |check| SPARK Pro, |check| , |check| , |check| , |blankcell|, |check| , |blankcell|, |check| , |check| , |check| - GNAT SAS, |blankcell|, |check| , |check| , |blankcell|, |check| , |blankcell|, |check| , |check| , |check| + CodeSonar for Ada, |blankcell|, |check| , |check| , |blankcell|, |check| , |blankcell|, |check| , |check| , |check| GNAT DAS, |blankcell|, |check| , |check| , |blankcell|, |check| , |blankcell|, |check| , |check| , |blankcell| GNAT Pro Assurance, |check| , |check| , |check| , |check| , |check| , |check| , |check| , |check| , |check| \ No newline at end of file diff --git a/content/booklets/adacore-technologies-for-space-systems-software/chapters/table-technology-q80c-compliance-summary.csv b/content/booklets/adacore-technologies-for-space-systems-software/chapters/table-technology-q80c-compliance-summary.csv index ad84ef269..c105a3e5a 100644 --- a/content/booklets/adacore-technologies-for-space-systems-software/chapters/table-technology-q80c-compliance-summary.csv +++ b/content/booklets/adacore-technologies-for-space-systems-software/chapters/table-technology-q80c-compliance-summary.csv @@ -5,7 +5,7 @@ SPARK language, |blankcell|, |check| , |check| GNAT Pro for Ada, |check| , |check| , |check| SPARK Pro, |check| , |check| , |check| - GNAT SAS, |check| , |check| , |check| + CodeSonar for Ada, |check| , |check| , |check| GNAT DAS, |check| , |check| , |check| GNAT Pro Assurance, |check| , |check| , |check| IDE, |check| , |check| , |check| \ No newline at end of file diff --git a/content/booklets/adacore-technologies-for-space-systems-software/chapters/table-verification-support.csv b/content/booklets/adacore-technologies-for-space-systems-software/chapters/table-verification-support.csv index 6aa50db14..1c9fe2636 100644 --- a/content/booklets/adacore-technologies-for-space-systems-software/chapters/table-verification-support.csv +++ b/content/booklets/adacore-technologies-for-space-systems-software/chapters/table-verification-support.csv @@ -7,26 +7,26 @@ Verification check #,Technology,Explanation 1,Ada language,Run-time check\ :superscript:`*` 1,SPARK language,Static check - 1,Defects and Vulnerability Analyzer (in GNAT Static Analysis Suite),Static check\ :superscript:`**` + 1,Defects and Vulnerability Analyzer (in CodeSonar for Ada),Static check\ :superscript:`**` 2,Ada language,Run-time check\ :superscript:`*` 2,SPARK language,Static check - 2,Defects and Vulnerability Analyzer (in GNAT Static Analysis Suite),Static check\ :superscript:`**` - 3,Defects and Vulnerability Analyzer (in GNAT Static Analysis Suite),Static check\ :superscript:`**` - 3,GNATcheck (in GNAT Static Analysis Suite),User-defined rule + 2,Defects and Vulnerability Analyzer (in CodeSonar for Ada),Static check\ :superscript:`**` + 3,Defects and Vulnerability Analyzer (in CodeSonar for Ada),Static check\ :superscript:`**` + 3,GNATcheck (in CodeSonar for Ada),User-defined rule 4,Ada and SPARK languages, Static check 5,Ada and SPARK languages, Static check - 5,Defects and Vulnerability Analyzer (in GNAT Static Analysis Suite),Static check\ :superscript:`**` + 5,Defects and Vulnerability Analyzer (in CodeSonar for Ada),Static check\ :superscript:`**` 6,Ada and SPARK languages, Static check 7,Ada and SPARK languages, Static check - 8,Defects and Vulnerability Analyzer (in GNAT Static Analysis Suite),Static check\ :superscript:`**` + 8,Defects and Vulnerability Analyzer (in CodeSonar for Ada),Static check\ :superscript:`**` 9,Ada language,Run-time check\ :superscript:`*` 9,SPARK language,Static check - 9,Defects and Vulnerability Analyzer (in GNAT Static Analysis Suite),Static check\ :superscript:`**` + 9,Defects and Vulnerability Analyzer (in CodeSonar for Ada),Static check\ :superscript:`**` 10,SPARK language,Static check - 10,Defects and Vulnerability Analyzer (in GNAT Static Analysis Suite),Static check\ :superscript:`**` - 11,Defects and Vulnerability Analyzer (in GNAT Static Analysis Suite),Static check\ :superscript:`**` - 12,Defects and Vulnerability Analyzer (in GNAT Static Analysis Suite),Static check\ :superscript:`**` + 10,Defects and Vulnerability Analyzer (in CodeSonar for Ada),Static check\ :superscript:`**` + 11,Defects and Vulnerability Analyzer (in CodeSonar for Ada),Static check\ :superscript:`**` + 12,Defects and Vulnerability Analyzer (in CodeSonar for Ada),Static check\ :superscript:`**` 12,Ada Language,Run-time check\ :superscript:`***` 13,Ada and SPARK languages, Static check - 14,Defects and Vulnerability Analyzer (in GNAT Static Analysis Suite),Static check\ :superscript:`**` + 14,Defects and Vulnerability Analyzer (in CodeSonar for Ada),Static check\ :superscript:`**` diff --git a/content/booklets/adacore-technologies-for-space-systems-software/chapters/tools.rst b/content/booklets/adacore-technologies-for-space-systems-software/chapters/tools.rst index 448a037c8..ded85f21e 100644 --- a/content/booklets/adacore-technologies-for-space-systems-software/chapters/tools.rst +++ b/content/booklets/adacore-technologies-for-space-systems-software/chapters/tools.rst @@ -50,11 +50,11 @@ of the *V*. In summary: variety of supplemental libraries (including some for which qualification material is available for |E-ST-40C| and |Q-ST-80C|.) -.. index:: single: GNAT Static Analysis Suite (GNAT SAS); Software life cycle -.. index:: single: Software life cycle; GNAT Static Analysis Suite (GNAT SAS) +.. index:: single: CodeSonar for Ada; Software life cycle +.. index:: single: Software life cycle; CodeSonar for Ada -* The GNAT Static Analysis Suite (see - :ref:`Space_Systems_SW_Static_Verification_GNAT_Static_Analysis_Suite_GNAT_SAS`) +* CodeSonar for Ada (see + :ref:`Space_Systems_SW_Static_Verification_CodeSonar_for_Ada`) applies during Software Development. It contains a variety of tools for Ada, including a vulnerability detector that can be used retrospectively to detect issues in existing codebases and/or during @@ -814,28 +814,28 @@ Footprint) QUAL run-time library (superseded by the Light-Tasking run-time) on LEON2 and LEON3 boards have been qualified at criticality category B (see :footcite:p:`Space_SW_AdaCore_Web_2019b`). -.. index:: GNAT Static Analysis Suite (GNAT SAS) +.. index:: CodeSonar for Ada -.. _Space_Systems_SW_Static_Verification_GNAT_Static_Analysis_Suite_GNAT_SAS: +.. _Space_Systems_SW_Static_Verification_CodeSonar_for_Ada: -Static Verification: GNAT Static Analysis Suite (GNAT SAS) ----------------------------------------------------------- +Static Verification: CodeSonar for Ada +-------------------------------------- -GNAT SAS is a set of Ada static analysis tools that complement |gnatpro| -for Ada. These tools can save time and effort in general during software -development and verification, and they are useful in particular in +CodeSonar for Ada is a set of Ada static analysis tools that complement +|gnatpro| for Ada. These tools can save time and effort in general during +software development and verification, and they are useful in particular in supporting compliance with ECSS standards. -.. index:: single: GNAT Static Analysis Suite (GNAT SAS); Defects and Vulnerability Analyzer +.. index:: single: CodeSonar for Ada; Defects and Vulnerability Analyzer .. _Space_Systems_SW_Defects_and_Vulnerability_Analyzer: Defects and Vulnerability Analyzer ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -One of the main tools in GNAT SAS is an Ada source code analyzer that detects -run-time and logic errors that can cause safety or security vulnerabilities -in a codebase. +One of the main tools in CodeSonar for Ada is an Ada source code analyzer +that detects run-time and logic errors that can cause safety or security +vulnerabilities in a codebase. This tool inspects the code for potential bugs before program execution, serving as an automated peer reviewer. It can be used on existing codebases, thereby @@ -927,7 +927,7 @@ these are the relevant sections of the two standards: * §7.1.3 Assurance activities for product quality requirements -.. index:: single: GNAT Static Analysis Suite (GNAT SAS); GNATmetric +.. index:: single: CodeSonar for Ada; GNATmetric .. index:: GNATmetric .. _Space_Systems_SW_GNATmetric: @@ -974,7 +974,7 @@ summary: * §7.1.5 Basic metrics .. index:: GNATcheck -.. index:: single: GNAT Static Analysis Suite (GNAT SAS); GNATcheck +.. index:: single: CodeSonar for Ada; GNATcheck .. _Space_Systems_SW_GNATcheck: diff --git a/content/booklets/adacore-technologies-for-space-systems-software/index.rst b/content/booklets/adacore-technologies-for-space-systems-software/index.rst index bbba2de37..3a402b7f2 100644 --- a/content/booklets/adacore-technologies-for-space-systems-software/index.rst +++ b/content/booklets/adacore-technologies-for-space-systems-software/index.rst @@ -180,7 +180,7 @@ reflects the current (2025) versions of |E-ST-40C|, |Q-ST-80C|, and AdaCore's offerings. Among other updates and enhancements to the company's products, the static analysis tools supplementing the |gnatpro| development environment have been -integrated into a cohesive toolset (the *GNAT Static Analysis Suite*). +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 diff --git a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/README.md b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/README.md index e62f2c126..ee335aae7 100644 --- a/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/README.md +++ b/content/courses/Guidelines_for_Safe_and_Secure_Ada_SPARK/README.md @@ -29,7 +29,7 @@ please see the Sphinx documentation ### GNATcheck -`GNATcheck` is part of the Static Analysis Suite provided by **AdaCore**. +`GNATcheck` is part of CodeSonar for Ada, provided by **AdaCore**. It is designed as a coding standards checker, and comes with many pre-defined rules to use in validating standards conformance. In addition, it uses the **Langkit Query Language** to allow users to diff --git a/content/courses/intro-to-spark/chapters/01_Overview.rst b/content/courses/intro-to-spark/chapters/01_Overview.rst index 05f4838af..6233bf9e2 100644 --- a/content/courses/intro-to-spark/chapters/01_Overview.rst +++ b/content/courses/intro-to-spark/chapters/01_Overview.rst @@ -63,7 +63,7 @@ it. Verification uses tools that perform static analysis. These can take various forms. They include tools that check types and enforce visibility rules, such as the compiler, in addition to those that perform more complex reasoning, such as abstract interpretation, as done by a tool like the -`GNAT Static Analysis Suite `_ +`CodeSonar for Ada `_ from AdaCore. The tools that come with SPARK perform two different forms of static analysis: diff --git a/content/global.txt b/content/global.txt index e034f9b98..ac997fbb6 100644 --- a/content/global.txt +++ b/content/global.txt @@ -46,7 +46,7 @@ .. |do-331| replace:: DO |nbhyphen| 331/ED |nbhyphen| 218 .. |do-332| replace:: DO |nbhyphen| 332/ED |nbhyphen| 217 .. |do-333| replace:: DO |nbhyphen| 333/ED |nbhyphen| 216 -.. |gnatsas| replace:: GNAT SAS +.. |codesonar-for-ada| replace:: CodeSonar for Ada .. |gnatdas| replace:: GNAT DAS .. |gnatpro| replace:: GNAT\ |nbsp|\ Pro