Lesson 2: Identifying Ineffective Statements
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.