Download SPARK Toolset Release Note 9

Tool Development and Support
SPARK Toolset Release Note 9
RN
Issue: 3.19
Contents
1
Introduction .............................................................................. 6
2
SPARK language changes....................................................... 7
2.1
2.2
2.3
2.4
SPARK 2005..........................................................................................7
Checking safety and security policies using flow analysis (IC15-003)
................................................................................................................8
Allow labels on statements in SPARK (SEPR 2703) ...........................8
Allow use of ‘others’ to initialize unconstrained array (SEPR 2723)..8
3
TN IA02-023 – Important Information for Users .................10
3.1
3.2
3.3
3.4
3.5
Description.......................................................................................... 10
SPARK Examiner versions affected................................................... 10
Test Case ............................................................................................ 10
Corrected Behaviour .......................................................................... 12
Recommended Action........................................................................ 13
4
Examiner changes..................................................................14
4.1
4.2
4.3
4.4
4.5
4.6
4.7
4.8
4.9
4.10
4.11
4.12
4.13
4.14
4.15
4.16
Allow labels on statements [I521-014] ............................................ 14
Allow proof refinement where applicable [I309-006] ...................... 14
Output Directory in report file [I610-021]......................................... 14
Allow use of ‘others’ to initialize unconstrained array [I409-012] .. 15
Control of path-names in “brief” output mode [I604-011].............. 15
Index file cache [I220-023] ............................................................... 15
New switch to select language profile [I717-014] ........................... 16
Stronger default “for” loop invariant [I715-017].............................. 16
Proof rules for record type equality [I803-018]................................ 18
Improved error messages for undeclared operators [I930-014] .... 19
Removal of Path Functions [IB17-027] ............................................ 19
Removal of obsolete VC Generation switches [IC01-020]............... 20
Casing option [I422-010] .................................................................. 20
Return annotations in function calls [I915-022].............................. 20
SLI file generation [J111-010] .......................................................... 22
Default install directory for Windows InstallShield [IB03-040] ....... 22
5
Simplifier changes .................................................................23
5.1
5.2
Enhanced log messages [I521-010]................................................. 23
Increased proof coverage for partially updated composites [I424030] .................................................................................................... 23
5.3 Simplifier uses inference rules from Examiner [I724-003] ............. 23
5.4 Extended Simplifier’s reasoning of simple universal quantifiers with
array updates [I724-016] .................................................................. 23
5.5 Better reasoning for bounds of modular expressions [I805-018] .. 24
5.6 Extended Simplifier’s reasoning of simple universal quantifiers
[I903-018] .......................................................................................... 24
5.7 Enhanced management of Hypothesis Identifiers [I629-007]........ 24
5.8 Improved readability of Simplifier verbose mode output [I727-020]
............................................................................................................. 24
5.9 Improved support for disjunctions [I611-014] ................................. 24
5.10 Improved reasoning of empty ranges in universal quantified VCs
[IA19-002] .......................................................................................... 25
Page 3 of 51