Hello,

i'm trying to test the usability of ESC\Java2 but i have an "unsolvable"
problem at line 32 of the first file of my big project.

I've extracted the problem in an example below, with the error message.
Does anybody know how to solve it?

TIA

-------------------------------------------------------- Test.java
package unidata;

import java.awt.Color;
import java.awt.Font;
import java.io.*;
import java.util.Locale;
import javax.swing.UIManager;

public final class Test {
    static public String tmp =
            System.getProperty("java.io.tmpdir") +
            System.getProperty("file.separator") +
            "tmp.txt";
}
-------------------------------------------------------- Cmd.exe

D:\User\Archives\ESCJava-2.0a9-01-10-05-binary>"C:\j2sdk1.4.2_10\bin\Java.exe"
-Dsimplify=D:\User\Archives\ESCJava-2.0a9-01-10-05-binary\Simplify-1.5.4.exe
-classpath
"D:\User\Archives\ESCJava-2.0a9-01-10-05-binary\esctools2.jar"
escjava.Main -classpath
D:\User\Archives\ESCJava-2.0a9-01-10-05-binary\jmlspecs.jar -classpath .
-nowarn Deadlock -Verbose Test.java
[Full classpath is
.;C:\j2sdk1.4.2_10\jre\lib\rt.jar;C:\j2sdk1.4.2_10\jre\lib\i18n.jar;C:\j2sdk1.4.2_10\jre\lib\sunrsasign.jar;C:\j2sdk1.4.2_10\jre\lib\jsse.jar;C:\j2sdk1.4.2_10\jre\lib\jce.jar;C:\j2sdk1.4.2_10\jre\lib\charsets.jar;C:\j2sdk1.4.2_10\jre\classes]
[Full sourcepath is null]
[Init TypeCheck.inst to escjava.tc.TypeCheck@15cda3f]
ESC/Java version ESCJava-2.0a9
[parsing Test.java]
Test.java: Caution: Using given file as the .java file, even though it
is not the java file for unidata.Test on the classpath
No MRCU found
Found refinement sequence files
Refinement Sequence: [ Test.java ]
Consolidating 1 refinement; java file exists
Combining Test.java
Constructed refinement sequence
    [0.08 s 4599424 bytes]

unidata.Test ...
[prepping-slinks unidata.Test]
[Superlink resolving unidata.Test]
[checkCompilationUnit: checking for Test.java]
[loading C:\j2sdk1.4.2_10\jre\lib\rt.jar:java/lang/Object.class]
[Superlink resolving java.lang.Object]
[checkCompilationUnit: checking for
C:\j2sdk1.4.2_10\jre\lib\rt.jar:java/lang/Object.class]
[Superlink resolved java.lang.Object]
[Superlink resolved unidata.Test]
[prepping unidata.Test]
[prepping-slinks java.lang.Object]
[prepping java.lang.Object]
[prepping-complete java.lang.Object]
[prepping-complete unidata.Test]
[typechecking unidata.Test]
[prepping-slinks java.lang.System]
[loading C:\j2sdk1.4.2_10\jre\lib\rt.jar:java/lang/System.class]
[Superlink resolving java.lang.System]
[checkCompilationUnit: checking for
C:\j2sdk1.4.2_10\jre\lib\rt.jar:java/lang/System.class]
[Superlink resolved java.lang.System]
[prepping java.lang.System]
[prepping-complete java.lang.System]
[prepping-slinks java.lang.String]
[loading C:\j2sdk1.4.2_10\jre\lib\rt.jar:java/lang/String.class]
[Superlink resolving java.lang.String]
[checkCompilationUnit: checking for
C:\j2sdk1.4.2_10\jre\lib\rt.jar:java/lang/String.class]
[loading C:\j2sdk1.4.2_10\jre\lib\rt.jar:java/io/Serializable.class]
[Superlink resolving java.io.Serializable]
[checkCompilationUnit: checking for
C:\j2sdk1.4.2_10\jre\lib\rt.jar:java/io/Serializable.class]
[Superlink resolved java.io.Serializable]
[loading C:\j2sdk1.4.2_10\jre\lib\rt.jar:java/lang/Comparable.class]
[Superlink resolving java.lang.Comparable]
[checkCompilationUnit: checking for
C:\j2sdk1.4.2_10\jre\lib\rt.jar:java/lang/Comparable.class]
[Superlink resolved java.lang.Comparable]
[loading C:\j2sdk1.4.2_10\jre\lib\rt.jar:java/lang/CharSequence.class]
[Superlink resolving java.lang.CharSequence]
[checkCompilationUnit: checking for
C:\j2sdk1.4.2_10\jre\lib\rt.jar:java/lang/CharSequence.class]
[Superlink resolved java.lang.CharSequence]
[Superlink resolved java.lang.String]
[prepping java.lang.String]
[prepping-slinks java.io.Serializable]
[prepping java.io.Serializable]
[prepping enclosed interface Serializable]
[prepping-slinks java.lang.<the root interface>]
[Superlink resolving java.lang.<the root interface>]
[Superlink resolved java.lang.<the root interface>]
[prepping java.lang.<the root interface>]
[prepping enclosed interface Object]
[prepping-complete java.lang.<the root interface>]
[prepping-complete java.io.Serializable]
[loading
C:\j2sdk1.4.2_10\jre\lib\rt.jar:java/lang/InterruptedException.class]
[Superlink resolving java.lang.InterruptedException]
[checkCompilationUnit: checking for
C:\j2sdk1.4.2_10\jre\lib\rt.jar:java/lang/InterruptedException.class]
[loading C:\j2sdk1.4.2_10\jre\lib\rt.jar:java/lang/Exception.class]
[Superlink resolving java.lang.Exception]
[checkCompilationUnit: checking for
C:\j2sdk1.4.2_10\jre\lib\rt.jar:java/lang/Exception.class]
[loading C:\j2sdk1.4.2_10\jre\lib\rt.jar:java/lang/Throwable.class]
[Superlink resolving java.lang.Throwable]
[checkCompilationUnit: checking for
C:\j2sdk1.4.2_10\jre\lib\rt.jar:java/lang/Throwable.class]
[Superlink resolved java.lang.Throwable]
[Superlink resolved java.lang.Exception]
[Superlink resolved java.lang.InterruptedException]
[prepping-slinks java.lang.Comparable]
[prepping java.lang.Comparable]
[prepping enclosed interface Comparable]
[prepping-complete java.lang.Comparable]
[prepping-slinks java.lang.CharSequence]
[prepping java.lang.CharSequence]
[prepping enclosed interface CharSequence]
[prepping-complete java.lang.CharSequence]
[prepping-complete java.lang.String]
Test.java:11: Error: No such method _infixConcat_(java.lang.String,
java.lang.String) in type java.lang.String
                        System.getProperty("java.io.tmpdir") +
                                             ^
Test.java:11: Error: No method valueOf(error) matching given argument types
                        System.getProperty("java.io.tmpdir") +
                                             ^
Test.java:12: Error: No such method _infixConcat_(error,
java.lang.String) in type java.lang.String
                        System.getProperty("file.separator") +
                                             ^
[typechecking-end unidata.Test 0.271 s 4721992 bytes]
Caution: Turning off extended static checking due to type error(s)
  [0.361 s 4732416 bytes total] (aborted)
2 cautions
3 errors