Using SPARK (gnatprove) with preconditions

General
1

I want to create a function that adds a byte to the front of a string. I have a precondition for the input length (less or equal than 31) but gnatprove is indicating range check errors…

===== test_spark.ads =====
package Test_Spark is
type u8 is mod 2**8;
type u8_Array is array (Natural range <>) of u8;

function Add_Tag is (Input : String) return u8_Array
with Pre => Input'Length >=0 and Input'Length <= 31;
end Test_Spark;

===== test_spark.adb =====
package body Test_Spark is
function Add_Tag (Input : String) return u8_Array is
Result : u8_Array (Input'First .. 1 + Input'Last) := (others := 0);
begin
return Result;
end Add_Tag;
end Test_SPARK;

When running gnatprove, I get two errors:

test_spark.adb:3 medium: range check might fail
3 | Result : u8 (Array (Input’First .. 1 + Input’Last) := (others => 0);
| ^~~~~~

test_spark.adb:3 medium: range check might fail
3 | Result : u8 (Array (Input’First .. 1 + Input’Last) := (others => 0);
| ~~^~~~~~~~~~~~

Is it possible to do this in SPARK?

2

Get rid of this one: it’s trivially true.
Try Input'Length <= 31 and Input'Last < Natural'Last.
And:

  function Add_Tag (Input : String) return u8_Array is
    Result : u8_Array (Input'First .. 1 + Input'Last) := (others := 0);
  begin
    Return Result : u8_Array(0..Input'Length) do
      Result(1..Input'Length):= Input(Input'Range);  -- Index sliding here.
      Result(0):= u8'Last; -- Or whatever tag-value you want.
    End return;
  end Add_Tag;

The reason that the prover was flagging those conditions was because you could have a u8_Array of range Natural'Last..Natural'Last, which would cause the 1+Input'Last to overflow.

1 Like