blob: c4a9f72c51c550e6994aa48918836db9314c5947 [file] [log] [blame]
Nico Huber2e09d2b2016-01-14 01:13:33 +01001-- This file is part of the coreboot project.
Patrick Georgi2faeb112020-05-08 18:32:38 +02002-- SPDX-License-Identifier: GPL-2.0-only
Nico Huber2e09d2b2016-01-14 01:13:33 +01003
4pragma Restrictions (No_Access_Subprograms);
5pragma Restrictions (No_Allocators);
6pragma Restrictions (No_Calendar);
7pragma Restrictions (No_Dispatch);
8pragma Restrictions (No_Exception_Handlers);
9pragma Restrictions (No_Fixed_Point);
10pragma Restrictions (No_Floating_Point);
11pragma Restrictions (No_Implicit_Dynamic_Code);
12pragma Restrictions (No_Implicit_Heap_Allocations);
13pragma Restrictions (No_Implicit_Loops);
14pragma Restrictions (No_Initialize_Scalars);
15pragma Restrictions (No_IO);
16pragma Restrictions (No_Local_Allocators);
17pragma Restrictions (No_Recursion);
18pragma Restrictions (No_Secondary_Stack);
19pragma Restrictions (No_Streams);
20pragma Restrictions (No_Tasking);
21pragma Restrictions (No_Unchecked_Access);
22pragma Restrictions (No_Unchecked_Deallocation);
23pragma Restrictions (No_Wide_Characters);
24pragma Restrictions (Static_Storage_Size);
25pragma Assertion_Policy
26 (Statement_Assertions => Disable,
27 Pre => Disable,
Nico Hubere941eef2016-10-05 17:45:33 +020028 Post => Disable,
29 Refined_Post => Disable);
Nico Huber2e09d2b2016-01-14 01:13:33 +010030pragma Overflow_Mode (General => Strict, Assertions => Eliminated);
31pragma SPARK_Mode (On);