When run in GNATprove mode, the frontend should still issue errors related
to wrong sizes for representation clauses and pragma Pack. As the target
machine can be specified with -gnatet, there is no need to ignore such
errors anymore.
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-01-21 Yannick Moy <m...@adacore.com>
* errout.adb (Special_Msg_Delete): Update comment. Remove
special case for GNATprove which should not ignore mismatch
in sizes for representation clauses.
* sem_prag.adb (Analyze_Pragma): Remove special case for GNATprove
which should not ignore pragma Pack.
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 206844)
+++ sem_prag.adb (working copy)
@@ -16168,11 +16168,11 @@
if not Rep_Item_Too_Late (Typ, N) then
- -- In the context of static code analysis, we do not need
- -- complex front-end expansions related to pragma Pack,
- -- so disable handling of pragma Pack in these cases.
+ -- In CodePeer mode, we do not need complex front-end
+ -- expansions related to pragma Pack, so disable handling
+ -- of pragma Pack.
- if CodePeer_Mode or GNATprove_Mode then
+ if CodePeer_Mode then
null;
-- Don't attempt any packing for VM targets. We possibly
Index: errout.adb
===================================================================
--- errout.adb (revision 206841)
+++ errout.adb (working copy)
@@ -2976,13 +2976,13 @@
elsif Msg = "size for& too small, minimum allowed is ^" then
- -- Suppress "size too small" errors in CodePeer mode and SPARK mode,
- -- since pragma Pack is also ignored in these configurations.
+ -- Suppress "size too small" errors in CodePeer mode, since code may
+ -- be analyzed in a different configuration than the one used for
+ -- compilation. Even when the configurations match, this message
+ -- may be issued on correct code, because pragma Pack is ignored
+ -- in CodePeer mode.
- -- At least the comment is bogus, since you can have this message
- -- with no pragma Pack in sight! ???
-
- if CodePeer_Mode or GNATprove_Mode then
+ if CodePeer_Mode then
return True;
-- When a size is wrong for a frozen type there is no explicit size
