Download ESC/Java User's Manual

methodological reasons (see, for example, the discussion of unchecked exceptions in section 4.5).
The .spec files, the JDK files, or both may simply contain errors.
(See also the disclaimers near the beginning of this manual.)
C.0.11 Shared variables
ESC/Java depends on programmers to supply monitored and monitored_by pragmas telling which locks
protect which shared variables. In the absence of such annotations, ESC/Java will not produce a warning when a
routine might access a variable without holding the appropriate lock. Even when the user does specify which
locks protect which variables, there is another potential source of unsoundness: ESC/Java assumes that the value
of a shared variable stays unchanged if a routine releases and then reacquires the lock that protects it, ignoring the
possibility that some other thread might have acquired the lock and modified the variable in the interim.
C.0.12 Initialization of fields declared non_null
There is an unsoundness in ESC/Java's checking that constructors assign non-null values to fields declared
non_null. Consider the following program:
1:
2:
class C {
/*@ non_null */ Object f;
3:
C() {
m();
}
4:
5:
6:
7:
//@ modifies this.f;
void m() {
8:
9:
...
}
}
When checking the implementation of the constructor for C, ESC/Java will assume (based solely on the pragmas
on lines 2 and 8) that the method m returns with this.f set to a non-null value. While checking the body of m,
ESC/Java will check that any assignments to f indeed assign non-null values. However, if the body of m can
complete normally without assigning to this.f, then ESC/Java's assumption that this.f is always non-null after
line 6 will be unsound.
C.0.13 String literals
Java's treatment of string concatenation (see [JLS, 3.10.5]) is not accurately modeled by ESC/Java. This is a
source both of unsoundness and of incompleteness.
C.0.14 Search limits in Simplify
If Simplify cannot find a proof or a (potential) counterexample for the verification condition (see appendix A) for
a routine within a set time limit, then ESC/Java issues no warnings for the method, even though it might have
issued a warning if given a longer time limit. If Simplify reaches its time limit after reporting one or more
91 of 95