Wasp messages
This chapter describes a Wasp message and the structure of a message listing saved to file.
Let us consider the example program errorLevels.java:
class errorLevels {
1 static void Step(int number, int[] a) {
2 if (number != 0) {
3 a[number] = 2;
4 int j = 0; int k = 5 / j;
5 }
6 }
7 public static void main (String args[]) {
8 int[] a;
9 int j;
10 a = new int[7];
11 for (int i = 1; i <= 7; ++i) {
12 Step(j,a); j++;
13 }
14 j = 7;
15 a[j] = 2;
16 }
17 }
The message file errorLevels.mes will be produced by Wasp launch for the program above.
Message levels
A message listing produced by Wasp includes error messages, conditional error messages and warnings. An error message corresponds to an absolute error because the error site in source code is proved by Wasp to be reached for every execution of a program. An error site for a conditional error is nested inside a control statement that may alter execution flow, such as if and switch statements, or a conditional expression. A conditional error turns to the actual error if the error site is reached for any execution of the program. It depends on the values of conditions in the listed above constructs enclosing the error site.
The message listing file errorLevels.mes includes the following messages:
###################### Scalar Errors (ABSOLUTE ERRORS) #####################
[E] (errorLevels.java 16,9) range 0:6 overflow on value 7
a[j] #= 2;
########### Variable usage before assignment (CONDITIONAL ERRORS) #########
[J] (errorLevels.java 13,19) variable j used before assignment on the
first iteration of cycle
Step(j,a); j#++;
##################### Scalar Errors (CONDITIONAL ERRORS) ###################
[C] (errorLevels.java 5,29) zero divisor 0
int j = 0; int k = 5 #/ j;
################ Variable usage before assignment (WARNINGS) ##############
[W] (errorLevels.java 13,12) variable j moved before assignment on the
first iteration of cycle
Step(#j,a); j++;
The first message reports an absolute error because the statement a[j] = 2 is always calculated when the program is executed. The third message indicates a conditional error, because it's error site is under condition number!=0 and possibly may not be reached in some program execution (if the value of i is zero). It is easy to see that the statement int k = 5 / j will be executed for all passes of the for cycle body except the first one. So this conditional error is an actual error.
The second message is also conditional but classified as a message of the [J] level. According to the Java language semantics, usage of variable value before variable assignment is not an error unlike semantics of other languages. However this situation is rather often induced by an error. So, Wasp produces a message if a variable usage is recognized as definite.
Information on variables
The message listing for the above example program errorLevels.java includes also the following messages:
######################## UNUSED VARIABLES (Strong) #########################
[W] (src/errorLevels.java 5,25) variable k assigned but not used
int j = 0; int k #= 5 / j;
[W] (src/errorLevels.java 8,34) formal parameter args not used
public static void main (String #args[]) {
######################### UNUSED VARIABLES (Weak) ##########################
[W] (errorLevels.java 4,18) variable $new0[] assigned but not used
a[number] $= 2;
#REFERENCES a^=$new0!
#DECLARATIONS $new0:(11,16) a:(2,37)
[W] (errorLevels.java 16,9) variable $new0[] assigned but not used
a[j] #= 2;
#REFERENCES a^=$new0!
#DECLARATIONS $new0:(11,16) a:(9,10)
The first section UNUSED VARIABLES (Strong) includes messages for strong (definite) assignments of variables while the second section includes messages for weak (possible) assignments.
Variable $new0 denotes the heap variable generated for an array in the execution of the statement a = new int[7]. For a K-th occurrence of the new construct in a Java program, the heap variable $newK denotes an object generated for this occurrence.
For an array variable X, X[] denotes an arbitrary element of the array X.
For a variable from message text, the #REFERENCES part of the message shows what variable points to it. The construct X^=Y means that the value of the variable X of the reference type is a heap variable Y, or, in other words, the reference variable X refers to an object presented by the heap variable Y.
In the last message of the above listing, the construct a^=$new0! means that variable a points to heap variable $new0. The token ! means that the variable $new0 is recognized by Wasp as a definite (obligatory) value of the variable a. The symbol "?" in that position would mean that the variable $new0 were recognized as possible value of the variable a.
In the #DECLARATIONS part, coordinates (line and column numbers) of the variable declaration in source code are shown for each variable from the #REFERENCES section.
Contexts
A context of a method F is a subset of the full set of call chains to the method F from the body of the public static void main(String []) method Let us illustrate the notion of context on the example program Contexts.java below.
1 public class Context {
2 static Str X=new Str(), Y=new Str(), U;
3 static int k=0;
4 static void F(Str Z) {
5 Z.field = k+1;
6 }
7 static void G(Str R) {
8 if (k!=0) F(R);
9 }
10 public static void main (String args[]) {
11 for (int i = 1; i <= 4; ++i) {
12 F(X); G(Y);
13 G(U); k--;
14 }
15 }
16 } //Context
17 class Str {
18 int field;
19 }
The full set of call chains to the method F (that is the full context) is the following:
main(12,9) ? F
main(12,15) ? G(8,16) ? F
main(13,9) ? G(8,16) ? F
The context above is called a total context. The non-total context is called a partial context.
Each Wasp message holds only within the context given in the #CONTEXT section of the message. If the #CONTEXT section is not present, the message holds for all possible call chains, for example, in the total context.
A context containing a single call chain
main(13,9) -> G(8,16) -> F
is used in the first message of the message listing (see below) for the Contexts.java program. This message is valid when the method F is called from the method G at position (8,16), and G, in turn, is called from the main method at position (13,9). The symbol "?" in G(10,21?) means that the indicated call of F in the body of G is under condition. The condition indicated for the G call in main(13,9?) is i <= 4 of the for statement.
Note that the second message of the listing below is induced by the erroneous situation showed by the first message.
########## null pointer exception & wrong cast (CONDITIONAL ERRORS) ########
[C] (Contexts.java 5,6) null pointer exception for variable Z
#Z.field = k+1;
#CONTEXT F(5,6) <- G(8,16?) <- main(13,9?)
############################ UNREACHABLE BRANCHES ##########################
[W] (Contexts.java 4,3) method F not completed normally
#static void F(Str Z) {
#CONTEXT F(4,3) <- G(8,16?) <- main(13,9?)
######################## UNUSED VARIABLES (Strong) #########################
[W] (Contexts.java 5,14) variables $new0.field,$new1.field assigned but
not used
Z.field #= k+1;
#REFERENCES Z^=$new0,$new1!
#DECLARATIONS $new0:(2,16) $new1:(2,29) Z:(4,21)
#CONTEXT F(5,14) <- G(8,16?) <- main(12,15?)
# F(5,14) <- main(12,9?)
The context included two call chains is defined in the last message of the listing above. The message part #REFERENCES Z^=$new0,$new1! means that the heap variables $new0 and $new1 both are definite values of the Z variable (each heap variable for it's own context).
In general case, a context is described by a tree-like chain of calls. Each new branch of the tree begins with the symbol # followed by a method call entered before.
In a Wasp message a call chain may finish before the main method. In this case, each continuation up to the main method is permitted. For instance, the call chain F(5,14) <- G(8,16?) means the following context:
#CONTEXT F(5,14) <- G(8,16?) <- main(12,15?)
# G(8,16?) <- main(13,9?)
For a call chain like F(5,14) <- G(8,16?), if you wish to know where the method G may be called, look for the string "G<" in the method call graph (see chapter Method call graph).
Variable denotations
The variable name modes used in Wasp message listing are described below.
<variable name> ::=
<variable identifier> |
<heap variable> |
<variable name>.<field name> |
<variable name>[] |
<previous instance of variable> |
<temporary variable>
If A is a name of an array variable, A[] denotes an arbitrary element or the array A.
<heap variable> ::=
$new<number of "new" occurrence>
<number of "new" occurrence> ::= <integer>
<previous instance of variable> ::=
<heap variable>'
Name $newK denotes a bf heap variable for an object generated by K-th occurrence of the new construct in a Java program. Any bf previous instance of the variable generated before by the same new construct is denoted by $newK.
In the example program below, after execution of the statement Node n = new Node(), the variable n points to the heap variable $new0. For the method call to_list(2) on line 10, the variable list (in the statement on line 5) refers to $new0 generated in the previous call of the method to_list, and hence list points to $new0'.
1 public class Previous {
2 static Node list; int i;
3 static void to_list(int e) {
4 Node n = new Node(); n.elem = e;
5 if (list != null) n.next = n;
6 list = n;
7 }
8 public static void main(String argv[]) {
9 to_list(1);
10 to_list(2);
11 }
12 }
13 class Node {
14 int elem;
15 Node next;
16 }
<temporary variable> ::=
@tmp<number>|
$method_result
<number> ::= <integer>
The temporary variables are used to denote some constructs such as conditional expressions. They rarely appear in Wasp messages. The variable $method_result means the result value of a method call.
|
