blob: 5a03406dadc1a07aab5aa4d751f5639bf1a66bd5 [file] [log] [blame]
Patrick Georgi2faeb112020-05-08 18:32:38 +02001-- SPDX-License-Identifier: GPL-2.0-only
Nico Huber2e09d2b2016-01-14 01:13:33 +01002
3pragma Restrictions (No_Access_Subprograms);
4pragma Restrictions (No_Allocators);
5pragma Restrictions (No_Calendar);
6pragma Restrictions (No_Dispatch);
7pragma Restrictions (No_Exception_Handlers);
8pragma Restrictions (No_Fixed_Point);
9pragma Restrictions (No_Floating_Point);
10pragma Restrictions (No_Implicit_Dynamic_Code);
11pragma Restrictions (No_Implicit_Heap_Allocations);
12pragma Restrictions (No_Implicit_Loops);
13pragma Restrictions (No_Initialize_Scalars);
14pragma Restrictions (No_IO);
15pragma Restrictions (No_Local_Allocators);
16pragma Restrictions (No_Recursion);
17pragma Restrictions (No_Secondary_Stack);
18pragma Restrictions (No_Streams);
19pragma Restrictions (No_Tasking);
20pragma Restrictions (No_Unchecked_Access);
21pragma Restrictions (No_Unchecked_Deallocation);
22pragma Restrictions (No_Wide_Characters);
23pragma Restrictions (Static_Storage_Size);
24pragma Assertion_Policy
25 (Statement_Assertions => Disable,
26 Pre => Disable,
Nico Hubere941eef2016-10-05 17:45:33 +020027 Post => Disable,
28 Refined_Post => Disable);
Nico Huber2e09d2b2016-01-14 01:13:33 +010029pragma Overflow_Mode (General => Strict, Assertions => Eliminated);
30pragma SPARK_Mode (On);