Skip to content

Instantly share code, notes, and snippets.

@JeremyGrosser

JeremyGrosser/gist:b805aab9f3f94533679b5453e0884afa

Created April 4, 2022 18:29
Show Gist options
  • Save JeremyGrosser/b805aab9f3f94533679b5453e0884afa to your computer and use it in GitHub Desktop.
Save JeremyGrosser/b805aab9f3f94533679b5453e0884afa to your computer and use it in GitHub Desktop.
Download ZIP
HAL SPARK errors
Raw
gistfile1.txt
synack@polar ~/build/hal(master) $ cat hal.gpr
project HAL is
for Source_Dirs use ("src");
for Library_Name use "hal";
for Object_Dir use "obj";
for Library_Dir use "lib";
for Library_Kind use "static";
package Compiler is
for Local_Configuration_Pragmas use "gnat.adc";
end Compiler;
end HAL;
synack@polar ~/build/hal(master) $ cat gnat.adc
pragma SPARK_Mode (On);
synack@polar ~/build/hal(master) $ /opt/GNAT/2021/bin/gnatprove -P hal.gpr -k
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
hal-time.ads:37:09: error: general access-to-variable type is not allowed in SPARK
37 | type Any_Delays is access all Delays'Class;
| ^~~~~~~~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-spi.ads:51:09: error: general access-to-variable type is not allowed in SPARK
51 | type Any_SPI_Port is access all SPI_Port'Class;
| ^~~~~~~~~~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-uart.ads:51:09: error: general access-to-variable type is not allowed in SPARK
51 | type Any_UART_Port is access all UART_Port'Class;
| ^~~~~~~~~~~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-gpio.ads:50:09: error: general access-to-variable type is not allowed in SPARK
50 | type Any_GPIO_Point is access all GPIO_Point'Class;
| ^~~~~~~~~~~~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-framebuffer.ads:47:09: error: general access-to-variable type is not allowed in SPARK
47 | type Any_Frame_Buffer_Display is access all Frame_Buffer_Display'Class;
| ^~~~~~~~~~~~~~~~~~~~~~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-framebuffer.ads:117:13: error: function with "in out" parameter is not allowed in SPARK
117 | function Hidden_Buffer
| ^~~~~~~~~~~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-bitmap.ads:103:09: error: general access-to-variable type is not allowed in SPARK
103 | type Any_Bitmap_Buffer is access all Bitmap_Buffer'Class;
| ^~~~~~~~~~~~~~~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-i2c.ads:51:09: error: general access-to-variable type is not allowed in SPARK
51 | type Any_I2C_Port is access all I2C_Port'Class;
| ^~~~~~~~~~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-real_time_clock.ads:81:09: error: general access-to-variable type is not allowed in SPARK
81 | type Any_RTC_Device is access all RTC_Device'Class;
| ^~~~~~~~~~~~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-block_drivers.ads:36:09: error: general access-to-variable type is not allowed in SPARK
36 | type Any_Block_Driver is access all Block_Driver'Class;
| ^~~~~~~~~~~~~~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-block_drivers.ads:43:13: error: function with "in out" parameter is not allowed in SPARK
43 | function Read
| ^~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-block_drivers.ads:50:13: error: function with "in out" parameter is not allowed in SPARK
50 | function Write
| ^~~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-bitmap.ads:103:09: error: general access-to-variable type is not allowed in SPARK
103 | type Any_Bitmap_Buffer is access all Bitmap_Buffer'Class;
| ^~~~~~~~~~~~~~~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-touch_panel.ads:55:09: error: general access-to-variable type is not allowed in SPARK
55 | type Any_Touch_Panel is access all Touch_Panel_Device'Class;
| ^~~~~~~~~~~~~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-touch_panel.ads:63:13: error: function with "in out" parameter is not allowed in SPARK
63 | function Active_Touch_Points (This : in out Touch_Panel_Device)
| ^~~~~~~~~~~~~~~~~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-touch_panel.ads:67:13: error: function with "in out" parameter is not allowed in SPARK
67 | function Get_Touch_Point (This : in out Touch_Panel_Device;
| ^~~~~~~~~~~~~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-touch_panel.ads:73:13: error: function with "in out" parameter is not allowed in SPARK
73 | function Get_All_Touch_Points
| ^~~~~~~~~~~~~~~~~~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-dsi.ads:62:09: error: general access-to-variable type is not allowed in SPARK
62 | type Any_DSI_Port is access all DSI_Port'Class;
| ^~~~~~~~~~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-filesystem.ads:82:09: error: general access-to-variable type is not allowed in SPARK
82 | type Any_Filesystem_Driver is access all Filesystem_Driver'Class;
| ^~~~~~~~~~~~~~~~~~~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-filesystem.ads:85:09: error: general access-to-variable type is not allowed in SPARK
85 | type Any_Directory_Handle is access all Directory_Handle'Class;
| ^~~~~~~~~~~~~~~~~~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-filesystem.ads:88:09: error: general access-to-variable type is not allowed in SPARK
88 | type Any_File_Handle is access all File_Handle'Class;
| ^~~~~~~~~~~~~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-filesystem.ads:91:09: error: general access-to-variable type is not allowed in SPARK
91 | type Any_Node_Handle is access all Node_Handle'Class;
| ^~~~~~~~~~~~~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-filesystem.ads:97:13: error: function with "in out" parameter is not allowed in SPARK
97 | function Open
| ^~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-filesystem.ads:104:13: error: function with "in out" parameter is not allowed in SPARK
104 | function Create_File (This : in out Filesystem_Driver;
| ^~~~~~~~~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-filesystem.ads:108:13: error: function with "in out" parameter is not allowed in SPARK
108 | function Unlink (This : in out Filesystem_Driver;
| ^~~~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-filesystem.ads:113:13: error: function with "in out" parameter is not allowed in SPARK
113 | function Remove_Directory (This : in out Filesystem_Driver;
| ^~~~~~~~~~~~~~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-filesystem.ads:123:13: error: function with "in out" parameter is not allowed in SPARK
123 | function Root_Node
| ^~~~~~~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-filesystem.ads:130:13: error: function with "in out" parameter is not allowed in SPARK
130 | function Read
| ^~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-filesystem.ads:167:13: error: function with "in out" parameter is not allowed in SPARK
167 | function Open
| ^~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-filesystem.ads:175:13: error: function with "out" parameter is not allowed in SPARK
175 | function Open
| ^~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-filesystem.ads:192:13: error: function with "in out" parameter is not allowed in SPARK
192 | function Read
| ^~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-filesystem.ads:199:13: error: function with "in out" parameter is not allowed in SPARK
199 | function Write
| ^~~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-filesystem.ads:211:13: error: function with "in out" parameter is not allowed in SPARK
211 | function Flush
| ^~~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
hal-filesystem.ads:215:13: error: function with "in out" parameter is not allowed in SPARK
215 | function Seek
| ^~~~
violation of pragma SPARK_Mode at /home/synack/build/hal/gnat.adc:1
1 |pragma SPARK_Mode (On);
|^ here
gnatprove: error during flow analysis and proof
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment