[multiple changes]
authorPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Thu, 16 Nov 2017 15:49:46 +0000 (15:49 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Thu, 16 Nov 2017 15:49:46 +0000 (15:49 +0000)
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

gcc/ada/ChangeLog
gcc/ada/debug.adb
gcc/ada/doc/gnat_ugn/gnat_utility_programs.rst

index 8a7b64963d6dca6e55c715d15dcf963c4ebf870b..0cc9d30af867e852a2815a0419e71e861ae78ab6 100644 (file)
@@ -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,
index 442ce0873e5294a01aa865c5ad0a48e1d488415e..75e9591289279de06b441ada1723cdf89dfb0db0 100644 (file)
@@ -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
 
index 1122b70b1588c8414a7fb03db48f54559b3fcc0e..7173c5610d00ca009e197ca1e8514c7e834a7648 100644 (file)
@@ -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
   ----------------------------------