blob: 88cf438d7747660e1c95fb02ae568e83dd49d973 [file] [log] [blame]
Nico Huber2e09d2b2016-01-14 01:13:33 +01001--
2-- This file is part of the coreboot project.
3--
4-- This program is free software; you can redistribute it and/or modify
5-- it under the terms of the GNU General Public License as published by
6-- the Free Software Foundation; version 2 of the License.
7--
8-- This program is distributed in the hope that it will be useful,
9-- but WITHOUT ANY WARRANTY; without even the implied warranty of
10-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
11-- GNU General Public License for more details.
12--
13
14pragma Restrictions (No_Access_Subprograms);
15pragma Restrictions (No_Allocators);
16pragma Restrictions (No_Calendar);
17pragma Restrictions (No_Dispatch);
18pragma Restrictions (No_Exception_Handlers);
19pragma Restrictions (No_Fixed_Point);
20pragma Restrictions (No_Floating_Point);
21pragma Restrictions (No_Implicit_Dynamic_Code);
22pragma Restrictions (No_Implicit_Heap_Allocations);
23pragma Restrictions (No_Implicit_Loops);
24pragma Restrictions (No_Initialize_Scalars);
25pragma Restrictions (No_IO);
26pragma Restrictions (No_Local_Allocators);
27pragma Restrictions (No_Recursion);
28pragma Restrictions (No_Secondary_Stack);
29pragma Restrictions (No_Streams);
30pragma Restrictions (No_Tasking);
31pragma Restrictions (No_Unchecked_Access);
32pragma Restrictions (No_Unchecked_Deallocation);
33pragma Restrictions (No_Wide_Characters);
34pragma Restrictions (Static_Storage_Size);
35pragma Assertion_Policy
36 (Statement_Assertions => Disable,
37 Pre => Disable,
Nico Hubere941eef2016-10-05 17:45:33 +020038 Post => Disable,
39 Refined_Post => Disable);
Nico Huber2e09d2b2016-01-14 01:13:33 +010040pragma Overflow_Mode (General => Strict, Assertions => Eliminated);
41pragma SPARK_Mode (On);