kpriv/freebsd-ports
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

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

Browse source 
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.
This commit is contained in:
John Marino 2015-06-24 13:32:41 +00:00
parent 54aa710ca1
commit 290da07c50
Notes: svn2git 2021-03-31 03:12:20 +00:00 
svn path=/head/; revision=390479
10 changed files with 272 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
devel/gnatcoll/Makefile
View file

@ -3,6 +3,7 @@
PORTNAME= gnatcoll
PORTVERSION= 2015
PORTREVISION= 1
CATEGORIES= devel
MASTER_SITES= http://downloads.dragonlace.net/src/
DISTNAME= ${PORTNAME}-gpl-${PORTVERSION}-src
@ -16,6 +17,7 @@ BUILD_DEPENDS= gprbuild>=20120510:${PORTSDIR}/devel/gprbuild \
gnat_util>=20140422:${PORTSDIR}/lang/gnat_util
LIB_DEPENDS= libgtkada.so:${PORTSDIR}/x11-toolkits/gtkada3 \
libgmp.so:${PORTSDIR}/math/gmp
RUN_DEPENDS= gnat_util>=20140422:${PORTSDIR}/lang/gnat_util
USES= ada gmake pkgconfig python
USE_GNOME= pygobject3

1
lang/Makefile
View file

@ -300,6 +300,7 @@
SUBDIR += smalltalk
SUBDIR += smlnj
SUBDIR += snobol4
SUBDIR += spark
SUBDIR += spidermonkey17
SUBDIR += spidermonkey170
SUBDIR += spidermonkey185

42
lang/spark/Makefile Normal file
View file

@ -0,0 +1,42 @@
# Created by: John Marino <marino@FreeBSD.org>
# $FreeBSD$
PORTNAME= spark
PORTVERSION= 2014
CATEGORIES= lang
MASTER_SITES= http://downloads.dragonlace.net/src/:main LOCAL/marino:main \
GCC/${MS_SUBDIR}
DISTNAME= spark-gpl-${PORTVERSION}-src
DISTFILES= ${DISTNAME}.tar.gz:main ${IDENTIFICATION}.tar.bz2
EXTRACT_ONLY= ${DISTNAME}.tar.gz
MAINTAINER= marino@FreeBSD.org
COMMENT= Technology for engineering high-reliability s/w applications
LICENSE= GPLv3
BUILD_DEPENDS= gnatcoll>=2014:${PORTSDIR}/devel/gnatcoll
RUN_DEPENDS= gnatwhy3:${PORTSDIR}/math/why3-gpl \
alt-ergo:${PORTSDIR}/math/alt-ergo
USES= ada gmake
ALL_TARGET= gnat2why gnatprove
GNATSRC= ${WRKSRC}/gnat2why/gnat_src
PORTDOCS= html pdf
MAKE_JOBS_UNSAFE= yes
.include "${.CURDIR}/../gcc5-aux/Makefile.version"
post-extract:
(cd ${WRKDIR} && ${TAR} -xf ${DISTDIR}/${IDENTIFICATION}.tar.bz2 \
${IDENTIFICATION}/gcc/ada)
${LN} -s ${WRKDIR}/${IDENTIFICATION}/gcc/ada ${GNATSRC}
${MKDIR} ${WRKSRC}/install/bin
post-install:
${INSTALL_PROGRAM} ${WRKSRC}/install/bin/* ${STAGEDIR}${PREFIX}/bin
(cd ${WRKSRC}/install/share && \
${COPYTREE_SHARE} . ${STAGEDIR}${PREFIX}/share)
.include <bsd.port.mk>

4
lang/spark/distinfo Normal file
View file

@ -0,0 +1,4 @@
SHA256 (spark-gpl-2014-src.tar.gz) = 238c82116346375bde63addf7be6950c700916c80c4362aa15c67b9bd72f134f
SIZE (spark-gpl-2014-src.tar.gz) = 37930303
SHA256 (gcc-5-20150609.tar.bz2) = 9154f0b0c4950cfb6dc802da8a35d02478029923a0c44f8ca963cd7ca9107885
SIZE (gcc-5-20150609.tar.bz2) = 90768076

50
lang/spark/files/patch-gnat2why_get__targ.adb Normal file
View file

@ -0,0 +1,50 @@
--- gnat2why/get_targ.adb.orig 2014-04-10 15:20:35 UTC
+++ gnat2why/get_targ.adb
@@ -99,33 +99,6 @@ package body Get_Targ is
return 64;
end Get_Long_Long_Size;
- --------------------
- -- Get_Float_Size --
- --------------------
-
- function Get_Float_Size return Pos is
- begin
- return 32;
- end Get_Float_Size;
-
- ---------------------
- -- Get_Double_Size --
- ---------------------
-
- function Get_Double_Size return Pos is
- begin
- return 64;
- end Get_Double_Size;
-
- --------------------------
- -- Get_Long_Double_Size --
- --------------------------
-
- function Get_Long_Double_Size return Pos is
- begin
- return 96;
- end Get_Long_Double_Size;
-
----------------------
-- Get_Pointer_Size --
----------------------
@@ -296,4 +269,13 @@ package body Get_Targ is
end if;
end Width_From_Size;
+ ------------------------------
+ -- Get_Back_End_Config_File --
+ ------------------------------
+
+ function Get_Back_End_Config_File return String_Ptr is
+ begin
+ return null;
+ end Get_Back_End_Config_File;
+
end Get_Targ;

18
lang/spark/files/patch-gnat2why_smissing.c Normal file
View file

@ -0,0 +1,18 @@
--- gnat2why/smissing.c.orig 2014-04-10 15:20:38 UTC
+++ gnat2why/smissing.c
@@ -32,6 +32,15 @@
allocation strategy for large objects in certain cases). */
int flag_stack_check = 0;
+/* Controls the balance between GNAT encodings and standard DWARF to
+ emit in the debug information. Useful for DWARF debugging information
+ generation only so not used in SPARK2014 */
+int gnat_encodings = 0;
+
+/* controlled by -fcompare-debug option on gcc, hardcode to 0 based on
+ comment above */
+int flag_compare_debug = 0;
+
/* Originally defined in GCC's toplev.c. */
int optimize = 0;
int optimize_size = 0;

