Gem #72: Tokeneer Discovery - Lesson 2

by Dean KuoAngela Wallenburg —AltranAltran

Let's get started…

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 Gem, we show how the SPARK Toolset finds ineffective statements to ensure that SPARK programs are free from them. We will inject an ineffective statement into the Tokeneer code and use the Examiner to locate it.

Step 1: Inject an ineffective statement

We will inject an ineffective statement into the implementation of the function NextListIndex 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;

Let's 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 because 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

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

auditlog.adb:196:10:
  Flow Error  10 - Ineffective statement.
auditlog.adb:198:14:
  Flow Error 501 - Expression contains reference(s) to variable Result, which may have an undefined value.
auditlog.adb:199:8:
  Flow Error  33 - The variable Result_Tmp is neither referenced nor exported.
auditlog.adb:199:8:
  Flow Error 602 - The undefined initial value of Result may be used in the derivation of the function value.

Summary

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

About the Author