SPARK

Using SPARK with GPS

 

 

 

 

 

 

 

 

 

 

 

SPARK_GPS

Issue: 1.4

Status: Definitive

12th November 2010

 

DOCTYPE:Praxis title:varchar=title reference:varchar=reference status:varchar=status issue:varchar=issue date:varchar=date author:varchar=author projectname:varchar=DocumentSet

Issue 1.4, Definitive, 12th November 2010

000_000 Using SPARK with GPS

 

 

Originator

 

 

SPARK Team

 

 

Approver

 

 

SPARK Team Line Manager

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 


Contents

1          The SPARK plug-in for GPS

2          Setting up a GPS project for SPARK

3          The SPARK Menu in GPS

Document Control and References

Changes history

Changes forecast

 

 


1                       The SPARK plug-in for GPS

The SPARK Toolset includes a plug-in for GPS that provides support for the SPARK language and toolset. The plug-in that ships with the SPARK Toolset may incorporate enhancements and new features not present in the version that is installed by GPS.

This plug-in will be enabled only if you have the SPARK tools (eg the Examiner) available on your PATH. On Windows, the PATH can be set through “Control Panel -> System -> Advanced -> Environment Variables”.

If you are using GPS version 4.2.2 or above then the SPARK plug-in installed with the SPARK toolset will automatically override the version installed by GPS so you can skip the rest of this section.

If you are using an earlier version of GPS, the plug-in should be updated as follows:

Copy the file spark.py from <spark_install_dir>/share/gps/plug-ins to <gnatpro_install_dir>/share/gps/plug-ins.

2                       Setting up a GPS project for SPARK

Before you start using the SPARK commands you should first set your project properties following the guidelines below.

·  Select Edit Project Properties from the Project menu.

·  In order to access SPARK generated files from the GPS project explorer, click the Languages tab and ensure that the following items are ticked: Ada, Cmd, Dpc, Fdl, Index, Listing, Metafile, Plg, Pogs Summary, Prv, Rls, Rlu, Rul, Sdp, Siv, Slg, Vcg, Vct, Vlg. You should click the Source Dirs tab and enable Include Subdirectories so that VCG, DPC, SDP, SIV, VCT and VLG files are displayed in the project explorer.

·  Click the Switches tab and select the Examiner tab. This allows you to control the following settings:

o    the location of the index, warning and target configuration files if required

o    the directory to which the Examiner should write its output

o    whether to ignore the default switch file (useful when you want to specify switches that conflict with spark.sw)

o    the language to be analysed: SPARK83, SPARK95 (default) or SPARK 2005

o    the concurrency profile (sequential or ravenscar)

o    whether to include the SPARK library in the analysis

o    the flow analysis mode: information flow (default) or data flow only

o    whether or not to generate VCs

o    whether or not to generate DPCs

o    whether or not to check casing of identifiers

o    whether to enable policy checking

o    syntax check only mode

o    the level of error explanation required

o    the replacement rules for composite constants (see the Proof Manual)

