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.
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 AuthorAngela Wallenburg has worked as a programmer and researcher since 1998. Early in her career she developed operation control and optimization software. Since program verification captured her interest she has worked on building verification tools at Chalmers and Gothenburg University in Sweden, University of Koblenz-Landau in Germany and Microsoft Research in the US. She joined Altran and the SPARK team in 2009 to continue her quest to build really usable tools for software engineers.
Last Updated: 10/13/2017
Posted on: 10/19/2009