Add new file lang/spark (will become run-depends for GPS)

SPARK 2014 is a programming language and a set of verification tools
designed to meet the needs of high-assurance software development. SPARK
is based on Ada 2012, both subsetting the language to remove features that
defy verification, but also extending the system of contracts and aspects
to support modular, formal verification.

The new aspects support abstraction and refinement and facilitate deep
static analysis to be performed including information-flow analysis and
formal verification of an implementation against a specification.

SPARK is a much larger and more flexible language than its predecessor
SPARK 2005. The language can be configured to suit a number of application
domains and standards, from server-class high-assurance systems (such as
air-traffic management applications), to embedded, hard real-time,
critical systems (such as avionic systems complying with DO-178C Level A).

A major feature of SPARK is the support for a mixture of proof and other
verification methods such as testing, which facilitates the use of unit
proof in place of unit testing; an approach now formalized in DO-178C and
the DO-333 formal methods supplement. Certain units may be formally proven
and other units validated through testing.

1 files changed, 36 insertions, 0 deletions

diff --git a/lang/spark/files/patch-gnatvsn.adb b/lang/spark/files/patch-gnatvsn.adb
new file mode 100644
index 000000000000..18ac935c7c15
--- /dev/null
+++ b/lang/spark/files/patch-gnatvsn.adb
@@ -0,0 +1,36 @@
+--- gnat2why/gnat_src/gnatvsn.adb.orig	2010-12-03 04:48:56 UTC
++++ gnat2why/gnat_src/gnatvsn.adb
+@@ -53,32 +53,13 @@ package body Gnatvsn is
+         " FOR A PARTICULAR PURPOSE.";
+    end Gnat_Free_Software;
+ 
+-   type char_array is array (Natural range <>) of aliased Character;
+-   Version_String : char_array (0 .. Ver_Len_Max - 1);
+-   --  Import the C string defined in the (language-independent) source file
+-   --  version.c using the zero-based convention of the C language.
+-   --  The size is not the real one, which does not matter since we will
+-   --  check for the nul character in Gnat_Version_String.
+-   pragma Import (C, Version_String, "version_string");
+-
+    -------------------------
+    -- Gnat_Version_String --
+    -------------------------
+ 
+    function Gnat_Version_String return String is
+-      S : String (1 .. Ver_Len_Max);
+-      Pos : Natural := 0;
+    begin
+-      loop
+-         exit when Version_String (Pos) = ASCII.NUL;
+-
+-         S (Pos + 1) := Version_String (Pos);
+-         Pos := Pos + 1;
+-
+-         exit when Pos = Ver_Len_Max;
+-      end loop;
+-
+-      return S (1 .. Pos);
++      return Gnat_Static_Version_String;
+    end Gnat_Version_String;
+ 
+ end Gnatvsn;