[coreboot-gerrit] New patch to review for coreboot: gnat.adc: Do not generate assertion code for Refined_Post

Nico Huber (nico.h@gmx.de) gerrit at coreboot.org
Sat Oct 8 23:46:14 CEST 2016


Nico Huber (nico.h at gmx.de) just uploaded a new patch set to gerrit, which you can find at https://review.coreboot.org/16945

-gerrit

commit ef972455759ffa0d09ca530bec22351160dd1198
Author: Nico Huber <nico.huber at secunet.com>
Date:   Wed Oct 5 17:45:33 2016 +0200

    gnat.adc: Do not generate assertion code for Refined_Post
    
    Change-Id: I67ca754f830e387efee3930e86929eb494bfaf03
    Signed-off-by: Nico Huber <nico.huber at secunet.com>
---
 gnat.adc | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/gnat.adc b/gnat.adc
index 3b463dc..88cf438 100644
--- a/gnat.adc
+++ b/gnat.adc
@@ -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);



More information about the coreboot-gerrit mailing list