75
lang/spark/files/patch-gnat2why_spark_spark__definition.adb Normal file
View file

@ -0,0 +1,75 @@
--- gnat2why/spark/spark_definition.adb.orig 2014-04-10 15:20:35 UTC
+++ gnat2why/spark/spark_definition.adb
@@ -2989,6 +2989,7 @@ package body SPARK_Definition is
Pragma_Elaborate_All |
Pragma_Elaborate_Body |
Pragma_Export |
+ Pragma_Extensions_Visible |
Pragma_Independent |
Pragma_Independent_Components |
Pragma_Inline |
@@ -3022,8 +3023,10 @@ package body SPARK_Definition is
Pragma_Async_Writers |
Pragma_Contract_Cases |
Pragma_Depends |
+ Pragma_Default_Initial_Condition |
Pragma_Effective_Reads |
Pragma_Effective_Writes |
+ Pragma_Ghost |
Pragma_Global |
Pragma_Initializes |
Pragma_Initial_Condition |
@@ -3050,6 +3053,8 @@ package body SPARK_Definition is
Pragma_Check_Policy |
Pragma_Inline_Always |
Pragma_Linker_Section |
+ Pragma_No_Elaboration_Code_All |
+ Pragma_No_Tagged_Streams |
Pragma_Pure_Function |
Pragma_Restriction_Warnings |
Pragma_Style_Checks |
@@ -3081,7 +3086,6 @@ package body SPARK_Definition is
when Pragma_Abort_Defer |
Pragma_Allow_Integer_Address |
Pragma_Attribute_Definition |
- Pragma_AST_Entry |
Pragma_C_Pass_By_Copy |
Pragma_Check_Float_Overflow |
Pragma_Check_Name |
@@ -3111,7 +3115,6 @@ package body SPARK_Definition is
Pragma_Elaboration_Checks |
Pragma_Eliminate |
Pragma_Enable_Atomic_Synchronization |
- Pragma_Export_Exception |
Pragma_Export_Function |
Pragma_Export_Object |
Pragma_Export_Procedure |
@@ -3124,12 +3127,10 @@ package body SPARK_Definition is
Pragma_Fast_Math |
Pragma_Favor_Top_Level |
Pragma_Finalize_Storage_Only |
- Pragma_Float_Representation |
Pragma_Ident |
Pragma_Implementation_Defined |
Pragma_Implemented |
Pragma_Implicit_Packing |
- Pragma_Import_Exception |
Pragma_Import_Function |
Pragma_Import_Object |
Pragma_Import_Procedure |
@@ -3149,7 +3150,6 @@ package body SPARK_Definition is
Pragma_Linker_Alias |
Pragma_Linker_Constructor |
Pragma_Linker_Destructor |
- Pragma_Long_Float |
Pragma_Loop_Optimize |
Pragma_Machine_Attribute |
Pragma_Main |
@@ -3170,6 +3170,7 @@ package body SPARK_Definition is
Pragma_Post_Class |
Pragma_Pre |
Pragma_Predicate |
+ Pragma_Prefix_Exception_Messages |
Pragma_Pre_Class |
Pragma_Priority_Specific_Dispatching |
Pragma_Profile_Warnings |

36
lang/spark/files/patch-gnatvsn.adb Normal file
View file

@ -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;

23
lang/spark/pkg-descr Normal file
View file

@ -0,0 +1,23 @@
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.
WWW: http://www.spark-2014.org

21
lang/spark/pkg-plist Normal file
View file

@ -0,0 +1,21 @@
bin/gnat2why
bin/gnatprove
bin/spark_report
%%DATADIR%%/config/frames.cgpr
%%DATADIR%%/config/gnat2why.cgpr
%%DATADIR%%/config/why.cgpr
%%DATADIR%%/theories/_gnatprove_standard.mlw
%%DATADIR%%/theories/_gnatprove_standard_th.why
%%DATADIR%%/theories/ada__containers__formal_doubly_linked_lists.mlw
%%DATADIR%%/theories/ada__containers__formal_doubly_linked_lists__generic_sorting.mlw
%%DATADIR%%/theories/ada__containers__formal_hashed_maps.mlw
%%DATADIR%%/theories/ada__containers__formal_hashed_sets.mlw
%%DATADIR%%/theories/ada__containers__formal_hashed_sets__generic_keys.mlw
%%DATADIR%%/theories/ada__containers__formal_ordered_maps.mlw
%%DATADIR%%/theories/ada__containers__formal_ordered_sets.mlw
%%DATADIR%%/theories/ada__containers__formal_ordered_sets__generic_keys.mlw
%%DATADIR%%/theories/ada__containers__formal_vectors.mlw
%%DATADIR%%/theories/ada__containers__formal_vectors__generic_sorting.mlw
%%DATADIR%%/theories/ada__model.mlw
%%DATADIR%%/theories/ada__model_th.why
%%DATADIR%%/theories/integers.why