Stack Overflow
Stack Overflow

Questions tagged [spark-ada]

SPARK is a programming language developed to allow formal proof of the absence of run-time errors. SPARK overlaps sufficiently with Ada that all SPARK programs can be compiled with an Ada compiler.

SPARK Ada is a subset of the Ada programming language, and a toolkit, that supports formal proof. It is intended for use in systems that require high reliability and integrity.

54 questions
8
votes
1 answer

How to prove this invariant?

I aim to prove that the Horner's Rule is correct. To do so, I compare the value currently calculated by Horner with the value of "real" polynominal. So I made this piece of code: package body Poly with SPARK_Mode is function Horner (X : Integer;…
qutrupali
  • 83
  • 3
5
votes
3 answers

Ada SPARK convert string to integer

I need help some help with Ada SPARK. I would like to save a string like "1" into an integer variable. Background: I would like to read numbers from the command line input and process them as integers and check the program with SPARK Prove. Here's a…
Nessa3001
  • 91
  • 2
5
votes
4 answers

Program verification in SPARK - Counting elements in an array

I wrote a very simple program but I failed to prove it's functional correctness. It uses a list of items, with each item having a field indicating if it's free or used : type t_item is record used : boolean := false; value : integer…
Arnauld Michelizza
  • 51
  • 1
4
votes
3 answers

SPARK Ada: Overlays Without Copying

I am trying to create a view of an array object to better utilise SIMD vectors on the x86_64 platform. Here's the main idea: type Char_Set_Index is range 0 .. 7; type Char_Set_Element is mod 2 ** 32; type Character_Set_Vector is array…
Mark
  • 153
  • 6
4
votes
1 answer

How can I access a symbol from the linker script in my Ada code?

I am building my Ada/SPARK project using GNAT and I am using a linker script. Here is an excerpt: SECTIONS { .code : { . = ALIGN(0x4); *(.text.section1) _end_of_section1 = .; *(.text.section2) ... …
Nola
  • 436
  • 4
  • 12
4
votes
2 answers

How is the `'Old` attribute in a **Post** contract handled for access types that might got deallocated inside the function or procedure?

Assume having the following setup: type My is new Integer; type My_Acc is access My; procedure Replace(Self : in out My_Acc; New_Int : Integer) with Pre => New_Int /= Self.all, Post => Self'Old.all /= Self.all; Note: Code above might not be…
mhatzl
  • 173
  • 1
  • 7
4
votes
2 answers

Failed assert that libsparkcrypto SHA256 results are equal

Summary of my issue I am using the libsparkcrypto library for my SHA256 function. I am finding that I cannot Assert that x = y implies Sha256(x) = Sha256(y). Any help would be greatly appreciated. Code testpackage.adb package body TestPackage with …
WhaleDancer
  • 83
  • 7
4
votes
1 answer

Potential aliasing violation in swap array indexes SPARK-Ada

The Introduction to Spark course contains an example (#5) where GNATprove fails to prove that no aliasing occurs in a procedure that swaps two elements of an array: package P with SPARK_Mode => On is type P_Array is array (Natural range <>) of…
Daniel Ricketts
  • 447
  • 2
  • 8
4
votes
1 answer

SPARK instantiation error w.r.t. volatile type

I have a data structure approximately (I am unable to share the full source but can provide additional information on request) as follows: generic type Item_Type is private; package Util.Pool is type Pool is limited new…
Arets Paeglis
  • 3,856
  • 4
  • 35
  • 44
4
votes
1 answer

SPARK-Ada Using GNATProve to Assume a Postcondition of a GCC Intrinsic Function

I would like to create a function in SPARK_Mode that utilizes the GNAT GCC intrinsic function "__builtin_ctzll". with Interfaces; use Interfaces; package GCC_Intrinsic with SPARK_Mode is function DividesLL (A, B : Unsigned_64) return Boolean…
user13907685
4
votes
1 answer

Postcondition on a procedure doesn't prove even though the same condition is asserted and true at the end of procedure

The code looks like this: spec: type Some_Record_Type is private; procedure Deserialize_Record_Y(Record: in out Some_Record_Type) with Post => ( if Status_OK then ( ... other postconditions ... and then …
Dmitry Petukhov
  • 53
  • 6
4
votes
2 answers

Spark-Ada postcondition for array total

How does one write a Spark postcondition for a function that sums the elements of an array? (Spark 2014, but if someone shows me how to do it for an earlier Spark I should be able to adapt it.) So if I have: type Positive_Array is array (Positive…
digitig
  • 1,989
  • 3
  • 25
  • 45
3
votes
1 answer

Ada/SPARK: should I be using GNATprove? Where can I find it?

On chapter 22.1 of this Learning Ada, trying to build the examples. It expects GNATprove to be installed. I am using Ubuntu 18.04 LTS, and I don't see any package that provides it. When I tried to find the main repo, all I found was something at…
Jeff
  • 105
  • 7
3
votes
1 answer

How to access a parameter of a procedure in Pre/Post contracts of a procedure/funtion that has the the procedure as access parameter?

The Containers.Vector package defines some procedures that have an access to a procedure as parameter. This procedure supports one parameter. Examples: procedure Update_Element (Container : in out Vector; Index : in Index_Type; …
mhatzl
  • 173
  • 1
  • 7
3
votes
3 answers

Do pre and post conditions take the place of in function validation?

I have been trying to learn the basics of using SPARK and I have got my head round using the pre and post conditions, but I am unsure whether they take the place of validation? for example a function for a plane that will not switch into takeoff…
HubertBlu
  • 747
  • 1
  • 7
  • 20
1
2 3 4