o    the annotation character to be used (default is #)

o    plain output (for regression analysis)

o    HTML output

o    the listing file extension to be used

o    the report file name to be used

These options control the switches that will be passed to the Examiner. The actual switch settings are displayed in a text field at the bottom of the window and can be edited here directly if desired. Figure 1 overleaf shows the Examiner tab with some example settings. For more information on the meaning of these settings please refer to the Examiner User Manual.

Figure 1: Examiner settings tab

The tabs for SPARKSimp, Simplifier, ViCToR, ZombieScope, SPARKFormat, POGS and SPARKMake allow the settings for these tools to be controlled in a similar way to that described for the Examiner above. Please refer to the specific user manual for each tool to find more information about these settings.

When you have finished making changes click OK to return to the main GPS interface.

Every SPARK tool has its own tab where the user can specify the flags to invoke the tool. Users should refer to the tool’s user manual to find further information about each flag.

3                       The SPARK Menu in GPS

The commands available under the SPARK menu are:

Examine File

Runs the Examiner to analyse the file that is currently selected in the editing window. The results of the analysis will be displayed in the SPARK Output window. If the Examiner reports any errors or warnings these will be listed in the Locations window. Clicking on an error or warning in the Locations window will cause the editor window to jump to the source code line associated with that error or warning. Note that this command can also be invoked by right-clicking anywhere in a SPARK source file in the editing window and selecting SPARK -> Examine File, via the <F8> key or by right clicking the file in the Project View and selecting SPARK -> Examine File.

Examine Metafile

Note that this command is only available if a metafile is currently selected in the editing window. It will invoke the Examiner on the metafile - equivalent to supplying the metafile on the command line. Note that this command can also be invoked by right-clicking anywhere in a metafile in the editing window and selecting SPARK -> Examine Metafile or by right clicking the metafile in the Project View and selecting SPARK -> Examine Metafile.

SPARKFormat File

This command is enabled if a SPARK source file is selected in the editor window. It will reformat the file in-place with SPARKFormat, using the switches set under Project Properties. Note that this command can also be invoked by right-clicking anywhere in a SPARK source file in the editing window and selecting SPARK-> SPARKFormat File or via the <F12> key.

SPARKFormat Selection

This command is enabled if a SPARK source file is selected in the editor window. It applies SPARKFormat to the selected text only so, for example, an individual annotation can be selected and reformatted.

Simplify File

This command is enabled if a .VCG file is open in the editing window. It will invoke the SPARK Simplifier on the VCG file, using the switches set under the Simplifier’s tab in Project Properties. Output is sent to the Simplifier Output window. The siv file is displayed in the editing window.

ViCToR File

This command is enabled if a .VCG or .SIV file is open in the editing window. It will invoke ViCToR to translate the VC file and attempt to prove it using the SMT solver specified under the ViCToR tab in project properties. Note that ViCToR is currently an unsupported experimental feature, available on GNU/Linux only. For more information see the ViCToR Wrapper User Manual.  

 

ZombieScope File

This command is enabled if a .DPC file is open in the editing window. It will invoke the ZombieScope dead path analyser on the DPC file, using the switches set under the ZombieScope tab in Project Properties. Output is sent to the SPARK Output window. The .SDP file is displayed in the editing window.

SPARKSimp

Search under the project directory for all VCG and DPC files that require analysis and attempt to prove them. This is done using the SPARKSimp tool, with the switches supplied under the SPARKSimp tab in Project Properties. Output is displayed in the SPARK Output window.

POGS

Invokes POGS (Proof ObliGation Summariser). This will scan for proof files in the project's root directory and report the proof status in a file. The file name is the project's name with a ".sum" suffix. The default behaviour can be overwritten through Project -> Edit Project Properties -> Switches -> POGS by specifying the Input Directory from which POGS scans for proof files and the Output File where it saves the summary file. The summary output file is displayed in the editing window.

Right-clicking on a VC or DPC in the summary file invokes a pop-up menu. From this menu you can select:

SPARK -> Show VC                                                                       (to view the VCG file)

SPARK -> Show Simplified VC                                          (to view the SIV file)

SPARK -> Show DPC                                                                     (to view the DPC file)

SPARK -> Show ZLG                          (to view the ZLG file)

to jump directly to the file concerned. POGS can also be invoked via the <F11> key.

SPARKMake

This command is enabled if a SPARK source file is selected in the editing window. It invokes the SPARKMake tool, using the current file as the 'root'. This scans the current directory tree (unless specified otherwise under Project Properties) and attempts to produce an index file and metafile for the analysis of the current package and all packages (including bodies) that it depends on. Project Properties can be used to modify the switches - see the SPARKMake User Manual for more details. Note that this command can also be invoked by right-clicking anywhere in a SPARK source file in the editing window and selecting SPARK->SPARKMake or selecting the file in Project View.

Document Control and References

Altran Praxis Limited, 20 Manvers Street, Bath BA1 1PX, UK.

Copyright ã Altran Praxis Limited 2010.  All rights reserved.

Changes history

Issue 0.1  (8th February 2010): First draft.

Issue 0.2  (23rd February 2010): Update following review.

Issue 1.0  (1st March 2010): Definitive issue following review.

Issue 1.1 (12th October 2010): Correct references to the Examiner.

Issue 1.2 (3rd November 2010): Updates for release 9.1.

Issue 1.3 (3rd November 2010): Definitive issue addressing review comments.

Issue 1.4 (12th November 2010): Updated for –sparklib Examiner switch.

Changes forecast

None.