diff options
| author | Arnaud Charlet <charlet@gcc.gnu.org> | 2016-06-22 11:51:47 +0200 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2016-06-22 11:51:47 +0200 |
| commit | 22da877084b5911b10f33195eea7487b1aeedb86 (patch) | |
| tree | a1efe225ac2928ed3055f84886f48b1045507a8f /gcc/ada/lib-xref-spark_specific.adb | |
| parent | 444656ce62eb1a2fd5e8e872b3804df0b61129a4 (diff) | |
| download | gcc-22da877084b5911b10f33195eea7487b1aeedb86.zip gcc-22da877084b5911b10f33195eea7487b1aeedb86.tar.gz gcc-22da877084b5911b10f33195eea7487b1aeedb86.tar.bz2 | |
[multiple changes]
2016-06-22 Hristian Kirtchev <kirtchev@adacore.com>
* exp_ch7.adb (Add_Invariant): Replace the
current type instance with the _object parameter even in ASIS mode.
(Build_Invariant_Procedure_Body): Do not insert the
invariant procedure body into the tree for ASIS and GNATprove.
(Build_Invariant_Procedure_Declaration): Do not insert the
invariant procedure declaration into the tree for ASIS and
GNATprove.
* lib-xref-spark_specific.adb (Add_SPARK_Scope): Update comment.
2016-06-22 Ed Schonberg <schonberg@adacore.com>
* sem_ch6.adb (Set_Actual_Subtypes): If the type of the actual
has predicates, the actual subtype must be frozen properly
because of the generated tests that may follow. The predicate
may be specified by an explicit aspect, or may be inherited in
a derivation.
From-SVN: r237684
Diffstat (limited to 'gcc/ada/lib-xref-spark_specific.adb')
| -rw-r--r-- | gcc/ada/lib-xref-spark_specific.adb | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index 062e50c..8bc6603 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -934,10 +934,9 @@ package body SPARK_Specific is D2 := D1; end if; - -- Some files do not correspond to Ada units, and as such present no - -- interest for SPARK cross references. Skip these files, as printing - -- their name may require printing the full name with spaces, which - -- is not handled in the code doing I/O of SPARK cross references. + -- Skip dependencies with no entity node, e.g. configuration files + -- with pragmas (.adc) or target description (.atp), since they + -- present no interest for SPARK cross references. if Present (Cunit_Entity (Sdep_Table (D1))) then Add_SPARK_File |