Wasp message list
This section gives the comments for all the messages produced by Wasp in a message listing. For proper understanding, read first the chapter Wasp messages.
The following constructs may appear as parameters in the messages described in this section.
<variable list> ::= <variable name> | <variable list>,<variable name>
See declaration of <variable name> in section Variable denotations.
<value> ::= <multy-range>
<multi-range> ::= <integer> | <range> | <integer>,<multy-range> | <range>,<multy-range>
<range> ::= <integer>:<integer>
<integer> ::= <cardinal> | -<cardinal>
<cardinal> ::= <digit> | <cardinal><digit>
For a Java program, Wasp statically calculates the value of each expression as a multy-range, which is the approximation (usually imprecise) of the calculations performed in reality.
<iteration condition> ::= on the first iteration of cycle | on the iterations of cycle after first
Sometimes a message holds only for the first iteration of a cycle (or for iterations after first) and invalid in general. In this case the <iteration condition> is included in the message text.
Analysis cutoff in declaration of method <method name>
Only part of the method body was analysed due to analysis cutoff (see chapter Wasp strategy for big programs). Next messages show the calls (inside the body) where the analysis was interrupted.
binary operator result out of bounds for <value> and <value>
The value of binary operator is out of bounds of type specified by the Java semantics for the operator result.
Cutoff for call of method <method name>
The message show the call of the method where Wasp analysis was interrupted due analysis cutoff. See chapter Wasp strategy for big programs. Part of the method declaration after this method call was not analysed by Wasp.
condition in for cycle always is equal true
The bf for cycle will be infinite if there is no exits from the cycle body. The message may appear also in the case when Wasp found null pointer exception or impermissible cast in the cycle body.
division by zero for variable(s) <variable list>
For absolute and conditional error the specified variable(s) is exactly zero. In the case of warning, zero is included to the value statically calculated by Wasp.
false condition - body of for cycle never executed
The condition to enter in cycle body is calculated by Wasp to be false.
false condition - unreachable then-branch
The condition in bf if statement is calculated by Wasp to be false.
false first operand in &&/|| operator
In the case of the "&&" operator, the second operand is never executed. In the case of the "||" operator, the second operand is always executed.
false while-condition - do statement executed only once
The while-condition in do statement is calculated by Wasp to be false.
false while-condition - loop body never executed
The condition in while statement is calculated by Wasp to be false.
field <Identifier> of variable(s) <variable list> not used
The field <Identifier> of the specified variable(s) is never used in the analysed configuration (see section Analysed configuration) of the program.
formal parameter <variable name> not used
The value of the specified formal parameter of the method is not used in the method body.
impermissible cast for variable(s) <variable list> [<iteration condition>]
The value of the specified variable(s) cannot be converted to the reference type in the cast operator. The ClassCastException will be thrown if this cast operator is reachable in execution.
method <Identifier> not completed normally
The specified method has no normal exit from its body. The method is either completed through exception or will work infinitely.
null pointer exception for variable(s) <variable list> [<iteration condition>]
The value of the specified variable(s) is calculated by Wasp to be null in the construct where an object is needed. The null pointer exception would be thrown if this construct were ever executed.
object generated by new not used
The object instance generated by the new operator is calculated by Wasp not to participate in further execution of a program.
range <range> overflow on value <value>
The specified <value> of an expression, statically calculated in the form of multy-range, includes at least one integer which is greater than the right integer in the specified range.
range <range> underflow on value <value>
The specified <value> of an expression, statically calculated in the form of multy-range, includes at least one integer which is less than the left integer in the specified range.
switch expression value may have no switch label
The value of the switch expression, statically calculated by Wasp, includes at least one integer for whom corresponds no label in this switch statement, and default label is missing in the switch statement.
true condition - unreachable else-branch
The condition in the if statement is calculated by Wasp to be true.
true first operand in &&|| operator
In the case of the "||" operator, the second operand is never executed. In the case of the "&&" operator, the second operand is always executed.
uncaught exception
For thrown exception there is no catch clause that handles it. This message is produced only for unchecked exceptions. The Java front-end guarantees that each checked exception will be caught.
unreachable branch in switch
The value of the switch expression, statically calculated by Wasp in the form of multy-range, does not include the label of the designated branch.
unreachable catch clause
There is no exception handled by this catch clause.
unreachable default branch in switch
Each integer included in the multy-range, statically calculated by Wasp for the switch expression, is encountered as some label of the switch statement. So default branch will be never executed.
variable(s) <variable list> assigned but not used
The value of the specified variable(s) assigned by the assignment operator is not used in further execution of the program. Possible reason may be the repeated assignment to specified variable(s) in further execution without usage of the variable(s) between two assignments.
variable(s) <variable list> moved before assignment [<iteration condition>]
There were no assignments to the specified variable(s) after its declaration except the default initialization. In the case of heap variable (see section Variable denotations), there were no assignments after creation by the new statement except the default initialization.
The situation for which this message was produced is the following: the default value of the specified variable(s) is either assigned to another variable or substituted as actual parameter of a method invocation.
According to the Java language semantics, usage of the variable value before variable assignment is not an error. Sometimes this situation may be induced by an error. Wasp produces this message if the variable(s) usage is recognized as definite.
variable(s) <variable list> used before assignment [<iteration condition>]
There were no assignments to the specified variable(s) after its declaration except the default initialization. In the case of heap variable (see section Variable denotations), there were no assignments after creation by the new statement except the default initialization.
The default value of the specified variable(s) is used in the execution of the construct showed in the message.
According to the Java language semantics, usage of the variable value before variable assignment is not an error. However this situation is rather often induced by an error. Wasp produces this message if the variable(s) usage is recognized as definite.
while-condition always is equal true
The while statement will be infinite if there are no other exits from the cycle body. The message may appear also in the case when Wasp found null pointer exception or impermissible cast in the cycle body.
while-condition in do statement always is equal true
Designated do statement will be infinite if there are no other exits from the cycle body.
zero divisor <value>
Zero is included in the multy-range, statically calculated by Wasp for the specified divisor. This situation may be an error in rare case because Wasp calculation usually imprecise.
|
