Tokeneer Discovery: A SPARK Tutorial

Every statement should have a purpose. An ineffective statement has no effect on any output variable and therefore has no effect on the behaviour of the code. The presence of ineffective statements reduces the quality and the maintainabiliy of the code. The SPARK Toolset identifies all ineffective statements.

In this lesson, we will show how the SPARK Toolset finds ineffective statements to ensure that SPARK programs are free from them.

Step-by-Step Instructions

We will inject an ineffective statement into the Tokeneer code and use the Examiner to find it.

Step 1: Inject an Ineffective Statement

Start with a fresh copy of the file auditlog.adb by copying the file auditlog_copy.adb in tokeneer/code/core to auditlog.adb in the same directory.

Let us inject an ineffective statement into the implementation of the function NextListIndex (shown below) in auditlog.adb.

 
        189  function NextListIndex(Value : LogFileIndexT) return  LogFileIndexT
        190  is
        191     Result : LogFileIndexT;
        192  begin
        193     if Value = LogFileIndexT'Last then
        194        Result := LogFileIndexT'First;
        195     else
        196        Result := Value + 1;
        197     end if;
        198     return Result;
        199  end NextListIndex;
    

Modify the above code by adding the new variable Result_Tmp of type LogFileTypeT (line 191) and change line 196 so that Value + 1 is assigned to the variable Result_Tmp instead of Result (see code below).

 
        189  function NextListIndex(Value : LogFileIndexT) return  LogFileIndexT
        190  is
        191     Result, Result_Tmp: LogFileIndexT;
        192  begin
        193     if Value = LogFileIndexT'Last then
        194        Result := LogFileIndexT'First;
        195     else
        196        Result_Tmp := Value + 1;
        197     end if;
        198     return Result;
        199  end NextListIndex;
    

The statement on line 196 is ineffective as Result_Tmp is never used. Furthermore, the value for Result may be undefined when Value /= LogFileIndexT'Last.

Step 2: See How the Examiner Finds the Problem

Re-run the Examiner for auditlog.adb and, as expected, it finds the ineffective statement as well as the possible undefined value for Result.

Summary

In this lesson we have seen an example of the SPARK tools finding an ineffective statement. The SPARK tools will find all ineffective statements. In the next lesson, we will study Input Validation.