volatile_package.ads:
package Volatile_Package with SPARK_Mode => On
is
type Index_Type is range 192 .. 210; -- Some small, arbitrary range
Package_Variable : Index_Type with Volatile;
end Volatile_Package;
volatile_uninit.adb:
with Ada.Text_IO;
with Volatile_Package;
procedure Volatile_Uninit with SPARK_Mode => On
is
type Array_Type is array (Volatile_Package.Index_Type) of Integer;
Local_Array : constant Array_Type := (others => 15); -- Some arbitrary value
Local_Index_Variable : Volatile_Package.Index_Type;
Local_Integer : Integer;
begin
Local_Index_Variable := Volatile_Package.Package_Variable;
Local_Integer := Local_Array (Local_Index_Variable);
Ada.Text_IO.Put_Line ("Value of Local_Integer: " & Local_Integer'Image);
end Volatile_Uninit;Running Spark:
alr gnatprove --assumptions
on the above code does not give any warning nor state in gnatprove.out that Volatile_Package.Package_Variable is assumed to be initialized. If I understand, Spark makes this assumption due to Async_Writers being implicitly true for Package_Variable and Spark RM 7.1.2 Rule 14 applying.
I would have expected Spark to warn that it is making this assumption to alert the user and prompt manual review, since incorrect usage can lead to undefined behavior/erroneous execution as in the case above:
alr build --release
alr run
Garbage output:
Value of Local_Integer: 1413566023
Versions:
gnat FSF: 14.2.1
gnatprove: 14.1.1
volatile_package.ads:
volatile_uninit.adb:
Running Spark:
on the above code does not give any warning nor state in
gnatprove.outthatVolatile_Package.Package_Variableis assumed to be initialized. If I understand, Spark makes this assumption due toAsync_Writersbeing implicitly true forPackage_Variableand Spark RM 7.1.2 Rule 14 applying.I would have expected Spark to warn that it is making this assumption to alert the user and prompt manual review, since incorrect usage can lead to undefined behavior/erroneous execution as in the case above:
Garbage output:
Versions:
gnat FSF:
14.2.1gnatprove:
14.1.1