gnat.adc: Do not generate assertion code for Refined_Post
Ada usually does lots of type and contract checking during runtime. As this produces overhead and there is nobody to tell when we run into an exception, we disable code generation for those checks. Now disable it for `Refined_Post` too, which was just missed earlier. Change-Id: I67ca754f830e387efee3930e86929eb494bfaf03 Signed-off-by: Nico Huber <nico.huber@secunet.com> Reviewed-on: https://review.coreboot.org/16945 Tested-by: build bot (Jenkins) Reviewed-by: Martin Roth <martinroth@google.com>
This commit is contained in:
parent
e84e625483
commit
e941eef823
3
gnat.adc
3
gnat.adc
|
@ -35,6 +35,7 @@ pragma Restrictions (Static_Storage_Size);
|
||||||
pragma Assertion_Policy
|
pragma Assertion_Policy
|
||||||
(Statement_Assertions => Disable,
|
(Statement_Assertions => Disable,
|
||||||
Pre => Disable,
|
Pre => Disable,
|
||||||
Post => Disable);
|
Post => Disable,
|
||||||
|
Refined_Post => Disable);
|
||||||
pragma Overflow_Mode (General => Strict, Assertions => Eliminated);
|
pragma Overflow_Mode (General => Strict, Assertions => Eliminated);
|
||||||
pragma SPARK_Mode (On);
|
pragma SPARK_Mode (On);
|
||||||
|
|
Loading…
Reference in New Issue