Index: head/devel/gnatcoll/Makefile =================================================================== --- head/devel/gnatcoll/Makefile (revision 390478) +++ head/devel/gnatcoll/Makefile (revision 390479) @@ -1,89 +1,91 @@ # Created by: John Marino # $FreeBSD$ PORTNAME= gnatcoll PORTVERSION= 2015 +PORTREVISION= 1 CATEGORIES= devel MASTER_SITES= http://downloads.dragonlace.net/src/ DISTNAME= ${PORTNAME}-gpl-${PORTVERSION}-src MAINTAINER= marino@FreeBSD.org COMMENT= GNAT Component Collection from Adacore LICENSE= GPLv3 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 PYCOMPILE= ${PREFIX}/lib/${PYTHON_VERSION}/compileall.py GNU_CONFIGURE= yes PORTDOCS= html gnatcoll.pdf PORTEXAMPLES= * MAKE_ARGS= PROCESSORS=${MAKE_JOBS_NUMBER} \ Gnatcoll_Build=Production OPTIONS_DEFINE= READLINE SYSLOG PGSQL ICONV DOCS EXAMPLES OPTIONS_DEFAULT= READLINE SYSLOG OPTIONS_SUB= yes DOCS_BUILD_DEPENDS= sphinx-build:${PORTSDIR}/textproc/py-sphinx SYSLOG_CONFIGURE_ENABLE= syslog CONFIGURE_TARGET= ${ARCH:S/amd64/x86_64/}-aux-${OPSYS:tl}${OSREL} CONFIGURE_ARGS= --with-gmp=${PREFIX} \ --with-sqlite=embedded \ --with-python=${PREFIX} \ --with-gtk=3.0 \ --enable-pygobject \ --disable-shared \ --disable-pygtk .include .if ${PORT_OPTIONS:MREADLINE} USES+= readline:port CONFIGURE_ARGS+= --enable-gpl .else CONFIGURE_ARGS+= --disable-readline .endif .if ${PORT_OPTIONS:MPGSQL} USES+= pgsql CONFIGURE_ARGS+= --with-postgresql=${PREFIX} .else CONFIGURE_ARGS+= --without-postgresql .endif # There might be something wrong with iconv support as seen in GPS crash. # That's why this option is not enabled by default .if ${PORT_OPTIONS:MICONV} USES+= iconv CONFIGURE_ARGS+= --with-iconv=${ICONV_PREFIX} .else CONFIGURE_ARGS+= --without-iconv .endif post-patch: @${REINPLACE_CMD} -e "s|@PREFIX@|${PREFIX}|g" \ ${WRKSRC}/src/gnatcoll_readline.gpr.in .if ! ${PORT_OPTIONS:MDOCS} ${MV} ${WRKSRC}/docs/_build ${WRKSRC}/docs/_hide_build .endif do-build: cd ${WRKSRC} && ${SETENV} ${MAKE_ENV} \ ${MAKE_CMD} ${MAKE_ARGS} ${ALL_TARGET} post-install: ${RM} -r ${STAGEDIR}${DOCSDIR}/html/_sources ${RM} -r ${STAGEDIR}${PREFIX}/share/gps ${RM} -r ${STAGEDIR}${EXAMPLESDIR}/library .if ! ${PORT_OPTIONS:MEXAMPLES} ${RM} -r ${STAGEDIR}${EXAMPLESDIR} .endif .include Index: head/lang/Makefile =================================================================== --- head/lang/Makefile (revision 390478) +++ head/lang/Makefile (revision 390479) @@ -1,341 +1,342 @@ # $FreeBSD$ # COMMENT = Programming languages SUBDIR += Gofer SUBDIR += abcl SUBDIR += adacontrol SUBDIR += afnix SUBDIR += algol68g SUBDIR += alisp SUBDIR += angelscript SUBDIR += arena SUBDIR += asis SUBDIR += asn1c SUBDIR += atlast SUBDIR += ats SUBDIR += awka SUBDIR += bas2tap SUBDIR += basic256 SUBDIR += bf2c SUBDIR += bigloo SUBDIR += bsh SUBDIR += bwbasic SUBDIR += c SUBDIR += ccl SUBDIR += cdent SUBDIR += cduce SUBDIR += ceylon SUBDIR += cfortran SUBDIR += chibi-scheme SUBDIR += chicken SUBDIR += cint SUBDIR += cjs SUBDIR += clang-cheri SUBDIR += clang-devel SUBDIR += clang33 SUBDIR += clang34 SUBDIR += clang35 SUBDIR += clang36 SUBDIR += clojure SUBDIR += clojure-mode.el SUBDIR += cloudabi-clang SUBDIR += cmucl SUBDIR += cmucl-extra SUBDIR += cocor SUBDIR += cparser SUBDIR += csharp-mode.el SUBDIR += cython SUBDIR += diveintopython SUBDIR += dlv SUBDIR += dmd1 SUBDIR += dmd2 SUBDIR += duktape SUBDIR += ecl SUBDIR += elan SUBDIR += elixir SUBDIR += elk SUBDIR += emacs-lisp-intro SUBDIR += erlang SUBDIR += erlang-java SUBDIR += erlang-runtime15 SUBDIR += erlang-runtime16 SUBDIR += erlang-runtime17 SUBDIR += erlang-wx SUBDIR += execline SUBDIR += expect SUBDIR += f2c SUBDIR += fasm SUBDIR += ferite SUBDIR += ficl SUBDIR += fpc SUBDIR += fpc-base SUBDIR += fpc-docs SUBDIR += fpc-lua SUBDIR += fpc-rexx SUBDIR += fpc-tcl SUBDIR += fpc-units SUBDIR += fpc-utils SUBDIR += fsharp SUBDIR += gambit-c SUBDIR += gauche SUBDIR += gawk SUBDIR += gcc SUBDIR += gcc-aux SUBDIR += gcc-ecj45 SUBDIR += gcc46 SUBDIR += gcc47 SUBDIR += gcc48 SUBDIR += gcc49 SUBDIR += gcc5 SUBDIR += gcc5-aux SUBDIR += gcc5-devel SUBDIR += gcc6-devel SUBDIR += gcl SUBDIR += gforth SUBDIR += ghc SUBDIR += gjs SUBDIR += gnat_util SUBDIR += gnatdroid-armv7 SUBDIR += gnatdroid-binutils SUBDIR += gnatdroid-sysroot SUBDIR += gnu-cobol SUBDIR += gnustep-base SUBDIR += go SUBDIR += gprolog SUBDIR += groovy SUBDIR += gscheme SUBDIR += guile SUBDIR += guile2 SUBDIR += harbour SUBDIR += hla SUBDIR += hope SUBDIR += hs-brainfuck SUBDIR += hs-epic SUBDIR += hs-unlambda SUBDIR += huc SUBDIR += hugs SUBDIR += icc SUBDIR += ici SUBDIR += icon SUBDIR += intel2gas SUBDIR += intercal SUBDIR += io SUBDIR += itcl SUBDIR += itcl4 SUBDIR += jakarta-commons-jelly SUBDIR += jimtcl SUBDIR += jruby SUBDIR += js_of_ocaml SUBDIR += jython SUBDIR += kawa SUBDIR += kturtle SUBDIR += lafontaine SUBDIR += lci SUBDIR += libhx SUBDIR += libjit SUBDIR += libobjc2 SUBDIR += librep SUBDIR += libstdc++_stldoc_4.2.2 SUBDIR += linux-c6-tcl85 SUBDIR += linux-f10-libg2c SUBDIR += linux-f10-tcl85 SUBDIR += linux-j SUBDIR += lua-ada SUBDIR += lua-mode.el SUBDIR += lua51 SUBDIR += lua52 SUBDIR += lua53 SUBDIR += luajit SUBDIR += malbolge SUBDIR += maude SUBDIR += mawk SUBDIR += mdk SUBDIR += micropython SUBDIR += mit-scheme SUBDIR += mixal SUBDIR += mlton SUBDIR += mmix SUBDIR += modula3 SUBDIR += mono SUBDIR += mono-basic SUBDIR += moscow_ml SUBDIR += mosh SUBDIR += mtasc SUBDIR += munger SUBDIR += nawk SUBDIR += nbc SUBDIR += nbfc SUBDIR += nesasm SUBDIR += newlisp SUBDIR += newlisp-devel SUBDIR += nhc98 SUBDIR += nickle SUBDIR += nim SUBDIR += nml SUBDIR += nqc SUBDIR += nwcc SUBDIR += nx SUBDIR += ocaml SUBDIR += ocaml-autoconf SUBDIR += ocaml-nox11 SUBDIR += ofc SUBDIR += ohugs SUBDIR += onyx SUBDIR += oo2c SUBDIR += opendylan SUBDIR += p2c SUBDIR += p5-Data-JavaScript SUBDIR += p5-Error SUBDIR += p5-Expect SUBDIR += p5-ExtUtils-F77 SUBDIR += p5-Interpolation SUBDIR += p5-JSAN SUBDIR += p5-JavaScript-SpiderMonkey SUBDIR += p5-JavaScript-Squish SUBDIR += p5-JavaScript-Value-Escape SUBDIR += p5-List-MoreUtils SUBDIR += p5-Marpa SUBDIR += p5-Marpa-PP SUBDIR += p5-Marpa-XS SUBDIR += p5-Modern-Perl SUBDIR += p5-Parse-Perl SUBDIR += p5-Perl6-Subs SUBDIR += p5-Promises SUBDIR += p5-Pugs-Compiler-Rule SUBDIR += p5-Quantum-Superpositions SUBDIR += p5-Scalar-List-Utils SUBDIR += p5-Switch SUBDIR += p5-Tcl SUBDIR += p5-Test-XPath SUBDIR += p5-Try-Tiny SUBDIR += p5-Try-Tiny-Retry SUBDIR += p5-TryCatch SUBDIR += p5-ePerl SUBDIR += p5-signatures SUBDIR += p5-v6 SUBDIR += parrot SUBDIR += pbasic SUBDIR += pcc SUBDIR += pecl-perl SUBDIR += perl5-devel SUBDIR += perl5.16 SUBDIR += perl5.18 SUBDIR += perl5.20 SUBDIR += perl5.22 SUBDIR += petite-chez SUBDIR += pfe SUBDIR += phantomjs SUBDIR += pharo SUBDIR += phc SUBDIR += php-mode.el SUBDIR += php5 SUBDIR += php5-extensions SUBDIR += php55 SUBDIR += php55-extensions SUBDIR += php56 SUBDIR += php56-extensions SUBDIR += php_doc SUBDIR += picoc SUBDIR += pike78 SUBDIR += polyml SUBDIR += ptoc SUBDIR += pure SUBDIR += py-clojure SUBDIR += py-mx-base SUBDIR += py-prolog SUBDIR += pypy SUBDIR += pypy3-devel SUBDIR += python SUBDIR += python-doc-html SUBDIR += python-doc-pdf-a4 SUBDIR += python-doc-pdf-letter SUBDIR += python-doc-text SUBDIR += python-mode.el SUBDIR += python-tools SUBDIR += python2 SUBDIR += python27 SUBDIR += python3 SUBDIR += python32 SUBDIR += python33 SUBDIR += python34 SUBDIR += qore SUBDIR += qscheme SUBDIR += qt5-qml SUBDIR += racket SUBDIR += racket-minimal SUBDIR += ratfor SUBDIR += rexx-imc SUBDIR += rexx-regina SUBDIR += rexx-regutil SUBDIR += rexx-wrapper SUBDIR += rhino SUBDIR += rubinius SUBDIR += ruby20 SUBDIR += ruby21 SUBDIR += ruby22 SUBDIR += runawk SUBDIR += rust SUBDIR += s9fes SUBDIR += sagittarius-scheme SUBDIR += sather-specification SUBDIR += sather-tutorial SUBDIR += sbcl SUBDIR += scala SUBDIR += scala-docs SUBDIR += scheme48 SUBDIR += scm SUBDIR += sdcc SUBDIR += sdcc-devel SUBDIR += see SUBDIR += seed7 SUBDIR += siod SUBDIR += sisc SUBDIR += sketchy SUBDIR += slib SUBDIR += slib-guile SUBDIR += slib-guile2 SUBDIR += slisp SUBDIR += smalltalk SUBDIR += smlnj SUBDIR += snobol4 + SUBDIR += spark SUBDIR += spidermonkey17 SUBDIR += spidermonkey170 SUBDIR += spidermonkey185 SUBDIR += spidermonkey24 SUBDIR += spl SUBDIR += squeak SUBDIR += squirrel SUBDIR += stalin SUBDIR += starlogo SUBDIR += stldoc SUBDIR += swi-pl SUBDIR += tcbasic SUBDIR += tcc SUBDIR += tcl-manual SUBDIR += tcl-wrapper SUBDIR += tcl84 SUBDIR += tcl85 SUBDIR += tcl86 SUBDIR += tclX SUBDIR += tinypy SUBDIR += tolua SUBDIR += tolua++ SUBDIR += tuareg-mode.el SUBDIR += twelf SUBDIR += ucc SUBDIR += urweb SUBDIR += v8 SUBDIR += v8-devel SUBDIR += vala SUBDIR += visualworks SUBDIR += whitespace SUBDIR += x10 SUBDIR += yabasic SUBDIR += yap SUBDIR += yap-devel SUBDIR += yorick SUBDIR += ypsilon .include Index: head/lang/spark/Makefile =================================================================== --- head/lang/spark/Makefile (nonexistent) +++ head/lang/spark/Makefile (revision 390479) @@ -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 Property changes on: head/lang/spark/Makefile ___________________________________________________________________ Added: svn:eol-style ## -0,0 +1 ## +native \ No newline at end of property Added: svn:keywords ## -0,0 +1 ## +FreeBSD=%H \ No newline at end of property Added: svn:mime-type ## -0,0 +1 ## +text/plain \ No newline at end of property Index: head/lang/spark/distinfo =================================================================== --- head/lang/spark/distinfo (nonexistent) +++ head/lang/spark/distinfo (revision 390479) @@ -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 Property changes on: head/lang/spark/distinfo ___________________________________________________________________ Added: fbsd:nokeywords ## -0,0 +1 ## +yes \ No newline at end of property Added: svn:eol-style ## -0,0 +1 ## +native \ No newline at end of property Added: svn:mime-type ## -0,0 +1 ## +text/plain \ No newline at end of property Index: head/lang/spark/files/patch-gnat2why_get__targ.adb =================================================================== --- head/lang/spark/files/patch-gnat2why_get__targ.adb (nonexistent) +++ head/lang/spark/files/patch-gnat2why_get__targ.adb (revision 390479) @@ -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; Property changes on: head/lang/spark/files/patch-gnat2why_get__targ.adb ___________________________________________________________________ Added: fbsd:nokeywords ## -0,0 +1 ## +yes \ No newline at end of property Added: svn:eol-style ## -0,0 +1 ## +native \ No newline at end of property Added: svn:mime-type ## -0,0 +1 ## +text/plain \ No newline at end of property Index: head/lang/spark/files/patch-gnat2why_smissing.c =================================================================== --- head/lang/spark/files/patch-gnat2why_smissing.c (nonexistent) +++ head/lang/spark/files/patch-gnat2why_smissing.c (revision 390479) @@ -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; Property changes on: head/lang/spark/files/patch-gnat2why_smissing.c ___________________________________________________________________ Added: fbsd:nokeywords ## -0,0 +1 ## +yes \ No newline at end of property Added: svn:eol-style ## -0,0 +1 ## +native \ No newline at end of property Added: svn:mime-type ## -0,0 +1 ## +text/plain \ No newline at end of property Index: head/lang/spark/files/patch-gnat2why_spark_spark__definition.adb =================================================================== --- head/lang/spark/files/patch-gnat2why_spark_spark__definition.adb (nonexistent) +++ head/lang/spark/files/patch-gnat2why_spark_spark__definition.adb (revision 390479) @@ -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 | Property changes on: head/lang/spark/files/patch-gnat2why_spark_spark__definition.adb ___________________________________________________________________ Added: fbsd:nokeywords ## -0,0 +1 ## +yes \ No newline at end of property Added: svn:eol-style ## -0,0 +1 ## +native \ No newline at end of property Added: svn:mime-type ## -0,0 +1 ## +text/plain \ No newline at end of property Index: head/lang/spark/files/patch-gnatvsn.adb =================================================================== --- head/lang/spark/files/patch-gnatvsn.adb (nonexistent) +++ head/lang/spark/files/patch-gnatvsn.adb (revision 390479) @@ -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; Property changes on: head/lang/spark/files/patch-gnatvsn.adb ___________________________________________________________________ Added: fbsd:nokeywords ## -0,0 +1 ## +yes \ No newline at end of property Added: svn:eol-style ## -0,0 +1 ## +native \ No newline at end of property Added: svn:mime-type ## -0,0 +1 ## +text/plain \ No newline at end of property Index: head/lang/spark/pkg-descr =================================================================== --- head/lang/spark/pkg-descr (nonexistent) +++ head/lang/spark/pkg-descr (revision 390479) @@ -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 Property changes on: head/lang/spark/pkg-descr ___________________________________________________________________ Added: fbsd:nokeywords ## -0,0 +1 ## +yes \ No newline at end of property Added: svn:eol-style ## -0,0 +1 ## +native \ No newline at end of property Added: svn:mime-type ## -0,0 +1 ## +text/plain \ No newline at end of property Index: head/lang/spark/pkg-plist =================================================================== --- head/lang/spark/pkg-plist (nonexistent) +++ head/lang/spark/pkg-plist (revision 390479) @@ -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 Property changes on: head/lang/spark/pkg-plist ___________________________________________________________________ Added: fbsd:nokeywords ## -0,0 +1 ## +yes \ No newline at end of property Added: svn:eol-style ## -0,0 +1 ## +native \ No newline at end of property Added: svn:mime-type ## -0,0 +1 ## +text/plain \ No newline at end of property