Removed SPARK annotations.

simonjwright · simonjwright · commit 4087cb78b9d1 · 2022-05-13T17:20:52.000+01:00
* src/aes.adb,
  src/analytical_engine-annunciator_panel-command_line.adb,
  src/analytical_engine-annunciator_panel-command_line.ads,
  src/analytical_engine-annunciator_panel.adb,
  src/analytical_engine-annunciator_panel.ads,
  src/analytical_engine-card-action_card.adb,
  src/analytical_engine-card-action_card.ads,
  src/analytical_engine-card-combinatorial_card.adb,
  src/analytical_engine-card-combinatorial_card.ads,
  src/analytical_engine-card-comment_card.ads,
  src/analytical_engine-card-number_card.adb,
  src/analytical_engine-card-number_card.ads,
  src/analytical_engine-card-operation_card.adb,
  src/analytical_engine-card-operation_card.ads,
  src/analytical_engine-card-stepping_card.ads,
  src/analytical_engine-card-tracing_card.adb,
  src/analytical_engine-card-tracing_card.ads,
  src/analytical_engine-card-variable_card.adb,
  src/analytical_engine-card-variable_card.ads,
  src/analytical_engine-card.ads src/analytical_engine-mill.adb,
  src/analytical_engine-mill.ads
  src/analytical_engine-output-printer.adb,
  src/analytical_engine-output-printer.ads,
  src/analytical_engine-output.adb, src/analytical_engine-output.ads: the
    code makes use of Ada features (private with, f.e.) which lead to
    SPARK incompatibility when used. I think.
diff --git a/src/aes.adb b/src/aes.adb
@@ -35,8 +35,6 @@ use Analytical_Engine;
 
 procedure Aes is
 
-   pragma SPARK_Mode (Off);
-
    Command_Line_Config : GNAT.Command_Line.Command_Line_Configuration;
    Tracing : aliased Boolean := False;
    Allow_Overwrite_Nonzero : aliased Boolean := False;
diff --git a/src/analytical_engine-annunciator_panel-command_line.adb b/src/analytical_engine-annunciator_panel-command_line.adb
@@ -22,8 +22,6 @@
 with Ada.Wide_Text_IO; use Ada.Wide_Text_IO;
 package body Analytical_Engine.Annunciator_Panel.Command_Line is
 
-   pragma SPARK_Mode (Off);
-
    procedure Log_Attendant_Message (Panel : Instance; Msg : Wide_String)
    is
       pragma Unreferenced (Panel);
diff --git a/src/analytical_engine-annunciator_panel-command_line.ads b/src/analytical_engine-annunciator_panel-command_line.ads
@@ -21,7 +21,6 @@
 
 package Analytical_Engine.Annunciator_Panel.Command_Line is
 
-   pragma SPARK_Mode (On);
    pragma Elaborate_Body;
 
    type Instance is new Annunciator_Panel.Instance with private;
diff --git a/src/analytical_engine-annunciator_panel.adb b/src/analytical_engine-annunciator_panel.adb
@@ -21,8 +21,6 @@
 
 package body Analytical_Engine.Annunciator_Panel is
 
-   pragma SPARK_Mode (Off);
-
    procedure Set_Tracing (This : in out Instance; To : Boolean) is
    begin
       This.Tracing := To;
diff --git a/src/analytical_engine-annunciator_panel.ads b/src/analytical_engine-annunciator_panel.ads
@@ -22,7 +22,6 @@
 --  private with Ada.Finalization;
 package Analytical_Engine.Annunciator_Panel is
 
-   pragma SPARK_Mode (On);
    pragma Elaborate_Body;
 
    type Instance is abstract tagged limited private;
diff --git a/src/analytical_engine-card-action_card.adb b/src/analytical_engine-card-action_card.adb
@@ -4,8 +4,6 @@ with GNATCOLL.GMP.Integers;
 
 package body Analytical_Engine.Card.Action_Card is
 
