+2018-07-17 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * frontend.adb (Frontend): The removal of ignored Ghost code must be
+ the last semantic operation performed on the tree.
+
2018-07-17 Hristian Kirtchev <kirtchev@adacore.com>
* frontend.adb (Frontend): Update the call to Register_Config_Switches.
Check_Elaboration_Scenarios;
- -- Remove any ignored Ghost code as it must not appear in the
- -- executable.
-
- Remove_Ignored_Ghost_Code;
-
-- Examine all top level scenarios collected during analysis and
-- resolution in order to diagnose conditional ABEs, even in the
-- presence of serious errors.
Sem_Warn.Output_Unreferenced_Messages;
Sem_Warn.Check_Unused_Withs;
Sem_Warn.Output_Unused_Warnings_Off_Warnings;
+
+ -- Remove any ignored Ghost code as it must not appear in the
+ -- executable. This action must be performed last because it
+ -- heavily alters the tree.
+
+ if Operating_Mode = Generate_Code or else GNATprove_Mode then
+ Remove_Ignored_Ghost_Code;
+ end if;
end if;
end if;
end;