Skip to content

Commit

Permalink
gnat.adc: Do not generate assertion code for Refined_Post
Browse files Browse the repository at this point in the history
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>
  • Loading branch information
n-huber authored and i-c-o-n committed Oct 28, 2016
1 parent e84e625 commit e941eef
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion gnat.adc
Expand Up @@ -35,6 +35,7 @@ pragma Restrictions (Static_Storage_Size);
pragma Assertion_Policy
(Statement_Assertions => Disable,
Pre => Disable,
Post => Disable);
Post => Disable,
Refined_Post => Disable);
pragma Overflow_Mode (General => Strict, Assertions => Eliminated);
pragma SPARK_Mode (On);

0 comments on commit e941eef

Please sign in to comment.