-   pragma SPARK_Mode (On);
-
    use GNATCOLL.GMP.Integers;
 
    procedure Execute (C : Action_Card;
diff --git a/src/analytical_engine-card-action_card.ads b/src/analytical_engine-card-action_card.ads
@@ -1,6 +1,5 @@
 private package Analytical_Engine.Card.Action_Card is
 
-   pragma SPARK_Mode (On);
    pragma Elaborate_Body;
 
    type Action_Kind is (Ring_Bell, Halt_Engine, Print_Last_Result);
diff --git a/src/analytical_engine-card-combinatorial_card.adb b/src/analytical_engine-card-combinatorial_card.adb
@@ -2,8 +2,6 @@ with Analytical_Engine.Framework;
 
 package body Analytical_Engine.Card.Combinatorial_Card is
 
-   pragma SPARK_Mode (On);
-
    procedure Execute (C : Combinatorial_Card;
                       In_The_Framework : in out Framework.Instance)
    is
diff --git a/src/analytical_engine-card-combinatorial_card.ads b/src/analytical_engine-card-combinatorial_card.ads
@@ -1,6 +1,5 @@
 private package Analytical_Engine.Card.Combinatorial_Card is
 
-   pragma SPARK_Mode (On);
    pragma Elaborate_Body;
 
    type Combinatorial_Card is new Card with record
diff --git a/src/analytical_engine-card-comment_card.ads b/src/analytical_engine-card-comment_card.ads
@@ -1,8 +1,5 @@
 private package Analytical_Engine.Card.Comment_Card is
 
-   pragma SPARK_Mode (On);
-   --  pragma Elaborate_Body;
-
    type Comment_Card is new Card with null record;
    overriding
    procedure Execute (C : Comment_Card;
diff --git a/src/analytical_engine-card-number_card.adb b/src/analytical_engine-card-number_card.adb
@@ -2,8 +2,6 @@ with Analytical_Engine.Framework;  -- was 'limited with' in parent spec
 
 package body Analytical_Engine.Card.Number_Card is
 
-   pragma SPARK_Mode (On);
-
    procedure Execute
      (C : Number_Card;
       In_The_Framework : in out Analytical_Engine.Framework.Instance)
diff --git a/src/analytical_engine-card-number_card.ads b/src/analytical_engine-card-number_card.ads
@@ -4,7 +4,6 @@ with Analytical_Engine.Store;
 
 private package Analytical_Engine.Card.Number_Card is
 
-   pragma SPARK_Mode (On);
    pragma Elaborate_Body;
 
    type Big_Integer_P is access GNATCOLL.GMP.Integers.Big_Integer;
diff --git a/src/analytical_engine-card-operation_card.adb b/src/analytical_engine-card-operation_card.adb
@@ -2,8 +2,6 @@ with Analytical_Engine.Framework;
 
 package body Analytical_Engine.Card.Operation_Card is
 
-   pragma SPARK_Mode (On);
-
    procedure Execute
      (C : Operation_Card;
       In_The_Framework : in out Analytical_Engine.Framework.Instance)
diff --git a/src/analytical_engine-card-operation_card.ads b/src/analytical_engine-card-operation_card.ads
@@ -2,7 +2,6 @@ with Analytical_Engine.Mill;
 
 private package Analytical_Engine.Card.Operation_Card is
 
-   pragma SPARK_Mode (On);
    pragma Elaborate_Body;
 
    type Operation_Card is new Card with record
diff --git a/src/analytical_engine-card-stepping_card.ads b/src/analytical_engine-card-stepping_card.ads
@@ -2,7 +2,6 @@ with Analytical_Engine.Mill;
 
 private package Analytical_Engine.Card.Stepping_Card is
 
-   pragma SPARK_Mode (On);
    pragma Elaborate_Body;
 
    type Stepping_Card is new Card with record
diff --git a/src/analytical_engine-card-tracing_card.adb b/src/analytical_engine-card-tracing_card.adb
@@ -2,8 +2,6 @@ with Analytical_Engine.Framework;
 
 package body Analytical_Engine.Card.Tracing_Card is
 
-   pragma SPARK_Mode (On);
-
    procedure Execute (C : Tracing_Card;
                       In_The_Framework : in out Framework.Instance)
    is
diff --git a/src/analytical_engine-card-tracing_card.ads b/src/analytical_engine-card-tracing_card.ads
@@ -1,6 +1,5 @@
 private package Analytical_Engine.Card.Tracing_Card is
 
-   pragma SPARK_Mode (On);
    pragma Elaborate_Body;
 
    type Tracing_Card is new Card with record
diff --git a/src/analytical_engine-card-variable_card.adb b/src/analytical_engine-card-variable_card.adb
@@ -4,8 +4,6 @@ with GNATCOLL.GMP.Integers;
 
 package body Analytical_Engine.Card.Variable_Card is
 
-   pragma SPARK_Mode (On);
-
    use GNATCOLL.GMP.Integers;
 
    procedure Execute
diff --git a/src/analytical_engine-card-variable_card.ads b/src/analytical_engine-card-variable_card.ads
@@ -3,7 +3,6 @@ with Analytical_Engine.Store;
 
 private package Analytical_Engine.Card.Variable_Card is
 
-   pragma SPARK_Mode (On);
    pragma Elaborate_Body;
 
    type Variable_Card is new Card with record
diff --git a/src/analytical_engine-card.ads b/src/analytical_engine-card.ads
@@ -29,8 +29,6 @@ private with System;
 
 package Analytical_Engine.Card is
 
-   pragma SPARK_Mode (On);
-
    --  Notes from http://www.fourmilab.ch/babbage/cards.html.
 
    --  Program Cards
diff --git a/src/analytical_engine-mill.adb b/src/analytical_engine-mill.adb
@@ -23,8 +23,6 @@ with Ada.Characters.Conversions;
 
 package body Analytical_Engine.Mill is
 
-   pragma SPARK_Mode;
-
    Max_Value : constant Big_Integer
      := Make ("100000000000000000000000000000000000000000000000000");
    Min_Value : constant Big_Integer := -Max_Value;
diff --git a/src/analytical_engine-mill.ads b/src/analytical_engine-mill.ads
@@ -25,9 +25,6 @@ with GNATCOLL.GMP.Integers; use GNATCOLL.GMP.Integers;
 
 package Analytical_Engine.Mill is
 
-   pragma SPARK_Mode;
-   --  pragma Elaborate_Body;
-
    type Axis is
      (Ingress,
       Ingress_Primed,
diff --git a/src/analytical_engine-output-printer.adb b/src/analytical_engine-output-printer.adb
@@ -24,8 +24,6 @@ with Ada.Wide_Text_IO; use Ada.Wide_Text_IO;
 
 package body Analytical_Engine.Output.Printer is
 
-   pragma SPARK_Mode (Off);
-
    procedure Output (To : Instance; S : Wide_String)
    is
    begin
diff --git a/src/analytical_engine-output-printer.ads b/src/analytical_engine-output-printer.ads
@@ -22,7 +22,6 @@
 with Analytical_Engine.Annunciator_Panel;
 package Analytical_Engine.Output.Printer is
 
-   pragma SPARK_Mode (Off);
    pragma Elaborate_Body;
 
    type Instance (Panel : not null Annunciator_Panel.Class_P)
diff --git a/src/analytical_engine-output.adb b/src/analytical_engine-output.adb
@@ -21,8 +21,6 @@
 
 package body Analytical_Engine.Output is
 
-   pragma SPARK_Mode (Off);
-
    procedure Set_Picture
      (This : in out Instance;
       To : Ada.Strings.Wide_Unbounded.Unbounded_Wide_String)
diff --git a/src/analytical_engine-output.ads b/src/analytical_engine-output.ads
@@ -26,8 +26,6 @@ with GNATCOLL.GMP.Integers;
 
 package Analytical_Engine.Output is
 
-   pragma SPARK_Mode (Off);
-
    type Instance (Panel : not null Annunciator_Panel.Class_P)
      is abstract new Ada.Finalization.Limited_Controlled with private;
    type Class_P is access all Instance'Class;
