From: Maciej Sobczak <see.my.homepage@gmail.com>
Subject: SPARK - runtime checks question
Date: Fri, 19 Jun 2009 08:26:39 -0700 (PDT)
Date: 2009-06-19T08:26:39-07:00 [thread overview]
Message-ID: <8d79ac48-d35d-4717-aca3-68f036de0de3@f16g2000vbf.googlegroups.com> (raw)
Consider the following:
-- my_package.ads:
package My_Package is
function Distance (X : in Natural; Y : in Natural) return Natural;
end My_Package;
-- my_package.adb:
package body My_Package is
function Distance (X : in Natural; Y : in Natural) return Natural
is
Result : Natural;
begin
if X > Y then
Result := X - Y; // line 8
else
Result := Y - X; // line 10
end if;
return Result;
end Distance;
end My_Package;
The Distance function is supposed to compute the distance between two
Naturals.
I have a problem with rtc checks that are generated for line 8 and 10.
After running spark -vcg, sparksimp and pogs, the spark.sum file
contains this:
VCs for function_distance :
----------------------------------------------------------------------------
| | | -----Proved In----- |
| |
# | From | To | vcg | siv | plg | prv | False |
TO DO |
----------------------------------------------------------------------------
1 | start | rtc check @ 8 | | | | | |
YES |
2 | start | rtc check @ 10 | | | | | |
YES |
3 | start | assert @ finish | | YES | | |
| |
4 | start | assert @ finish | | YES | | |
| |
----------------------------------------------------------------------------
and of course 50% of VCs are undischarged in the final report.
As far as I understand the math, the relevant values are always within
the target type. What am I missing in this simple example?
--
Maciej Sobczak * www.msobczak.com * www.inspirel.com
Database Access Library for Ada: www.inspirel.com/soci-ada
next reply other threads:[~2009-06-19 15:26 UTC|newest]
Thread overview: 8+ messages / expand[flat|nested] mbox.gz Atom feed top
2009-06-19 15:26 Maciej Sobczak [this message]
2009-06-19 15:31 ` SPARK - runtime checks question Maciej Sobczak
2009-06-19 16:04 ` Rod Chapman
2009-06-19 18:29 ` Adam Beneschan
2009-06-19 18:55 ` Rod Chapman
2009-06-19 21:38 ` Maciej Sobczak
2009-06-19 18:33 ` Adam Beneschan
2009-06-19 21:16 ` Maciej Sobczak
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox