Created
April 4, 2022 18:29
-
-
Save JeremyGrosser/b805aab9f3f94533679b5453e0884afa to your computer and use it in GitHub Desktop.
HAL SPARK errors
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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