|
The SPARK FAQ
This page contains our most-often asked support questions,
and question of the month - a recent enquiry to sparkinfo@praxis-his.com.
Question of the Month
Assignment to arrays
Q: When we attempt to intialise the array as follows:
for I in Index loop
AnArray (I) := 0.0;
end loop;
we get the following flow warning:
!!! ( 1) Flow Error : 23: Statement contains reference(s)
to undefined variable AnArray.
Similarly, if we try:
AnArray(Element1) := 0.0;
AnArray(Element2) := 0.0;
AnArray(Element3) := 0.0;
the same flow warning appears.
Why is this and what can we do about it?
A: Flow analysis on arrays in SPARK must be done with entire
arrays. Hence at the assignment to Element1 of AnArray, the
other elements of the array are undefined at that point, and
an error message is raised.
To initialise an array, an aggregate which specifies a value
for every component, should be used.
FAQs
Am I Supported?
Two main classes of customer are fully supported: professional
customers that have a current maintenance agreement with Praxis
High Integrity Systems, and academic institutions, where we
support a single named member of staff per faculty.
People who are not fully supported include students
at academic institutions, and buyers of the "SPARK Book"
by John Barnes. If you fall into one of these classes and
need help or wish to report a problem, then please do drop
us a line, and we will do our best to respond.
On what host operating systems are the tools available?
SPARC/Solaris (versions 2.5, 2.6, 7, 8 or 9),
Intel IA32/Windows NT 4, 2000, or XP
VAX/VMS (Version 5.5-2 and above)
What about other operating systems and targets?
The Examiner and the SPADE tools are known to run on Windows
95, 98 and ME, but these hosts are not supported.
Other Host/OS combinations that may be available in future
include Alpha/OpenVMS, Itanium/OpenVMS and Intel IA32/Linux.
Please contact us if you have specific requirements for one
of these.
My Examiner stops with a message about an "internal
limit" being reached. What's going on?
The Examiner's internal data structures all have fixed sizes,
which can be exceeded in the analysis of large or complex
programs. We normally ship three variants, imaginatively called
"Small", "Medium", and "Large."
If you've exceeded the limits in Small or Medium, then simply
use the next size up. We have found that the limits in the
Large Examiner are sufficient for well-designed systems of
almost any size. If you have exceeded the limits in the Large
Examiner, then please contact us for assistance.
My Examiner stops with "Storage_Error." What's
going on?
The Examiner requires resources from the host operating system
in order to run, chiefly memory and file "handles."
Some operating systems place limits on these resources which
may prevent the Examiner from running.
On Solaris, you may need to "unlimit" your process's
stack size and maximum number of file handles. See the Solaris
installation guide for details.
On Windows NT, you may need to increase the amount of virtual
and/or physical RAM available. We recommend a minimum of 64
Megabytes of physical RAM.
On the VAX, The "Small" Examiner runs, but "Large"
does not.
You may need your system administrator to increase your account's
quotas. The specific quotas that need increasing are:
Fillm (File Handle Limit)
WSquo (Working Set Quota)
WSextent (Working Set Extent)
Pgflquo (Page File Quota)
These quotas are modified using the sys$system:[000000]authorize
tool.
Previous Questions of the Month
Language
Information flow for functions
Q: Why don’t we specify information flow for functions?
A procedure has a derives annotation, e.g.
procedure Add (X, Y : in Integer; Z out Integer);
--# derives Z from X, Y;
but the equivalent function:
function Add (X, Y : in Integer) returns Integer;
has no derives annotation.
A: A function may not have side effects so it has, in effect,
only one export, its return value. Every other parameter and
global must therefore be an import. So we always know what the
information flow relation for a function is: it "derives
its return value from all of its parameters and globals".
Adding an annotation to say this would be redundant.
For a procedure, in general, this does not hold. We can change
arbitrary subsets of the parameters and globals depending on
other arbitrary subsets of them, so an annotation to describe
what is actually intended is essential. There are cases, such
as the example, where the information flow could be inferred
from the parameter list, but this is not generally true so it
is easier to always require the derives annotation even in cases
where it might not be strictly necessary.
ASCII characters
Q: I need to use the character ° in a text string, but
SPARK objects. Why?
A: The Examiner does not directly support characters above
ASCII 127 in SPARK83. In SPARK95, you can use Ada.Characters.Latin_1
to get the appropriate character constant, and use the "&"
operator to knit together a static string, e.g:
C : constant String := "hello" & Ada.Characters.Latin_1.Wibble;
Overflow concepts
Q: I have a question regarding the overflow concepts in Ada
and in SPARK. I want to understand the following warning better:
--- Warning : 302 : This expression may be re-ordered by
a compiler. Left to right evaluation was assumed for RTC generation.
The User Manual states:
"Issued when a potentially re-orderable expression
is encountered when run-time expression overflow checks are
being generated. For example x := a + b + c; Whether intermediate
sub-expression values overflow may depend on the order of
evaluation which is compiler-dependent. The Examiner generates
RTCs on the basis of left-to-right evaluation; however, code
generating this warning should be parenthesised to remove
the ambiguity. e.g. x := (a + b) + c;. "
Assume we have a type which is defined like this:
type Test_Type is range 1..10;
and the following variables A,B,C and D of type Test_Type:
A := 2;
B := 9;
C := 3;
D := A + B - C;
What is trying to warn me is that depending on the order
the Ada compiler chooses to evaluate the above expression,
a CONSTRAINT_ERROR exception may be raised. Using my example,
the following cases could happen.
Case 1: D:=2 + 9 - 3 = 11 - 3 (overflow)
Case 2: D:=2 + 9 -3 = 2 + 6 = 8 (OK)
The conclusion is that intermediate sub-expressions may cause
an overflow/constraint_error. Is this a correct understanding?
A: Almost…
A := 2;
B := 9;
C := 3;
D := A + B - C;
The operators here "+" and "-" actually
have the type signature:
function "+"(Left, Right : in Test_Type'Base)
return Test_Type'Base;
function "-"(Left, Right : in Test_Type'Base) return
Test_Type'Base;
(See LRM A.1(17)).
The Overflow_Check is therefore against Test_Type'Base not
Test_Type.
So...for D := A + B - C; we get the following, assuming Left-to-Right
evaluation order:
Temp := A + B;
if Temp not in Test_Type'Base then raise Constraint_Error;
end if; -- Overflow_Check
Temp := Temp - C;
if Temp not in Test_Type'Base then raise Constraint_Error;
end if; -- Overflow_Check
if Temp not in Test_Type than raise Constraint_Error; end
if; -- Range_Check.
D := Temp; -- everything OK!
Note - two Overflow_Checks and just ONE Range_Check at the
end.
There's a problem if the first intermediate assignment can
go outside of Test_Type'Base. When you have 2 or more operators
in an expressions that have the same precedence, then evaluation
order _can_ matter here, so you should always use brackets
to indicate the required order.
To see these Overflow_Checks with GNAT, you must compile
with the "-gnato" option.
POGS
Q: POGS doesn’t always notice that the Simplifier proved
everything!
A: If you’re using a .siv file which
is out-of-date, then POGS will generate a warning, and ignore
it. If you regenerate your .vcg files after simplification
then POGS will see the .siv files as out-of-date. The simple
solution to this question is therefore to ensure that your
files have been generated in the correct order.
Of course, you may have a valid reason for generating them
in a different order, in which case use the /i switch on POGS
which ignores dates.
It is worth noting that if you are running the Examiner using
the /plain switch you will also need to use the /i switch
when running POGS. |
