lib-xref-spark_specific.adb (Collect_SPARK_Xrefs): Skip unneeded cross ref files.
authorJohannes Kanig <kanig@adacore.com>
Wed, 7 Jan 2015 10:24:46 +0000 (10:24 +0000)
committerArnaud Charlet <charlet@gcc.gnu.org>
Wed, 7 Jan 2015 10:24:46 +0000 (11:24 +0100)
2015-01-07  Johannes Kanig  <kanig@adacore.com>

* lib-xref-spark_specific.adb (Collect_SPARK_Xrefs): Skip unneeded
cross ref files.

From-SVN: r219292

gcc/ada/ChangeLog
gcc/ada/lib-xref-spark_specific.adb

index a422194de6f8889af813ff5ab4ba32db47e583cc..526bf38027b7e0ca86a0894f478e54d73f64c38a 100644 (file)
@@ -1,3 +1,8 @@
+2015-01-07  Johannes Kanig  <kanig@adacore.com>
+
+       * lib-xref-spark_specific.adb (Collect_SPARK_Xrefs): Skip unneeded
+       cross ref files.
+
 2015-01-07  Robert Dewar  <dewar@adacore.com>
 
        * s-taprop-linux.adb, clean.adb: Minor reformatting.
index 28677060aae0db44fc6180fc75bab5ddf161627f..b38d65b23dd4894a75161c16c276413bde236940 100644 (file)
@@ -889,10 +889,18 @@ package body SPARK_Specific is
             D2 := D1;
          end if;
 
-         Add_SPARK_File
-           (Ubody => Sdep_Table (D1),
-            Uspec => Sdep_Table (D2),
-            Dspec => D2);
+         --  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.
+
+         if Present (Cunit_Entity (Sdep_Table (D1))) then
+            Add_SPARK_File
+              (Ubody => Sdep_Table (D1),
+               Uspec => Sdep_Table (D2),
+               Dspec => D2);
+         end if;
+
          D1 := D2 + 1;
       end loop;