[multiple changes]

2017-11-16  Joel Brobecker  <brobecker@adacore.com>

	* doc/gnat_ugn/gnat_utility_programs.rst: Document the switches
	available in gnatsymbolize.

2017-11-16  Steve Baird  <baird@adacore.com>

	* debug.adb: Update comment to indicate gnat2scil's use of the -gnatd.7
	switch.

From-SVN: r254826

3 files changed, 42 insertions, 2 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 8a7b649..0cc9d30 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,13 @@
+2017-11-16  Joel Brobecker  <brobecker@adacore.com>
+
+	* doc/gnat_ugn/gnat_utility_programs.rst: Document the switches
+	available in gnatsymbolize.
+
+2017-11-16  Steve Baird  <baird@adacore.com>
+
+	* debug.adb: Update comment to indicate gnat2scil's use of the -gnatd.7
+	switch.
+
 2017-11-16  Gary Dismukes  <dismukes@adacore.com>
 
 	* doc/gnat_ugn/elaboration_order_handling_in_gnat.rst, sem_ch6.adb,
diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb
index 442ce08..75e9591 100644
--- a/gcc/ada/debug.adb
+++ b/gcc/ada/debug.adb
@@ -161,7 +161,7 @@ package body Debug is
    --  d.4  Do not delete generated C file in case of errors
    --  d.5  Do not generate imported subprogram definitions in C code
    --  d.6  Do not avoid declaring unreferenced types in C code
-   --  d.7
+   --  d.7  Disable unsound heuristics in gnat2scil (for CP as SPARK prover)
    --  d.8
    --  d.9  Disable build-in-place for nonlimited types
 
diff --git a/gcc/ada/doc/gnat_ugn/gnat_utility_programs.rst b/gcc/ada/doc/gnat_ugn/gnat_utility_programs.rst
index 1122b70..7173c56 100644
--- a/gcc/ada/doc/gnat_ugn/gnat_utility_programs.rst
+++ b/gcc/ada/doc/gnat_ugn/gnat_utility_programs.rst
@@ -5031,7 +5031,7 @@ Alternatively, you may run the script using the following command line:
 
   ::
 
-       $ gnatsymbolize filename [ addresses ]
+       $ gnatsymbolize [ switches ] filename [ addresses ]
 
   For instance, consider the following Ada program:
 
@@ -5103,6 +5103,36 @@ Alternatively, you may run the script using the following command line:
        Foo at foo.adb:6
        Main at b~foo.adb:184
 
+  Switches for ``gnatsymbolize``
+  ------------------------------
+
+  ``gnatsymbolize`` recognizes the following switches:
+
+  .. index:: --help (gnatsymbolize)
+
+  :switch:`--help`
+    Display the program's usage, and then exit, disregarding all other
+    options.
+
+  :switch:`--cache`
+    Read the symbolic information from the executable and cache them
+    in memory in order to accelerate the translation of each address
+    into a symbolic location.
+
+    Depending on the size of the executable and the number of addresses
+    to translate, this may not always make ``gnatsymbolize`` faster
+    overall.
+
+  :switch:`--dump`
+    If :switch:`--cache` is used, dump the contents of the cache on
+    Standard Output. Has no effect otherwise.
+
+  :switch:`--count={N}`
+    If specified, compute the symbolic traceback ``N`` times in a row.
+    This option is mostly useful for measuring the performance of
+    ``gnatsymbolize``, particularly in the case where the cache is
+    being used.
+
   Requirements for Correct Operation
   ----------------------------------