Package: spark
Severity: wishlist
Tags: patch
Hello.
A rebuild of spark against gnat-6 will soon be necessary anyway.
Instead of triggering a binNMU, please consider uploading an updated
debian package including the attached changes.
>From 91be63df791f158370234518b8621c6e91b91501 Mon Sep 17 00:00:00 2001
From: Nicolas Boulenguez <nicolas.bouleng...@free.fr>
Date: Sun, 31 Jul 2016 12:41:49 +0200
Subject: [PATCH 1/6] Fix short description style.
---
debian/control | 2 +-
debian/spark.lintian-overrides | 1 -
2 files changed, 1 insertion(+), 2 deletions(-)
delete mode 100644 debian/spark.lintian-overrides
diff --git a/debian/control b/debian/control
index 160cd2f..d7f07e5 100644
--- a/debian/control
+++ b/debian/control
@@ -12,7 +12,7 @@ Package: spark
Architecture: any
Depends: ${shlibs:Depends}, ${misc:Depends}, ${swi-prolog:Depends}, swi-prolog-nox
Suggests: gnat, alt-ergo
-Description: SPARK programming language toolset
+Description: check formal properties of programs in the SPARK/Ada language
SPARK is a formally-defined computer programming language based on the
Ada programming language, intended to be secure and to support the
development of high integrity software used in applications and systems
diff --git a/debian/spark.lintian-overrides b/debian/spark.lintian-overrides
deleted file mode 100644
index e4e6d16..0000000
--- a/debian/spark.lintian-overrides
+++ /dev/null
@@ -1 +0,0 @@
-spark: description-starts-with-package-name
--
2.8.1
>From da20106edf3cac520613f739256a33cdf5277da4 Mon Sep 17 00:00:00 2001
From: Nicolas Boulenguez <nicolas.bouleng...@free.fr>
Date: Sun, 31 Jul 2016 13:48:53 +0200
Subject: [PATCH 2/6] Documentation: add manpages and Victor manual.
---
debian/copyright | 4 +++
debian/man/sparkclean.1 | 62 ++++++++++++++++++++++++++++++++++++++++
debian/man/vct.1 | 66 +++++++++++++++++++++++++++++++++++++++++++
debian/man/wrap_utility.1 | 43 ++++++++++++++++++++++++++++
debian/spark.doc-base.vct-man | 9 ++++++
debian/spark.docs | 1 +
debian/spark.manpages | 10 +------
7 files changed, 186 insertions(+), 9 deletions(-)
create mode 100644 debian/man/sparkclean.1
create mode 100644 debian/man/vct.1
create mode 100644 debian/man/wrap_utility.1
create mode 100644 debian/spark.doc-base.vct-man
create mode 100644 debian/spark.docs
diff --git a/debian/copyright b/debian/copyright
index bdb59ec..6bbbaca 100644
--- a/debian/copyright
+++ b/debian/copyright
@@ -28,7 +28,11 @@ Copyright: 2011 Florian Schanda <florian.scha...@altran-praxis.com>
License: GFDL-1.3+
Files: debian/man/checker.1
+ debian/man/sparkclean.1
+ debian/man/vct.1
+ debian/man/wrap_utility.1
Copyright: 2011 Eugeniy Meshcheryakov <eu...@debian.org>
+ 2016 Nicolas Boulenguez <nico...@debian.org>
License: GPL-3.0+ or GFDL-1.3+
License: GPL-3.0+
diff --git a/debian/man/sparkclean.1 b/debian/man/sparkclean.1
new file mode 100644
index 0000000..87c1a96
--- /dev/null
+++ b/debian/man/sparkclean.1
@@ -0,0 +1,62 @@
+.\" Man page for sparkclean.
+.\"
+.\" Copyright (C) 2016 Nicolas Boulenguez <nico...@debian.org>
+
+.\" Permission is granted to copy, distribute and/or modify this document
+.\" under the terms of the GNU General Public License version 3,
+.\" or (at your option) the GNU Free Documentation License Version 1.3
+.\" with no Invariant Sections, no Front-Cover Texts and no Back-Cover
+.\" Texts,
+.\" or (at your option) any later version published by the Free Software
+.\" Foundation.
+
+.TH sparkclean 1 "2016-07-30"
+
+.SH NAME
+sparkclean \- delete files generated by the SPARK tools
+
+.SH SYNOPSIS
+.B sparkclean
+.RB [\| \-examiner \|]
+.RB [\| \-simplifier \|]
+.RB [\| \-victor \|]
+.RB [\| \-pogs \|]
+
+.SH DESCRIPTION
+Automatically delete files generated by the SPARK tools.
+
+.SH OPTIONS
+.TP
+.BR \-examiner
+delete VCs, DPCs and reports/listings
+.TP
+.BR \-simplifier
+delete simplified VCs and DPCs
+.TP
+.BR \-victor
+delete victor proof logs
+.TP
+.BR \-pogs
+delete pogs summary files
+.TP
+With no OPTION given, all files generated by the SPARK tools will be deleted.
+
+.SH "SEE ALSO"
+.RI "the VICTOR reference manual" /usr/share/doc/spark/vct-man.pdf ,
+.BR checker (1),
+.BR pogs (1),
+.BR spadesimp (1),
+.BR spark (1),
+.BR sparkformat (1),
+.BR sparkmake (1),
+.BR sparksimp (1),
+.BR vct (1),
+.BR victor (1),
+.BR wrap_utility (1),
+.BR zombiescope (1).
+
+.SH AUTHORS
+This manual page was written by
+Nicolas Boulenguez <nico...@debian.org>
+for the
+.I "Debian GNU/Linux" .
diff --git a/debian/man/vct.1 b/debian/man/vct.1
new file mode 100644
index 0000000..4e49c0b
--- /dev/null
+++ b/debian/man/vct.1
@@ -0,0 +1,66 @@
+.\" Man page for vct.
+.\"
+.\" Copyright (C) 2016 Nicolas Boulenguez <nico...@debian.org>
+
+.\" Permission is granted to copy, distribute and/or modify this document
+.\" under the terms of the GNU General Public License version 3,
+.\" or (at your option) the GNU Free Documentation License Version 1.3
+.\" with no Invariant Sections, no Front-Cover Texts and no Back-Cover
+.\" Texts,
+.\" or (at your option) any later version published by the Free Software
+.\" Foundation.
+
+.TH vct 1 "2016-07-30"
+
+.SH NAME
+vct \- SPARK verification condition translator and prover driver
+
+.SH SYNOPSIS
+.B vct
+.RB [\| options \|]
+.RB [\| unitname \|]
+
+.SH DESCRIPTION
+SPARK tool driving external provers like Alt-Ergo, CvC3, Yices or Z3.
+
+.SH OPTIONS
+The
+.B unitname
+argument is used to identify a single unit on which to run Victor.
+
+To run Victor on multiple units, omit the
+.B unitname
+argument and use instead the
+.B units
+option to specify a unit listing input file.
+
+If both a
+.B unitname
+and a
+.B units
+option are provided, the
+.B units
+option is ignored.
+
+Victor takes numerous options, many of which are currently necessary.
+Please find more information in the manual.
+
+.SH "SEE ALSO"
+.RI "the VICTOR reference manual" /usr/share/doc/spark/vct-man.pdf ,
+.BR checker (1),
+.BR pogs (1),
+.BR spadesimp (1),
+.BR spark (1),
+.BR sparkclean (1),
+.BR sparkformat (1),
+.BR sparkmake (1),
+.BR sparksimp (1),
+.BR victor (1),
+.BR wrap_utility (1),
+.BR zombiescope (1).
+
+.SH AUTHORS
+This manual page was written by
+Nicolas Boulenguez <nico...@debian.org>
+for the
+.IR "Debian GNU/Linux" .
diff --git a/debian/man/wrap_utility.1 b/debian/man/wrap_utility.1
new file mode 100644
index 0000000..f469873
--- /dev/null
+++ b/debian/man/wrap_utility.1
@@ -0,0 +1,43 @@
+.\" Man page for wrap_utility.
+.\"
+.\" Copyright (C) 2016 Nicolas Boulenguez <nico...@debian.org>
+
+.\" Permission is granted to copy, distribute and/or modify this document
+.\" under the terms of the GNU General Public License version 3,
+.\" or (at your option) the GNU Free Documentation License Version 1.3
+.\" with no Invariant Sections, no Front-Cover Texts and no Back-Cover
+.\" Texts,
+.\" or (at your option) any later version published by the Free Software
+.\" Foundation.
+
+.TH wrap_utility 1 "2016-07-30"
+
+.SH NAME
+wrap_utility \- helper formatting tool for the SPARK toolset
+
+.SH SYNOPSIS
+.B wrap_utility
+.RB [\| source \|[\| destination \|]\|]
+
+.SH DESCRIPTION
+Wrap long lines in intermediate files used by SPARK.
+
+.SH "SEE ALSO"
+.RI "the VICTOR reference manual" /usr/share/doc/spark/vct-man.pdf ,
+.BR checker (1),
+.BR pogs (1),
+.BR spadesimp (1),
+.BR spark (1),
+.BR sparkclean (1),
+.BR sparkformat (1),
+.BR sparkmake (1),
+.BR sparksimp (1),
+.BR vct (1),
+.BR victor (1),
+.BR zombiescope (1).
+
+.SH AUTHORS
+This manual page was written by
+Nicolas Boulenguez <nico...@debian.org>
+for the
+.IR "Debian GNU/Linux" .
diff --git a/debian/spark.doc-base.vct-man b/debian/spark.doc-base.vct-man
new file mode 100644
index 0000000..4d06772
--- /dev/null
+++ b/debian/spark.doc-base.vct-man
@@ -0,0 +1,9 @@
+Document: vct-man
+Title: Reference manual for the Victor prover driver.
+Author: Paul Jackson <p...@inf.ed.ac.uk>
+Abstract: Victor extracts verification conditions from source code,
+ translate them and attempts to check them with external provers.
+Section: Programming
+
+Format: PDF
+Files: /usr/share/doc/spark/vct-man.pdf.gz
diff --git a/debian/spark.docs b/debian/spark.docs
new file mode 100644
index 0000000..dea32d8
--- /dev/null
+++ b/debian/spark.docs
@@ -0,0 +1 @@
+victor/vct/doc/vct-man.pdf
diff --git a/debian/spark.manpages b/debian/spark.manpages
index 692fe8d..19f429f 100644
--- a/debian/spark.manpages
+++ b/debian/spark.manpages
@@ -1,9 +1 @@
-debian/man/pogs.1
-debian/man/spadesimp.1
-debian/man/spark.1
-debian/man/sparkformat.1
-debian/man/sparkmake.1
-debian/man/sparksimp.1
-debian/man/victor.1
-debian/man/zombiescope.1
-debian/man/checker.1
+debian/man/*
--
2.8.1
>From 77e85bde26012fd08eb8a599a263399f116992c2 Mon Sep 17 00:00:00 2001
From: Nicolas Boulenguez <nicolas.bouleng...@free.fr>
Date: Sun, 31 Jul 2016 13:51:59 +0200
Subject: [PATCH 3/6] Patch fixing typos.
---
debian/man/victor.1 | 2 +-
debian/patches/series | 1 +
debian/patches/typos.diff | 273 ++++++++++++++++++++++++++++++++++++++++++++++
3 files changed, 275 insertions(+), 1 deletion(-)
create mode 100644 debian/patches/typos.diff
diff --git a/debian/man/victor.1 b/debian/man/victor.1
index b688314..d420790 100644
--- a/debian/man/victor.1
+++ b/debian/man/victor.1
@@ -60,7 +60,7 @@ first attempt to process foo.siv and then fall back to
foo.vcg.
.TP
\*(T<\fB\-plain\fR\*(T>
-Plain mode \[em] supress timings and versions.
+Plain mode \[em] suppress timings and versions.
.TP
\*(T<\fB\-solver=\fR\*(T>\fISOLVER\fR
Specifies an alternative SMT solver. By default we use
diff --git a/debian/patches/series b/debian/patches/series
index 4c64520..579b695 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -34,3 +34,4 @@ ada-link-env-flags.diff
swi-prolog-settings-module-conflict.pro
vct-bison-3-fix.diff
victor-quote-cppflags.diff
+typos.diff
diff --git a/debian/patches/typos.diff b/debian/patches/typos.diff
new file mode 100644
index 0000000..9b6dd26
--- /dev/null
+++ b/debian/patches/typos.diff
@@ -0,0 +1,273 @@
+Description: fix various typos detected by Lintian.
+Author: Nicolas Boulenguez <nico...@debian.org>
+
+--- a/examiner/dag-buildexpndag.adb
++++ b/examiner/dag-buildexpndag.adb
+@@ -2474,7 +2474,7 @@
+ -- Identifier and Selected Components --
+ ---------------------------------------------------------------------
+
+- -- Called whenever an identifer is encountered in the expression
++ -- Called whenever an identifier is encountered in the expression
+ -- An identifier appears in many places in the grammar. It is paricularly
+ -- interesting if it is a variable, a type mark or a function call.
+ -- If it is a function call the procedure Setup_Function_Call establishes
+--- a/examiner/dag_io.ads
++++ b/examiner/dag_io.ads
+@@ -49,7 +49,7 @@
+ -- is also used in Declarations to produce the declaration
+ -- of this constant, so it is declared here once.
+ -- The name is chosen so that it cannot clash with any
+- -- legal user-defined identifer.
++ -- legal user-defined identifier.
+ ----------------------------------------------------------------
+ Null_String_Literal_Name : constant String := "null__string";
+
+--- a/examiner/errorhandler-conversions-tostring-semanticerr.adb
++++ b/examiner/errorhandler-conversions-tostring-semanticerr.adb
+@@ -2336,7 +2336,7 @@
+ E_Strings.Append_String (E_Str => E_Str,
+ Str => "Attributes are not permitted in a String concatenation expression");
+ --! Character attributes such as 'Val, 'Pos, 'Succ and 'Pred are not
+- --! permitted below a concatentation operator in a String expression.
++ --! permitted below a concatenation operator in a String expression.
+
+ when 425 =>
+ E_Strings.Append_String (E_Str => E_Str,
+@@ -3499,7 +3499,7 @@
+
+ when 757 =>
+ E_Strings.Append_String (E_Str => E_Str,
+- Str => "The identifer ");
++ Str => "The identifier ");
+ Append_Name (E_Str => E_Str,
+ Name => Err_Num.Name1,
+ Scope => Err_Num.Scope);
+@@ -3776,7 +3776,7 @@
+ E_Strings.Append_String
+ (E_Str => E_Str,
+ Str => "The only allowed values of Default_Bit_Order are Low_Order_First and High_Order_First");
+- --! System.Bit_Order is implicity declared in package System when a configuration
++ --! System.Bit_Order is implicitly declared in package System when a configuration
+ --! file is given. This is an enumeration type with only two literals
+ --! Low_Order_First and High_Order_First
+
+--- a/examiner/errors.htm
++++ b/examiner/errors.htm
+@@ -1924,7 +1924,7 @@
+ </p>
+ <p>
+ <i>
+- Character attributes such as 'Val, 'Pos, 'Succ and 'Pred are not permitted below a concatentation operator in a String expression.
++ Character attributes such as 'Val, 'Pos, 'Succ and 'Pred are not permitted below a concatenation operator in a String expression.
+ </i>
+ </p>
+ <a name="semantic-425"></a>
+@@ -2750,7 +2750,7 @@
+ </p>
+ <a name="semantic-757"></a>
+ <p>
+-*** Semantic Error : 757 : The identifer XXX is either undeclared or not visible at this point. A record field name cannot be the same as its indicated type.
++*** Semantic Error : 757 : The identifier XXX is either undeclared or not visible at this point. A record field name cannot be the same as its indicated type.
+ </p>
+ <a name="semantic-770"></a>
+ <p>
+@@ -3036,7 +3036,7 @@
+ </p>
+ <p>
+ <i>
+- System.Bit_Order is implicity declared in package System when a configuration file is given. This is an enumeration type with only two literals Low_Order_First and High_Order_First.
++ System.Bit_Order is implicitly declared in package System when a configuration file is given. This is an enumeration type with only two literals Low_Order_First and High_Order_First.
+ </i>
+ </p>
+ <a name="semantic-820"></a>
+--- a/examiner/sem-wf_basic_declarative_item.adb
++++ b/examiner/sem-wf_basic_declarative_item.adb
+@@ -1161,7 +1161,7 @@
+
+ -------------------------------------------------------------------------
+ -- Name_Node - Node naming a variable, or a (sub) field of a variable
+- -- Entire_Sym - Symbol of entire variable (ie, first identifer found)
++ -- Entire_Sym - Symbol of entire variable (ie, first identifier found)
+ -- Object_Sym - Symbol of right most element (ie, the variable or
+ -- subcomponent to be marked)
+ -- == NullSymbol if anything goes wrong
+--- a/lib/spark/errors.htm
++++ b/lib/spark/errors.htm
+@@ -1924,7 +1924,7 @@
+ </p>
+ <p>
+ <i>
+- Character attributes such as 'Val, 'Pos, 'Succ and 'Pred are not permitted below a concatentation operator in a String expression.
++ Character attributes such as 'Val, 'Pos, 'Succ and 'Pred are not permitted below a concatenation operator in a String expression.
+ </i>
+ </p>
+ <a name="semantic-425"></a>
+@@ -2750,7 +2750,7 @@
+ </p>
+ <a name="semantic-757"></a>
+ <p>
+-*** Semantic Error : 757 : The identifer XXX is either undeclared or not visible at this point. A record field name cannot be the same as its indicated type.
++*** Semantic Error : 757 : The identifier XXX is either undeclared or not visible at this point. A record field name cannot be the same as its indicated type.
+ </p>
+ <a name="semantic-770"></a>
+ <p>
+@@ -3036,7 +3036,7 @@
+ </p>
+ <p>
+ <i>
+- System.Bit_Order is implicity declared in package System when a configuration file is given. This is an enumeration type with only two literals Low_Order_First and High_Order_First.
++ System.Bit_Order is implicitly declared in package System when a configuration file is given. This is an enumeration type with only two literals Low_Order_First and High_Order_First.
+ </i>
+ </p>
+ <a name="semantic-820"></a>
+--- a/examiner/errorhandler-conversions-tostring-semanticerr-semanticerrexpl.adb
++++ b/examiner/errorhandler-conversions-tostring-semanticerr-semanticerrexpl.adb
+@@ -1093,7 +1093,7 @@
+ E_Strings.Append_String
+ (E_Str => E_Str,
+ Str => "Character attributes such as 'Val, 'Pos, 'Succ and 'Pred are not" &
+- " permitted below a concatentation operator in a String expression.");
++ " permitted below a concatenation operator in a String expression.");
+ when 425 =>
+ E_Strings.Append_String
+ (E_Str => E_Str,
+@@ -1789,7 +1789,7 @@
+ when 815 =>
+ E_Strings.Append_String
+ (E_Str => E_Str,
+- Str => "System.Bit_Order is implicity declared in package System when a configuration" &
++ Str => "System.Bit_Order is implicitly declared in package System when a configuration" &
+ " file is given. This is an enumeration type with only two literals" &
+ " Low_Order_First and High_Order_First");
+ when 820 =>
+--- a/examiner/errorhandler.adb
++++ b/examiner/errorhandler.adb
+@@ -2397,7 +2397,7 @@
+ elsif Err_Num = 394 and then WarningStatus.Is_Suppressed (The_Element => Unuseable_Private_Types) then
+ Inc_Suppressed_Warning_Counter (Warning_Type => Unuseable_Private_Types);
+
+- -- following two separate warnings share the same supression key word
++ -- following two separate warnings share the same suppression key word
+ elsif Err_Num = 396
+ and then -- non-moded variable with address clause
+ WarningStatus.Is_Suppressed (The_Element => Unexpected_Address_Clauses) then
+--- a/examiner/sem-walk_expression_p-wf_expression.adb
++++ b/examiner/sem-walk_expression_p-wf_expression.adb
+@@ -275,7 +275,7 @@
+ or else Right.Errors_In_Expression;
+
+ -- OtherSymbol may carry a function symbol in the case of uses of unchecked_conversion.
+- -- This symbol is used (by wf_Assign) to convery information to the VCG to supress
++ -- This symbol is used (by wf_Assign) to convery information to the VCG to suppress
+ -- checks when an unchecked_conversion is assigned to something of the same subtype.
+ -- We do not want this mechanism if the unchecked_conversion is sued in any other context
+ -- than a direct assignment. Therefore we clear OtherSymbol here:
+--- a/examiner/sem-walk_expression_p-wf_factor.adb
++++ b/examiner/sem-walk_expression_p-wf_factor.adb
+@@ -299,7 +299,7 @@
+ end if;
+
+ -- OtherSymbol may carry a function symbol in the case of uses of unchecked_conversion.
+- -- This symbol is used (by wf_Assign) to convery information to the VCG to supress
++ -- This symbol is used (by wf_Assign) to convery information to the VCG to suppress
+ -- checks when an unchecked_conversion is assigned to something of the same subtype.
+ -- We do not want this mechanism if the unchecked_conversion is used in any other context
+ -- than a direct assignment. Therefore we clear OtherSymbol here:
+@@ -436,7 +436,7 @@
+ or else Right.Errors_In_Expression;
+
+ -- OtherSymbol may carry a function symbol in the case of uses of unchecked_conversion.
+- -- This symbol is used (by wf_Assign) to convery information to the VCG to supress
++ -- This symbol is used (by wf_Assign) to convery information to the VCG to suppress
+ -- checks when an unchecked_conversion is assigned to something of the same subtype.
+ -- We do not want this mechanism if the unchecked_conversion is sued in any other context
+ -- than a direct assignment. Therefore we clear OtherSymbol here:
+--- a/examiner/sem-walk_expression_p-wf_relation.adb
++++ b/examiner/sem-walk_expression_p-wf_relation.adb
+@@ -480,7 +480,7 @@
+ end if;
+
+ -- OtherSymbol may carry a function symbol in the case of uses of unchecked_conversion.
+- -- This symbol is used (by wf_Assign) to convery information to the VCG to supress
++ -- This symbol is used (by wf_Assign) to convery information to the VCG to suppress
+ -- checks when an unchecked_conversion is assigned to something of the same subtype.
+ -- We do not want this mechanism if the unchecked_conversion is sued in any other context
+ -- than a direct assignment. Therefore we clear OtherSymbol here:
+--- a/examiner/sem-walk_expression_p-wf_simple_expression.adb
++++ b/examiner/sem-walk_expression_p-wf_simple_expression.adb
+@@ -301,7 +301,7 @@
+ or else Right.Errors_In_Expression;
+
+ -- OtherSymbol may carry a function symbol in the case of uses of unchecked_conversion.
+- -- This symbol is used (by Wf_Assign) to convery information to the VCG to supress
++ -- This symbol is used (by Wf_Assign) to convery information to the VCG to suppress
+ -- checks when an unchecked_conversion is assigned to something of the same subtype.
+ -- We do not want this mechanism if the unchecked_conversion is sued in any other context
+ -- than a direct assignment. Therefore we clear OtherSymbol here:
+--- a/examiner/sem-walk_expression_p-wf_simple_expression_opt.adb
++++ b/examiner/sem-walk_expression_p-wf_simple_expression_opt.adb
+@@ -234,7 +234,7 @@
+ end if;
+
+ -- OtherSymbol may carry a function symbol in the case of uses of unchecked_conversion.
+- -- This symbol is used (by wf_Assign) to convery information to the VCG to supress
++ -- This symbol is used (by wf_Assign) to convery information to the VCG to suppress
+ -- checks when an unchecked_conversion is assigned to something of the same subtype.
+ -- We do not want this mechanism if the unchecked_conversion is sued in any other context
+ -- than a direct assignment. Therefore we clear OtherSymbol here:
+--- a/examiner/sem-walk_expression_p-wf_term.adb
++++ b/examiner/sem-walk_expression_p-wf_term.adb
+@@ -142,7 +142,7 @@
+ or else Left.Errors_In_Expression
+ or else Right.Errors_In_Expression;
+ -- OtherSymbol may carry a function symbol in the case of uses of unchecked_conversion.
+- -- This symbol is used (by Wf_Assign) to convery information to the VCG to supress
++ -- This symbol is used (by Wf_Assign) to convery information to the VCG to suppress
+ -- checks when an unchecked_conversion is assigned to something of the same subtype.
+ -- We do not want this mechanism if the unchecked_conversion is sued in any other context
+ -- than a direct assignment. Therefore we clear OtherSymbol here:
+--- a/examiner/sem-wf_generic_subprogram_instantiation-wf_generic_actual_part.adb
++++ b/examiner/sem-wf_generic_subprogram_instantiation-wf_generic_actual_part.adb
+@@ -444,7 +444,7 @@
+ Error_Found := True;
+ else
+ -- Fundamentally ok to add
+- -- mark any errors (both to avoid use of invalid instantiation and to supress rule generation)
++ -- mark any errors (both to avoid use of invalid instantiation and to suppress rule generation)
+ if Exp_Result.Errors_In_Expression then
+ Error_Found := True;
+ end if;
+--- a/examiner/sem-wf_package_declaration.adb
++++ b/examiner/sem-wf_package_declaration.adb
+@@ -254,7 +254,7 @@
+ Child_Sym => Pack_Sym,
+ Child_Str => Ident_Str);
+ end if;
+- -- if Pack_Sym is null then something went wrong when we added the child so we need to supress
++ -- if Pack_Sym is null then something went wrong when we added the child so we need to suppress
+ -- any further analysis of the package specification
+ Valid_Name := not Dictionary.Is_Null_Symbol (Pack_Sym);
+ else
+--- a/victor_wrapper/banner.adb
++++ b/victor_wrapper/banner.adb
+@@ -83,7 +83,7 @@
+ Put_Line ("OPTIONS can be one or more of the below:");
+ Put_Line (" -h / -help Show this help message.");
+ Put_Line (" -v Ignore .siv files and only use .vcg files.");
+- Put_Line (" -plain Plain mode - supress timings and versions.");
++ Put_Line (" -plain Plain mode - suppress timings and versions.");
+ Put_Line (" -nouserrules Do not use user rules.");
+ Put_Line (" -keep Keep intermediate SMT files in the current directory.");
+
+--- a/examiner/dictionary.adb
++++ b/examiner/dictionary.adb
+@@ -10837,7 +10837,7 @@
+ Result := SLI_Unknown_Type;
+ SystemErrors.Fatal_Error
+ (Sys_Err => SystemErrors.Other_Internal_Error,
+- Msg => "DICTIONARY.GET_TYPE_DISCRIMINANT : PROGRAM ERRROR");
++ Msg => "DICTIONARY.GET_TYPE_DISCRIMINANT : PROGRAM ERROR");
+ end case;
+ end Get_Type_Discriminant;
+
--
2.8.1
>From 8d2103f7f129cdf5195eb2b6b3e1b62c4896c84a Mon Sep 17 00:00:00 2001
From: Nicolas Boulenguez <nicolas.bouleng...@free.fr>
Date: Sun, 31 Jul 2016 14:09:43 +0200
Subject: [PATCH 4/6] Standards-Version: 3.9.8 (no changes).
---
debian/control | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/debian/control b/debian/control
index d7f07e5..f6c8948 100644
--- a/debian/control
+++ b/debian/control
@@ -3,7 +3,7 @@ Section: devel
Priority: optional
Maintainer: Євгеній Мещеряков <eu...@debian.org>
Build-Depends: debhelper (>= 9), gnat, swi-prolog-nox (>= 6.2.6-2~), libgmp-dev (>= 2:5.0.1+dfsg-7~), bison, flex
-Standards-Version: 3.9.6
+Standards-Version: 3.9.8
Homepage: http://libre.adacore.com/libre/tools/spark-gpl-edition/
Vcs-Git: git://anonscm.debian.org/collab-maint/spark.git
Vcs-Browser: https://anonscm.debian.org/cgit/collab-maint/spark.git
--
2.8.1
>From 8028dce0d66494465b84c0feefed1a7df007d6a1 Mon Sep 17 00:00:00 2001
From: Nicolas Boulenguez <nicolas.bouleng...@free.fr>
Date: Sun, 31 Jul 2016 19:55:12 +0200
Subject: [PATCH 5/6] Clarify data flow of build flags. Make data flow explicit
with command-line variables instead of exports. Patch upstream Makefiles when
they overwrite usual variables. * ada-use-evn-optflags,
victor-use-env-opt-flags, ada-link-env-flags: merged into buildflags.diff.
Most of ada-link-env-flags is done globally via GNATMAKE_OPTS. *
debian-architecture-detect, examiner-architecture-bits: a command-line Make
variable is more simple and portable. * victore-gmpxx-as-needed: --as-needed
now activated by debian_packaging.mk. * checker-makefile, no-alt-ergo,
no-static-gmp: diff indexes affected by other changes. * Let
/u/s/dpkg/default.mk, /u/s/ada/debian_packaging.mk set variable values. *
Enable all hardening flags.
Declare phony targets in debian/rules.
---
debian/control | 7 +-
debian/patches/ada-link-env-flags.diff | 129 -------------------------
debian/patches/ada-use-evn-optflags.diff | 16 ---
debian/patches/buildflags.diff | 74 ++++++++++++++
debian/patches/checker-makefile.diff | 2 +-
debian/patches/debian-architecture-detect.diff | 26 -----
debian/patches/examiner-architecture-bits.diff | 17 ----
debian/patches/no-alt-ergo.diff | 2 +-
debian/patches/series | 7 +-
debian/patches/victor-gmpxx-as-needed.diff | 15 ---
debian/patches/victor-no-static-gmp.diff | 4 +-
debian/patches/victor-use-env-opt-flags.diff | 38 --------
debian/rules | 46 ++++-----
13 files changed, 109 insertions(+), 274 deletions(-)
delete mode 100644 debian/patches/ada-link-env-flags.diff
delete mode 100644 debian/patches/ada-use-evn-optflags.diff
create mode 100644 debian/patches/buildflags.diff
delete mode 100644 debian/patches/debian-architecture-detect.diff
delete mode 100644 debian/patches/examiner-architecture-bits.diff
delete mode 100644 debian/patches/victor-gmpxx-as-needed.diff
delete mode 100644 debian/patches/victor-use-env-opt-flags.diff
diff --git a/debian/control b/debian/control
index f6c8948..7b6e80b 100644
--- a/debian/control
+++ b/debian/control
@@ -2,7 +2,12 @@ Source: spark
Section: devel
Priority: optional
Maintainer: Євгеній Мещеряков <eu...@debian.org>
-Build-Depends: debhelper (>= 9), gnat, swi-prolog-nox (>= 6.2.6-2~), libgmp-dev (>= 2:5.0.1+dfsg-7~), bison, flex
+Build-Depends: debhelper (>= 9),
+ dpkg-dev (>= 1.16.1),
+# providing /usr/share/dpkg/default.mk
+ gnat (>= 4.9),
+# providing debian_packaging*.mk
+ swi-prolog-nox (>= 6.2.6-2~), libgmp-dev (>= 2:5.0.1+dfsg-7~), bison, flex
Standards-Version: 3.9.8
Homepage: http://libre.adacore.com/libre/tools/spark-gpl-edition/
Vcs-Git: git://anonscm.debian.org/collab-maint/spark.git
diff --git a/debian/patches/ada-link-env-flags.diff b/debian/patches/ada-link-env-flags.diff
deleted file mode 100644
index c61f40b..0000000
--- a/debian/patches/ada-link-env-flags.diff
+++ /dev/null
@@ -1,129 +0,0 @@
---- a/examiner/Makefile
-+++ b/examiner/Makefile
-@@ -95,6 +95,8 @@
- LINK_ARGS:=
- endif
-
-+LINK_ARGS += ${ADA_LINK}
-+
- ################################################################################
- # TARGETS
- ################################################################################
---- a/pogs/Makefile
-+++ b/pogs/Makefile
-@@ -45,6 +45,7 @@
-
- # Files containing platform specific code that is handled by gnatprep
- PREP_TARGETS:=${SPARK_PREPED}
-+LINK_ARGS:=${ADA_LINK}
-
- ################################################################################
- # TARGETS
-@@ -53,7 +54,7 @@
- all: ${OUTPUT_NAME}${EXE_EXTN}
-
- ${OUTPUT_NAME}${EXE_EXTN}: preamble prep
-- gnatmake -j${SPARKCPUS} ${GNATMAKE_OPTS} ${OUTPUT_NAME} -o $@ -bargs ${BIND_OPTS}
-+ gnatmake -j${SPARKCPUS} ${GNATMAKE_OPTS} ${OUTPUT_NAME} -o $@ -bargs ${BIND_OPTS} -largs ${LINK_ARGS}
-
- self-analysis: preamble prep
- -spark -plain @${OUTPUT_NAME}.smf
---- a/sparkformat/Makefile
-+++ b/sparkformat/Makefile
-@@ -68,6 +68,8 @@
- LINK_ARGS:=
- endif
-
-+LINK_ARGS += ${ADA_LINK}
-+
- ################################################################################
- # TARGETS
- ################################################################################
---- a/sparkmake/Makefile
-+++ b/sparkmake/Makefile
-@@ -34,6 +34,7 @@
-
- # Location of common.
- COMMON:=${ROOT}/common
-+LINK_ARGS:=${ADA_LINK}
-
- include ${COMMON}/Makefile.inc
-
-@@ -44,7 +45,7 @@
- all: ${OUTPUT_NAME}${EXE_EXTN}
-
- ${OUTPUT_NAME}${EXE_EXTN}: preamble prep parser
-- gnatmake -j${SPARKCPUS} ${GNATMAKE_OPTS} ${OUTPUT_NAME} -o $@ -bargs ${BIND_OPTS}
-+ gnatmake -j${SPARKCPUS} ${GNATMAKE_OPTS} ${OUTPUT_NAME} -o $@ -bargs ${BIND_OPTS} -largs ${LINK_ARGS}
-
- self-analysis: preamble prep parser
- -spark -plain @${OUTPUT_NAME}.smf
---- a/sparksimp/Makefile
-+++ b/sparksimp/Makefile
-@@ -41,7 +41,7 @@
- # PLATFORM INDEPENDENT CONFIGURATION
- ################################################################################
-
--LINK_ARGS:=new_expect.o
-+LINK_ARGS:=new_expect.o ${ADA_LINK}
-
- ################################################################################
- # TARGETS
---- a/victor_wrapper/Makefile
-+++ b/victor_wrapper/Makefile
-@@ -34,6 +34,7 @@
-
- # Location of common.
- COMMON:=${ROOT}/common
-+LINK_ARGS:=${ADA_LINK}
-
- include ${COMMON}/Makefile.inc
-
-@@ -44,7 +45,7 @@
- all: ${OUTPUT_NAME}${EXE_EXTN}
-
- ${OUTPUT_NAME}${EXE_EXTN}: preamble prep
-- gnatmake -j${SPARKCPUS} ${GNATMAKE_OPTS} ${OUTPUT_NAME} -o $@ -bargs ${BIND_OPTS}
-+ gnatmake -j${SPARKCPUS} ${GNATMAKE_OPTS} ${OUTPUT_NAME} -o $@ -bargs ${BIND_OPTS} -largs ${LINK_ARGS}
-
- self-analysis: preamble prep
- -spark -plain @${OUTPUT_NAME}.smf
---- a/wraputility/Makefile
-+++ b/wraputility/Makefile
-@@ -34,6 +34,7 @@
-
- # Location of common.
- COMMON:=${ROOT}/common
-+LINK_ARGS:=${ADA_LINK}
-
- include ${COMMON}/Makefile.inc
-
-@@ -44,7 +45,7 @@
- all: ${OUTPUT_NAME}${EXE_EXTN}
-
- ${OUTPUT_NAME}${EXE_EXTN}: preamble prep
-- gnatmake -j${SPARKCPUS} ${GNATMAKE_OPTS} ${OUTPUT_NAME} -o $@ -bargs ${BIND_OPTS}
-+ gnatmake -j${SPARKCPUS} ${GNATMAKE_OPTS} ${OUTPUT_NAME} -o $@ -bargs ${BIND_OPTS} -largs ${LINK_ARGS}
-
- self-analysis: preamble prep
- -spark -plain @${OUTPUT_NAME}.smf
---- a/sparkclean/Makefile
-+++ b/sparkclean/Makefile
-@@ -37,6 +37,8 @@
-
- include ${COMMON}/Makefile.inc
-
-+LINK_ARGS = ${ADA_LINK}
-+
- ################################################################################
- # TARGETS
- ################################################################################
-@@ -44,7 +46,7 @@
- all: ${OUTPUT_NAME}${EXE_EXTN}
-
- ${OUTPUT_NAME}${EXE_EXTN}:
-- gnatmake -j${SPARKCPUS} ${GNATMAKE_OPTS} ${OUTPUT_NAME} -o $@ -bargs ${BIND_OPTS}
-+ gnatmake -j${SPARKCPUS} ${GNATMAKE_OPTS} ${OUTPUT_NAME} -o $@ -bargs ${BIND_OPTS} -largs ${LINK_ARGS}
-
- self-analysis:
- -spark -plain @${OUTPUT_NAME}.smf
diff --git a/debian/patches/ada-use-evn-optflags.diff b/debian/patches/ada-use-evn-optflags.diff
deleted file mode 100644
index 6799fc3..0000000
--- a/debian/patches/ada-use-evn-optflags.diff
+++ /dev/null
@@ -1,16 +0,0 @@
-From: Eugeniy Meshcheryakov <eu...@debian.org>
-Subject: Use ADA_OPT environment variable
- ADA_OPT contains optimization switches for Ada compiller. This
- allows to use noopt in DEB_BUILD_OPTIONS
-Forwarded: not-needed
---- a/common/Makefile.inc
-+++ b/common/Makefile.inc
-@@ -84,7 +84,7 @@
-
- # Common compiler options.
- COMMON_OPTS:=-g -gnatwae -gnat05 -gnatwl -gnaty3abefhiklnprt -I${CUSTOMER_LIB} -I${COMMON}/versioning -I${ROOT}/examiner -gnatf -k
--GNATMAKE_OPTS:=${COMMON_OPTS} -O2 -fno-strict-aliasing
-+GNATMAKE_OPTS:=${COMMON_OPTS} ${ADA_OPT} -fno-strict-aliasing
- BIND_OPTS:=-E
-
- # Override compiler options for debug. No optimization, plus full
diff --git a/debian/patches/buildflags.diff b/debian/patches/buildflags.diff
new file mode 100644
index 0000000..0fbf5c3
--- /dev/null
+++ b/debian/patches/buildflags.diff
@@ -0,0 +1,74 @@
+Description: Read usual buildflags from command line or environment.
+ Namely: CC CFLAGS CPPFLAGS ADAFLAGS CPPFLAGS CXXFLAGS LDFLAGS.
+Author: Eugeniy Meshcheryakov <eu...@debian.org>
+Author: Nicolas Boulenguez <nico...@debian.org>
+
+--- a/common/Makefile.inc
++++ b/common/Makefile.inc
+@@ -83,8 +83,13 @@
+ CUSTOMER_LIB:=${ROOT}/lib/spark/current
+
+ # Common compiler options.
++CC ?= gcc
++CFLAGS ?= -g -O2
++ADAFLAGS ?= -O2
++
+ COMMON_OPTS:=-g -gnatwae -gnat05 -gnatwl -gnaty3abefhiklnprt -I${CUSTOMER_LIB} -I${COMMON}/versioning -I${ROOT}/examiner -gnatf -k
+-GNATMAKE_OPTS:=${COMMON_OPTS} -O2 -fno-strict-aliasing
++COMMON_OPTS += -largs ${LDFLAGS} -margs
++GNATMAKE_OPTS:=${COMMON_OPTS} ${ADAFLAGS} -fno-strict-aliasing
+ BIND_OPTS:=-E
+
+ # Override compiler options for debug. No optimization, plus full
+--- a/sparksimp/Makefile
++++ b/sparksimp/Makefile
+@@ -53,7 +53,7 @@
+ gnatmake -j${SPARKCPUS} ${GNATMAKE_OPTS} ${OUTPUT_NAME} -o $@ -bargs ${BIND_OPTS} -largs ${LINK_ARGS}
+
+ new_expect.o: new_expect.c
+- gcc -c -g -O2 -D${PREP_TARGET} $<
++ $(CC) -c $(CFLAGS) $(CPPFLAGS) -D${PREP_TARGET} -o $@ $<
+
+ # Cleaning code base
+ # ==================
+--- a/victor/Makefile
++++ b/victor/Makefile
+@@ -30,15 +30,12 @@
+ # PLATFORM SPECIFIC CONFIGURATION
+ ################################################################################
+
+-CPPFLAGS=
+-LDFLAGS=
+-
+ # Windows.
+ ifeq (${TARGET},Windows)
+ ifeq (${GCC_TARGET},i686-pc-mingw32)
+ # on windows, let the compiler know the gmplib location
+- CPPFLAGS="-I /gmp/include"
+- LDFLAGS="-L /gmp/lib"
++ CPPFLAGS += "-I /gmp/include"
++ LDFLAGS += "-L /gmp/lib"
+ endif
+ endif
+
+--- a/victor/vct/src/Makefile
++++ b/victor/vct/src/Makefile
+@@ -111,15 +111,12 @@
+ OPT=2
+
+ ifeq ($(OPT),none)
+- CXXFLAGS= -g -Wall
++ CXXFLAGS ?= -g -Wall
+ else
+- CXXFLAGS= -g -Wall -O$(OPT)
++ CXXFLAGS ?= -g -Wall -O$(OPT)
+ endif
+
+-
+-CPPFLAGS=
+-
+-LDFLAGS= -Wall
++LDFLAGS ?= -Wall
+
+ ifdef STATIC_GMP_MAC
+ LDLIBS= /usr/local/lib/libgmpxx.a /usr/local/lib/libgmp.a
diff --git a/debian/patches/checker-makefile.diff b/debian/patches/checker-makefile.diff
index e93d366..33f79d2 100644
--- a/debian/patches/checker-makefile.diff
+++ b/debian/patches/checker-makefile.diff
@@ -28,7 +28,7 @@ Forwarded: not-needed
ifeq ($(findstring ${TARGET},Windows),${TARGET})
--- a/common/Makefile.inc
+++ b/common/Makefile.inc
-@@ -106,10 +106,12 @@
+@@ -111,10 +111,12 @@
PREP_OPTS:=-c
# Common compiler options.
diff --git a/debian/patches/debian-architecture-detect.diff b/debian/patches/debian-architecture-detect.diff
deleted file mode 100644
index 25f6eea..0000000
--- a/debian/patches/debian-architecture-detect.diff
+++ /dev/null
@@ -1,26 +0,0 @@
-From: Eugeniy Meshcheryakov <eu...@debian.org>
-Subject: Assume that target is always Linux on Debian
- This makes it easier to compile SPARK on systems with *BSD kernels.
-Forwarded: not-needed
---- a/Makefile
-+++ b/Makefile
-@@ -31,7 +31,7 @@
- ################################################################################
-
- # Determine which platform this Makefile is being run on.
--TARGET:=$(shell uname -s)
-+TARGET:=Linux
- GCC_TARGET:=$(shell gcc -dumpmachine)
-
- # Canonicalize the target string.
---- a/common/Makefile.inc
-+++ b/common/Makefile.inc
-@@ -45,7 +45,7 @@
- ################################################################################
-
- # Determine which platform this Makefile is being run on.
--TARGET:=$(shell uname -s)
-+TARGET:=Linux
- GCC_TARGET:=$(shell gcc -dumpmachine)
-
- # Canonicalize the target string.
diff --git a/debian/patches/examiner-architecture-bits.diff b/debian/patches/examiner-architecture-bits.diff
deleted file mode 100644
index 89373e5..0000000
--- a/debian/patches/examiner-architecture-bits.diff
+++ /dev/null
@@ -1,17 +0,0 @@
-From: Eugeniy Meshcheryakov <eu...@debian.org>
-Subject: Use dpkg-architecture to detect address size
---- a/common/Makefile.inc
-+++ b/common/Makefile.inc
-@@ -121,11 +121,7 @@
- EXE_EXTN:=
- TAR:=tar
- PREP_TARGET:=Intel_Linux
-- ifeq (${GCC_TARGET},x86_64-pc-linux-gnu)
-- ADDRESS_SIZE:=64
-- else
-- ADDRESS_SIZE:=32
-- endif
-+ ADDRESS_SIZE:=$(shell dpkg-architecture -qDEB_HOST_ARCH_BITS)
- BUILD_VICTOR:=true
- SPLD_CONF:=
- endif
diff --git a/debian/patches/no-alt-ergo.diff b/debian/patches/no-alt-ergo.diff
index 179b8b3..b907125 100644
--- a/debian/patches/no-alt-ergo.diff
+++ b/debian/patches/no-alt-ergo.diff
@@ -14,7 +14,7 @@ Forwarded: not-needed
cp ./victor/vct/run/prelude.fdl ./share/spark/
--- a/victor/Makefile
+++ b/victor/Makefile
-@@ -50,7 +50,7 @@
+@@ -47,7 +47,7 @@
# Target to build vct and alt-ergo
ifeq (${BUILD_VICTOR},true)
diff --git a/debian/patches/series b/debian/patches/series
index 579b695..5077bec 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -1,5 +1,4 @@
-debian-architecture-detect.diff
-examiner-architecture-bits.diff
+buildflags.diff
checker-makefile.diff
checker-swi-prolog.diff
checker-predefined-predicates.diff
@@ -27,10 +26,6 @@ simplifier-pro-suffixes.diff
simplifier-undefined-exports.diff
simplifier-unexistent-units.diff
simplifier-remove-close_all_streams.diff
-victor-use-env-opt-flags.diff
-ada-use-evn-optflags.diff
-victor-gmpxx-as-needed.diff
-ada-link-env-flags.diff
swi-prolog-settings-module-conflict.pro
vct-bison-3-fix.diff
victor-quote-cppflags.diff
diff --git a/debian/patches/victor-gmpxx-as-needed.diff b/debian/patches/victor-gmpxx-as-needed.diff
deleted file mode 100644
index 570aaff..0000000
--- a/debian/patches/victor-gmpxx-as-needed.diff
+++ /dev/null
@@ -1,15 +0,0 @@
-From: Eugeniy Meshcheryakov <eu...@debian.org>
-Subject: Link to gmp libraries only when they are needed
- On x86_64 libgmpxx is unused. This could be different on other
- architectures.
---- a/victor/vct/src/Makefile
-+++ b/victor/vct/src/Makefile
-@@ -114,7 +114,7 @@
- ifdef STATIC_GMP
- LDLIBS= -Xlinker -Bstatic -lgmpxx -lgmp -Xlinker -Bdynamic -static-libstdc++ -s
- else
-- LDLIBS= -lgmpxx -lgmp
-+ LDLIBS= -Wl,--as-needed -lgmpxx -lgmp -Wl,--no-as-needed
- endif
- endif
-
diff --git a/debian/patches/victor-no-static-gmp.diff b/debian/patches/victor-no-static-gmp.diff
index 996167f..9d14df4 100644
--- a/debian/patches/victor-no-static-gmp.diff
+++ b/debian/patches/victor-no-static-gmp.diff
@@ -1,8 +1,10 @@
From: Eugeniy Meshcheryakov <eu...@debian.org>
Subject: Do not link gmp statically
+Forwarded: not-needed
+
--- a/victor/Makefile
+++ b/victor/Makefile
-@@ -60,7 +60,7 @@
+@@ -57,7 +57,7 @@
ifeq (${TARGET},Darwin)
$(MAKE) -C ${VICTOR}/src CPPFLAGS=${CPPFLAGS} LDFLAGS=${LDFLAGS} STATIC_GMP_MAC=1
else
diff --git a/debian/patches/victor-use-env-opt-flags.diff b/debian/patches/victor-use-env-opt-flags.diff
deleted file mode 100644
index 6a8f03b..0000000
--- a/debian/patches/victor-use-env-opt-flags.diff
+++ /dev/null
@@ -1,38 +0,0 @@
-From: Eugeniy Meshcheryakov <eu...@debian.org>
-Subject: Do not set LDFLAGS and CXXFLAGS in victor's Makefile
- Values from environment variables should be used instead. This
- allows to use noopt in DEB_BUILD_OPTIONS.
---- a/victor/vct/src/Makefile
-+++ b/victor/vct/src/Makefile
-@@ -108,19 +108,6 @@
- # Expected values of OPT set on make command line are "none", "1",
- # "2" or "3".
-
--OPT=2
--
--ifeq ($(OPT),none)
-- CXXFLAGS= -g -Wall
--else
-- CXXFLAGS= -g -Wall -O$(OPT)
--endif
--
--
--CPPFLAGS=
--
--LDFLAGS= -Wall
--
- ifdef STATIC_GMP_MAC
- LDLIBS= /usr/local/lib/libgmpxx.a /usr/local/lib/libgmp.a
- else
---- a/victor/Makefile
-+++ b/victor/Makefile
-@@ -30,9 +30,6 @@
- # PLATFORM SPECIFIC CONFIGURATION
- ################################################################################
-
--CPPFLAGS=
--LDFLAGS=
--
- # Windows.
- ifeq (${TARGET},Windows)
- ifeq (${GCC_TARGET},i686-pc-mingw32)
diff --git a/debian/rules b/debian/rules
index 8540b07..98410da 100755
--- a/debian/rules
+++ b/debian/rules
@@ -1,26 +1,24 @@
#!/usr/bin/make -f
-# FFLAGS because there are no Ada flags, and using CFLAGS results in a lot of warnings
-ADA_OPT = -gnatyN $(shell dpkg-buildflags --get FFLAGS)
-ADA_LINK = $(shell dpkg-buildflags --get LDFLAGS)
-
+DEB_BUILD_MAINT_OPTIONS := hardening=+all
+include /usr/share/dpkg/default.mk
+include /usr/share/ada/debian_packaging*.mk
+# The latter sets --as-needed in LDFLAGS.
+# For example, -lgmp is not actually used on all architectures.
+ADAFLAGS := -gnatyN $(ADAFLAGS)
ifeq (,$(filter noopt,$(DEB_BUILD_OPTIONS)))
- ADA_OPT += -fdata-sections -ffunction-sections
- ADA_LINK += -Wl,--gc-sections
-endif
-
-ifneq (,$(filter parallel=%,$(DEB_BUILD_OPTIONS)))
- NUMJOBS = $(patsubst parallel=%,%,$(filter parallel=%,$(DEB_BUILD_OPTIONS)))
- SPARKCPUS = $(NUMJOBS)
-else
- SPARKCPUS = 1
+ ADAFLAGS += -fdata-sections -ffunction-sections
+ LDFLAGS += -Wl,--gc-sections
endif
-export ADA_OPT ADA_LINK SPARKCPUS
-
-%:
+POLICY_TARGETS := binary binary-arch binary-indep build build-arch build-indep clean
+.PHONY: $(POLICY_TARGETS)
+$(POLICY_TARGETS):
dh $@ --with swi_prolog
+# Avoid debhelper running usual Make targets.
+.PHONY: $(addprefix override_dh_auto_,configure clean build test install)
+
override_dh_auto_clean:
$(MAKE) reallycleanall
@@ -30,14 +28,16 @@ override_dh_auto_build:
mkdir -p bin
mkdir -p share/spark
- dh_auto_build
-
-override_dh_auto_install:
- # nothing
-
-override_dh_auto_test:
- # nothing
+# From: Eugeniy Meshcheryakov <eu...@debian.org>
+# Assume that target is always Linux on Debian
+# This makes it easier to compile SPARK on systems with *BSD kernels.
+ dh_auto_build -- \
+ TARGET=Linux \
+ ADDRESS_SIZE=$(DEB_HOST_ARCH_BITS) \
+ SPARKCPUS=$(BUILDER_JOBS) \
+ $(foreach v,ADAFLAGS CFLAGS CPPFLAGS CXXFLAGS LDFLAGS,"$(v)=$($(v))")
+.PHONY: override_dh_install
override_dh_install:
dh_install
rm -r debian/spark/usr/lib/spark/current/spark_
--
2.8.1
>From 0e0d7778075e53ba3ff1ce0880e85210ca2acd6b Mon Sep 17 00:00:00 2001
From: Nicolas Boulenguez <nicolas.bouleng...@free.fr>
Date: Sun, 31 Jul 2016 20:30:46 +0200
Subject: [PATCH 6/6] Update URL of format for copyright file.
---
debian/copyright | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/debian/copyright b/debian/copyright
index 6bbbaca..eec05d4 100644
--- a/debian/copyright
+++ b/debian/copyright
@@ -1,4 +1,4 @@
-Format: http://dep.debian.net/deps/dep5
+Format: https://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
Upstream-Name: spark-gpl
Source: http://libre.adacore.com/libre/tools/spark-gpl-edition/
Comment:
--
2.8.1
