From owner-svn-ports-all@freebsd.org Wed Jun 24 13:32:45 2015 Return-Path: Delivered-To: svn-ports-all@mailman.ysv.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2001:1900:2254:206a::19:1]) by mailman.ysv.freebsd.org (Postfix) with ESMTP id 564D691544E; Wed, 24 Jun 2015 13:32:45 +0000 (UTC) (envelope-from marino@FreeBSD.org) Received: from svn.freebsd.org (svn.freebsd.org [IPv6:2001:1900:2254:2068::e6a:0]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by mx1.freebsd.org (Postfix) with ESMTPS id 467A815BE; Wed, 24 Jun 2015 13:32:45 +0000 (UTC) (envelope-from marino@FreeBSD.org) Received: from svn.freebsd.org ([127.0.1.70]) by svn.freebsd.org (8.14.9/8.14.9) with ESMTP id t5ODWjLK051445; Wed, 24 Jun 2015 13:32:45 GMT (envelope-from marino@FreeBSD.org) Received: (from marino@localhost) by svn.freebsd.org (8.14.9/8.14.9/Submit) id t5ODWgYO051430; Wed, 24 Jun 2015 13:32:42 GMT (envelope-from marino@FreeBSD.org) Message-Id: <201506241332.t5ODWgYO051430@svn.freebsd.org> X-Authentication-Warning: svn.freebsd.org: marino set sender to marino@FreeBSD.org using -f From: John Marino Date: Wed, 24 Jun 2015 13:32:42 +0000 (UTC) To: ports-committers@freebsd.org, svn-ports-all@freebsd.org, svn-ports-head@freebsd.org Subject: svn commit: r390479 - in head: devel/gnatcoll lang lang/spark lang/spark/files X-SVN-Group: ports-head MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-BeenThere: svn-ports-all@freebsd.org X-Mailman-Version: 2.1.20 Precedence: list List-Id: SVN commit messages for the ports tree List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 24 Jun 2015 13:32:45 -0000 Author: marino Date: Wed Jun 24 13:32:41 2015 New Revision: 390479 URL: https://svnweb.freebsd.org/changeset/ports/390479 Log: 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. Added: head/lang/spark/ head/lang/spark/Makefile (contents, props changed) head/lang/spark/distinfo (contents, props changed) head/lang/spark/files/ head/lang/spark/files/patch-gnat2why_get__targ.adb (contents, props changed) head/lang/spark/files/patch-gnat2why_smissing.c (contents, props changed) head/lang/spark/files/patch-gnat2why_spark_spark__definition.adb (contents, props changed) head/lang/spark/files/patch-gnatvsn.adb (contents, props changed) head/lang/spark/pkg-descr (contents, props changed) head/lang/spark/pkg-plist (contents, props changed) Modified: head/devel/gnatcoll/Makefile head/lang/Makefile Modified: head/devel/gnatcoll/Makefile ============================================================================== --- head/devel/gnatcoll/Makefile Wed Jun 24 12:58:58 2015 (r390478) +++ head/devel/gnatcoll/Makefile Wed Jun 24 13:32:41 2015 (r390479) @@ -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:${PORT 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 Modified: head/lang/Makefile ============================================================================== --- head/lang/Makefile Wed Jun 24 12:58:58 2015 (r390478) +++ head/lang/Makefile Wed Jun 24 13:32:41 2015 (r390479) @@ -300,6 +300,7 @@ SUBDIR += smalltalk SUBDIR += smlnj SUBDIR += snobol4 + SUBDIR += spark SUBDIR += spidermonkey17 SUBDIR += spidermonkey170 SUBDIR += spidermonkey185 Added: head/lang/spark/Makefile ============================================================================== --- /dev/null 00:00:00 1970 (empty, because file is newly added) +++ head/lang/spark/Makefile Wed Jun 24 13:32:41 2015 (r390479) @@ -0,0 +1,42 @@ +# Created by: John Marino +# $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 Added: head/lang/spark/distinfo ============================================================================== --- /dev/null 00:00:00 1970 (empty, because file is newly added) +++ head/lang/spark/distinfo Wed Jun 24 13:32:41 2015 (r390479) @@ -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 Added: head/lang/spark/files/patch-gnat2why_get__targ.adb ============================================================================== --- /dev/null 00:00:00 1970 (empty, because file is newly added) +++ head/lang/spark/files/patch-gnat2why_get__targ.adb Wed Jun 24 13:32:41 2015 (r390479) @@ -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; Added: head/lang/spark/files/patch-gnat2why_smissing.c ============================================================================== --- /dev/null 00:00:00 1970 (empty, because file is newly added) +++ head/lang/spark/files/patch-gnat2why_smissing.c Wed Jun 24 13:32:41 2015 (r390479) @@ -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; Added: head/lang/spark/files/patch-gnat2why_spark_spark__definition.adb ============================================================================== --- /dev/null 00:00:00 1970 (empty, because file is newly added) +++ head/lang/spark/files/patch-gnat2why_spark_spark__definition.adb Wed Jun 24 13:32:41 2015 (r390479) @@ -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 | Added: head/lang/spark/files/patch-gnatvsn.adb ============================================================================== --- /dev/null 00:00:00 1970 (empty, because file is newly added) +++ head/lang/spark/files/patch-gnatvsn.adb Wed Jun 24 13:32:41 2015 (r390479) @@ -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; Added: head/lang/spark/pkg-descr ============================================================================== --- /dev/null 00:00:00 1970 (empty, because file is newly added) +++ head/lang/spark/pkg-descr Wed Jun 24 13:32:41 2015 (r390479) @@ -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 Added: head/lang/spark/pkg-plist ============================================================================== --- /dev/null 00:00:00 1970 (empty, because file is newly added) +++ head/lang/spark/pkg-plist Wed Jun 24 13:32:41 2015 (r390479) @@ -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