[Ada] Alternative display of multi-line messages for GNATprove

Pierre-Marie de Rodat derodat@adacore.com
Mon Oct 19 09:54:22 GMT 2020


GNATprove now supports better display of multi-line messages on the
command-line, where additional information for a given check is issued
on separate lines that are clearly associated to the main message, both
by prefixing such lines with space characters, and by separating a block
of lines corresponding to one message from the next with a newline.

For example:

after_tax.adb:7:22: medium: range check might fail
  e.g. when Before_Tax = 101
        and Rate = 2
  reason for check: returned value must fit in the result type ...
  possible fix: precondition of subprogram at after_tax.ads:3 should ...

This is made possible by implementing an alternative display of
continuation messages under debug switch -gnatdF.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* debug.adb: Use debug switch -gnatdF for this alternative
	display of messages.
	* errout.adb (Output_Messages): Alternative display when -gnatdF
	is used.
	* erroutc.adb (Output_Msg_Text): Likewise.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: patch.diff
Type: text/x-diff
Size: 3628 bytes
Desc: not available
URL: <https://gcc.gnu.org/pipermail/gcc-patches/attachments/20201019/62328e9c/attachment-0001.bin>


More information about the Gcc-patches mailing list