Commit 4873032f authored by davidcok's avatar davidcok
Browse files

Adding support for multiple language variants

parent fb80b1bf
......@@ -354,7 +354,7 @@ The internal specifications are written for programs that conform to Java 1.7.
\item \textbf{-dirs} : treat all subsequent command-line arguments as if each were the argument to \texttt{-dir}
\item \textbf{-specspath} \textit{<path>} : defines the specifications path, cf. section TBD
\item \textbf{-keys} \textit{<keys>} : the argument is a comma-separated list of options JML keys (cf. section TBD)
\item \textbf{-strictJML} : warns about an OpenJML extensions to standard JML
\item \textbf{-lang=jml} : warns about an OpenJML extensions to standard JML
\end{itemize}
\begin{itemize}
......@@ -531,7 +531,7 @@ An option used primarily for testing:
\item \textbf{-specspath}: the parameter gives the sequence of directories in which to find .jml specification files for unnamed but referenced classes (cf. section TBD)
\item \textbf{-checkSpecsPath}: if enabled (the default), warns about \texttt{specspath} elements that do not exist
\item \textbf{-keys}: comma-separated list of the optional JML comment keys to enable (empty by default)
\item \textbf{-strictJML}: (disabled by default) warns about the use of any OpenJML extensions to standard JML; disable with -no-strictJML
\item \textbf{-lang=jml}: (disabled by default) warns about the use of any OpenJML extensions to standard JML; disable with -lang=jml+
\item \textbf{-showNotImplemented}: (disabled by default) warns about the use of features that are not implemented; disable with -no-showNotImplemented
\end{itemize}
......
......@@ -1073,14 +1073,14 @@ public class JmlAttr extends Attr implements IJmlVisitor {
boolean methodOverrides = utils.parents(jmethod.sym).size() > 1;
if (specHasAlso && !methodOverrides) {
if (!jmethod.name.toString().equals("compareTo") && !jmethod.name.toString().equals("definedComparison")) {// FIXME
if (JmlOption.isOption(context, JmlOption.STRICT)) {
if (JmlOption.langJML.equals(JmlOption.value(context, JmlOption.LANG))) {
log.error(spec, "jml.extra.also", jmethod.name.toString() );
} else {
log.warning(spec, "jml.extra.also", jmethod.name.toString() );
}
}
} else if (!specHasAlso && methodOverrides) {
if (JmlOption.isOption(context, JmlOption.STRICT)) {
if (JmlOption.langJML.equals(JmlOption.value(context, JmlOption.LANG))) {
log.error(spec, "jml.missing.also", jmethod.name.toString());
} else {
log.warning(spec, "jml.missing.also", jmethod.name.toString());
......@@ -3332,7 +3332,7 @@ public class JmlAttr extends Attr implements IJmlVisitor {
// // these JML methods, so it should not technically be needed.
Env<AttrContext> localEnv = env;
ListBuffer<Type> argtypesBuf = new ListBuffer<Type>();
boolean jmlstrict = JmlOption.isOption(context, JmlOption.STRICT);
boolean jmlstrict = JmlOption.langJML.equals(JmlOption.value(context, JmlOption.LANG));
Type t = null;
int n;
......
......@@ -846,7 +846,7 @@ public class JmlParser extends JavacParser {
nextToken();
}
} else {
if (JmlOption.isOption(context, JmlOption.STRICT)) {
if (JmlOption.langJML.equals(JmlOption.value(context, JmlOption.LANG))) {
log.warning(pos(),"jml.refining.required");
}
}
......@@ -2042,7 +2042,7 @@ public class JmlParser extends JavacParser {
}
if (clauses.size() == 0 && stat == null) {
if (jt != null && JmlOption.isOption(context, JmlOption.STRICT)) {
if (jt != null && JmlOption.langJML.equals(JmlOption.value(context, JmlOption.LANG))) {
jmlerror(pos, "jml.empty.specification.case");
}
if (jt == null && also == null && !code) return null;
......@@ -2677,7 +2677,7 @@ public class JmlParser extends JavacParser {
if (token.kind == STAR) {
nextToken();
} else if (token.kind == RBRACKET) {
if (JmlOption.isOption(context, JmlOption.STRICT)) {
if (JmlOption.langJML.equals(JmlOption.value(context, JmlOption.LANG))) {
log.warning(rbracketPos,"jml.not.strict","storeref with implied end-of-range (a[i..])");
}
// OK - missing hi end implies end of array
......@@ -2813,7 +2813,7 @@ public class JmlParser extends JavacParser {
// we just silently ignore that situation
// (this is true at the moment for math annotations, but could
// also be true for a modifier someone forgot)
if (JmlTokenKind.extensions.contains(j) && JmlOption.isOption(context, JmlOption.STRICT)) {
if (JmlTokenKind.extensions.contains(j) && JmlOption.langJML.equals(JmlOption.value(context, JmlOption.LANG))) {
log.warning(pos(),"jml.not.strict",j.internedName()); // FIXME - probably wrong position
}
} else if (j == ENDJMLCOMMENT) {
......@@ -3039,7 +3039,7 @@ public class JmlParser extends JavacParser {
case BSEXCEPTION:// FIXME - what can follow this?
case BSCOUNT:
case BSVALUES:// FIXME - what can follow this?
if (JmlOption.isOption(context,JmlOption.STRICT)) {
if (JmlOption.langJML.equals(JmlOption.value(context, JmlOption.LANG))) {
log.warning(p,"jml.not.strict",jt.internedName());
}
// fall-through
......@@ -3481,7 +3481,7 @@ public class JmlParser extends JavacParser {
// pos is the position of the \lbl token
int labelPos = pos();
if (token.kind == TokenKind.LPAREN) {
if (JmlOption.isOption(context,JmlOption.STRICT)) {
if (JmlOption.langJML.equals(JmlOption.value(context, JmlOption.LANG))) {
log.warning(pos,"jml.not.strict","functional form of lbl expression");
}
nextToken();
......@@ -3501,7 +3501,7 @@ public class JmlParser extends JavacParser {
} else {
Name n = ident();
JCExpression e = parseExpression();
if (jmlToken == JmlTokenKind.BSLBLANY && JmlOption.isOption(context,JmlOption.STRICT)) {
if (jmlToken == JmlTokenKind.BSLBLANY && JmlOption.langJML.equals(JmlOption.value(context, JmlOption.LANG))) {
log.warning(pos,"jml.not.strict","\\lbl");
}
return toP(jmlF.at(pos).JmlLblExpression(labelPos,jmlToken, n, e));
......
......@@ -190,7 +190,7 @@ public class Extensions {
} catch (java.io.IOException e) {
throw new RuntimeException(e);
}
if (JmlOption.isOption(context, JmlOption.STRICT)) return;
if (JmlOption.langJML.equals(JmlOption.value(context, JmlOption.LANG))) return;
String exts = JmlOption.value(context, JmlOption.EXTENSIONS);
if (exts == null || exts.isEmpty()) return;
for (String extname : exts.split(",")) {
......
......@@ -45,7 +45,11 @@ public class JmlOption implements IOption {
public static final JmlOption BOOGIE = new JmlOption("-boogie",false,false,"Enables static checking with boogie",null);
public static final JmlOption USEJAVACOMPILER = new JmlOption("-java",false,false,"When on, the tool uses only the underlying javac or javadoc compiler (must be the first option)",null);
public static final JmlOption JML = new JmlOption("-jml",false,true,"When on, the JML compiler is used and all JML constructs are ignored; use -no-jml to use OpenJML but ignore JML annotations",null);
public static final JmlOption STRICT = new JmlOption("-strictJML",false,false,"Disables any JML extensions in OpenJML",null);
//public static final JmlOption STRICT = new JmlOption("-strictJML",false,false,"Disables any JML extensions in OpenJML",null);
public static final String langJML = "jml";
public static final String langJavelyn = "javelyn";
public static final String langPlus = "jml+";
public static final JmlOption LANG = new JmlOption("-lang",true,"jml+","Set the language variant to use: " + langJML + ", " + langJavelyn + ", or " + langPlus + " (the default)",null);
public static final JmlOption EXTENSIONS = new JmlOption("-extensions",true,null,"Extension packages and classes (comma-separated qualified names)",null);
public static final JmlOption STOPIFERRORS = new JmlOption("-stopIfParseErrors",false,false,"When enabled, stops after parsing if any files have parsing errors",null);
......
......@@ -840,10 +840,6 @@ public class Main extends com.sun.tools.javac.main.Main {
Options options = Options.instance(context);
Utils utils = Utils.instance(context);
// if (options.get(helpOption) != null) {
// return false;
// }
String t = options.get(JmlOption.JMLTESTING.optionName());
Utils.testingMode = ( t != null && !t.equals("false"));
String benchmarkDir = options.get(JmlOption.BENCHMARKS.optionName());
......@@ -942,6 +938,16 @@ public class Main extends com.sun.tools.javac.main.Main {
options.put(JmlOption.ESC_BV.optionName(),(String)JmlOption.ESC_BV.defaultValue());
}
val = options.get(JmlOption.LANG.optionName());
if (val == null || val.isEmpty()) {
options.put(JmlOption.LANG.optionName(),(String)JmlOption.LANG.defaultValue());
} else if(JmlOption.langPlus.equals(val) || JmlOption.langJavelyn.equals(val) || JmlOption.langJML.equals(val)) {
} else {
Log.instance(context).warning("jml.message","Command-line argument error: Expected '" + JmlOption.langPlus + "', '" + JmlOption.langJML + "' or '" + JmlOption.langJavelyn + "' for -lang: " + val);
//Log.instance(context).getWriter(WriterKind.NOTICE).println("Command-line argument error: Expected 'auto', 'true' or 'false' for -escBV: " + val);
options.put(JmlOption.LANG.optionName(),(String)JmlOption.LANG.defaultValue());
}
String keysString = options.get(JmlOption.KEYS.optionName());
utils.commentKeys = new HashSet<String>();
if (keysString != null && !keysString.isEmpty()) {
......@@ -951,7 +957,7 @@ public class Main extends com.sun.tools.javac.main.Main {
if (utils.esc) utils.commentKeys.add("ESC");
if (utils.rac) utils.commentKeys.add("RAC");
if (JmlOption.isOption(context,JmlOption.STRICT.optionName())) utils.commentKeys.add("STRICT");
if (JmlOption.langJML.equals(JmlOption.value(context, JmlOption.LANG))) utils.commentKeys.add("STRICT");
utils.commentKeys.add("OPENJML");
JmlSpecs.instance(context).initializeSpecsPath();
......
......@@ -59,7 +59,7 @@ public class ShowStatement extends JmlExtension.Statement {
int pp = parser.pos();
int pe = parser.endPos();
init(parser);
if (JmlOption.isOption(context, JmlOption.STRICT)) {
if (JmlOption.langJML.equals(JmlOption.value(context, JmlOption.LANG))) {
log.warning(pp,"jml.not.strict","show statement");
}
......
......@@ -60,7 +60,7 @@ public class TypeRepresentsClauseExtension extends JmlExtension.TypeClause {
parser.nextToken();
e = parser.parseExpression();
} else if (parser.jmlTokenKind() == JmlTokenKind.LEFT_ARROW) {
if (parser.isDeprecationSet() || JmlOption.isOption(context, JmlOption.STRICT)) {
if (parser.isDeprecationSet() || JmlOption.langJML.equals(JmlOption.value(context, JmlOption.LANG))) {
log.warning(parser.pos(), "jml.deprecated.left.arrow.in.represents");
}
suchThat = false;
......
......@@ -146,7 +146,7 @@ compiler.err.jml.misplaced.count=\
compiler.err.jml.unrecoverable=\
Unrecoverable situation: {0}
compiler.warn.jml.not.strict=\
The {0} construct is an OpenJML extension to JML and not allowed under -strictJML
The {0} construct is an OpenJML extension to JML and not allowed under -lang=jml
compiler.err.jml.file.class.mismatch=\
A class is not defined in the expected file: {0}
compiler.warn.jml.refining.specs.not.implemented=\
......
......@@ -45,7 +45,7 @@ JML options:
-boogie Enables static checking with boogie
-java When on, the tool uses only the underlying javac or javadoc compiler (must be the first option)
-jml When on, the JML compiler is used and all JML constructs are ignored; use -no-jml to use OpenJML but ignore JML annotations
-strictJML Disables any JML extensions in OpenJML
-lang Set the language variant to use: jml, javelyn, or jml+ (the default)
-extensions Extension packages and classes (comma-separated qualified names)
-stopIfParseErrors When enabled, stops after parsing if any files have parsing errors
-method Comma-separated list of method name patterns on which to run ESC
......
......@@ -390,7 +390,7 @@ public class SFBugs extends EscBase {
}
@Test public void gitbug528() {
helpTCG("-strictJML","-check"); // Just checking
helpTCG("-lang=jml","-check"); // Just checking
}
@Test public void gitbug529() {
......
......@@ -509,7 +509,7 @@ public class api extends JmlTestCase {
}
String parseString(String prog) throws Exception {
IAPI m = Factory.makeAPI("-jml","-strictJML");
IAPI m = Factory.makeAPI("-jml","-lang=jml");
return m.parseString("A.java",prog).toString();
}
......
......@@ -800,11 +800,11 @@ public class compiler {
{ "-classpath","../OpenJML/runtime",
"-sourcepath","test/testNoErrors",
"-specspath","../OpenJML/runtime",
"-strictJML",
"-lang=jml",
"-extensions=X", // Ignored when strict
"test/testNoErrors/A.jml"
},0,0
,"$SPECS/specs/java/util/stream/Stream.jml:60: warning: The /count construct is an OpenJML extension to JML and not allowed under -strictJML\n"
,"$SPECS/specs/java/util/stream/Stream.jml:60: warning: The /count construct is an OpenJML extension to JML and not allowed under -lang=jml\n"
+" //@ loop_invariant i == /count && 0 <= i && i <= values.length;\n"
+" ^\n"
+"1 warning\n");
......
......@@ -4257,7 +4257,7 @@ public class esc extends EscBase {
@Test
public void testShowStatement() {
expectedExit = 0;
main.addOptions("-strictJML");
main.addOptions("-lang=jml");
helpTCX("tt.TestJava",
"package tt; \n"
+ "public class TestJava { \n"
......@@ -4268,8 +4268,8 @@ public class esc extends EscBase {
+ " //@ show i;\n"
+ " }\n"
+ "}\n"
,"/tt/TestJava.java:7: warning: The show statement construct is an OpenJML extension to JML and not allowed under -strictJML",10
,"$SPECS/specs/java/util/stream/Stream.jml:60: warning: The \\count construct is an OpenJML extension to JML and not allowed under -strictJML",37
,"/tt/TestJava.java:7: warning: The show statement construct is an OpenJML extension to JML and not allowed under -lang=jml",10
,"$SPECS/specs/java/util/stream/Stream.jml:60: warning: The \\count construct is an OpenJML extension to JML and not allowed under -lang=jml",37
);
}
......
......@@ -177,7 +177,7 @@ public class escinline extends EscBase {
@Test // inline is an extension and should be final
public void testInline3() {
main.addOptions("-strictJML");
main.addOptions("-lang=jml");
helpTCX("tt.TestJava","package tt; //@ code_java_math spec_java_math \n"
+" class M { \n"
+" public int j;\n"
......@@ -187,8 +187,8 @@ public class escinline extends EscBase {
+" return i + 1;\n"
+" }\n"
+"}\n"
,"/tt/TestJava.java:4: warning: The inline construct is an OpenJML extension to JML and not allowed under -strictJML", 15
,"$SPECS/specs/java/util/stream/Stream.jml:60: warning: The \\count construct is an OpenJML extension to JML and not allowed under -strictJML",37
,"/tt/TestJava.java:4: warning: The inline construct is an OpenJML extension to JML and not allowed under -lang=jml", 15
,"$SPECS/specs/java/util/stream/Stream.jml:60: warning: The \\count construct is an OpenJML extension to JML and not allowed under -lang=jml",37
,"/tt/TestJava.java:4: warning: Inlined methods should be final since overriding methods will be ignored: minline", 15
);
}
......
......@@ -37,30 +37,26 @@ public class escoption extends EscBase {
}
public void testOptionValueBoolean() {
Assert.assertEquals(false,JmlOption.isOption(main.context(), JmlOption.STRICT));
Assert.assertEquals("false",JmlOption.value(main.context(), JmlOption.STRICT));
Assert.assertEquals(false,JmlOption.isOption(main.context(), "-strictJML"));
Assert.assertEquals("false",JmlOption.value(main.context(), "-strictJML"));
JmlOption.setOption(main.context(), JmlOption.STRICT, true);
Assert.assertEquals(true,JmlOption.isOption(main.context(), JmlOption.STRICT));
JmlOption.setOption(main.context(), JmlOption.STRICT, false);
Assert.assertEquals(false,JmlOption.isOption(main.context(), JmlOption.STRICT));
main.addOptions("-strictJML");
Assert.assertEquals(true,JmlOption.isOption(main.context(), JmlOption.STRICT));
main.addOptions("-no-strictJML");
Assert.assertEquals(false,JmlOption.isOption(main.context(), JmlOption.STRICT));
JmlOption.putOption(main.context(), JmlOption.STRICT);
Assert.assertEquals(true,JmlOption.isOption(main.context(), JmlOption.STRICT));
JmlOption.setOption(main.context(), JmlOption.STRICT, false);
Assert.assertEquals(false,JmlOption.isOption(main.context(), JmlOption.STRICT));
JmlOption.putOption(main.context(), JmlOption.STRICT, "true");
Assert.assertEquals(true,JmlOption.isOption(main.context(), JmlOption.STRICT));
JmlOption.putOption(main.context(), JmlOption.STRICT, "false");
Assert.assertEquals(false,JmlOption.isOption(main.context(), JmlOption.STRICT));
JmlOption.putOption(main.context(), JmlOption.STRICT, "");
Assert.assertEquals(true,JmlOption.isOption(main.context(), JmlOption.STRICT));
JmlOption.putOption(main.context(), JmlOption.STRICT, null);
Assert.assertEquals(false,JmlOption.isOption(main.context(), JmlOption.STRICT));
Assert.assertEquals("jml+",JmlOption.value(main.context(), JmlOption.LANG));
Assert.assertEquals("jml+",JmlOption.value(main.context(), JmlOption.LANG));
Assert.assertEquals("jml+",JmlOption.value(main.context(), "-lang"));
Assert.assertEquals("jml+",JmlOption.value(main.context(), "-lang"));
JmlOption.putOption(main.context(), JmlOption.LANG, "jml");
Assert.assertEquals("jml",JmlOption.value(main.context(), JmlOption.LANG));
JmlOption.putOption(main.context(), JmlOption.LANG, "javelyn");
Assert.assertEquals("javelyn",JmlOption.value(main.context(), JmlOption.LANG));
JmlOption.putOption(main.context(), JmlOption.LANG, "jml+");
Assert.assertEquals("jml+",JmlOption.value(main.context(), JmlOption.LANG));
main.addOptions("-lang=jml");
Assert.assertEquals("jml",JmlOption.value(main.context(), JmlOption.LANG));
main.addOptions("-lang=javelyn");
Assert.assertEquals("javelyn",JmlOption.value(main.context(), JmlOption.LANG));
main.addOptions("-lang=jml+");
Assert.assertEquals("jml+",JmlOption.value(main.context(), JmlOption.LANG));
JmlOption.putOption(main.context(), JmlOption.LANG, "javelyn");
Assert.assertEquals("javelyn",JmlOption.value(main.context(), JmlOption.LANG));
JmlOption.putOption(main.context(), JmlOption.LANG, "jml+");
Assert.assertEquals("jml+",JmlOption.value(main.context(), JmlOption.LANG));
}
@Test
......
......@@ -9,14 +9,16 @@ import org.junit.Test;
public class strict extends TCBase {
String opt = JmlOption.STRICT.optionName();
String opt = JmlOption.LANG.optionName();
String optjml = opt + "=jml";
String optjmlp = opt + "=jml+";
@Override
public void setUp() throws Exception {
// noCollectDiagnostics = true;
// jmldebug = true;
super.setUp();
main.addOptions(opt);
main.addOptions(optjml);
expectedExit = 0;
}
......@@ -24,13 +26,13 @@ public class strict extends TCBase {
public void testLbl() {
helpTCF("A.java","public class A {\n" +
" //@ ghost int i = (\\lbl A 0);\n }"
,"/A.java:2: warning: The \\lbl construct is an OpenJML extension to JML and not allowed under " + opt,21
,"/A.java:2: warning: The \\lbl construct is an OpenJML extension to JML and not allowed under " + optjml,21
);
}
@Test
public void testLblB() {
main.addOptions(opt + "=false");
main.addOptions(optjmlp);
helpTCF("A.java","public class A {\n" +
" //@ ghost int i = (\\lbl A 0);\n }"
);
......@@ -42,13 +44,13 @@ public class strict extends TCBase {
" void m(int[] a) { for (int i: a) {\n" +
" //@ assert \\count == i; \n" +
" }}}"
,"/A.java:3: warning: The \\count construct is an OpenJML extension to JML and not allowed under " + opt,16
,"/A.java:3: warning: The \\count construct is an OpenJML extension to JML and not allowed under " + optjml,16
);
}
@Test
public void testIndexB() {
main.addOptions(opt + "=false");
main.addOptions(optjmlp);
helpTCF("A.java","public class A {\n" +
" void m(int[] a) { for (int i: a) {\n" +
" //@ assert \\count == i; \n" +
......@@ -62,13 +64,13 @@ public class strict extends TCBase {
" void m(int[] a) { for (int i: a) {\n" +
" //@ assert \\values.size() >= 0; \n" +
" }}}"
,"/A.java:3: warning: The \\values construct is an OpenJML extension to JML and not allowed under " + opt,16
,"/A.java:3: warning: The \\values construct is an OpenJML extension to JML and not allowed under " + optjml,16
);
}
@Test
public void testValuesB() {
main.addOptions(opt + "=false");
main.addOptions(optjmlp);
helpTCF("A.java","public class A {\n" +
" void m(int[] a) { for (int i: a) {\n" +
" //@ assert \\values.size() >= 0; \n" +
......@@ -78,7 +80,7 @@ public class strict extends TCBase {
@Test
public void testExceptionB() {
main.addOptions(opt + "=false");
main.addOptions(optjmlp);
helpTCF("A.java","public class A {\n" +
" //@ signals (Exception) \\exception != null;\n" +
" void m(int[] a) {\n" +
......@@ -92,7 +94,7 @@ public class strict extends TCBase {
" //@ signals (Exception) \\exception != null;\n" +
" void m(int[] a) {\n" +
" }}"
,"/A.java:2: warning: The \\exception construct is an OpenJML extension to JML and not allowed under " + opt,26
,"/A.java:2: warning: The \\exception construct is an OpenJML extension to JML and not allowed under " + optjml,26
);
}
......@@ -102,13 +104,13 @@ public class strict extends TCBase {
" /*@ secret */ private int i;\n" +
" void m(int[] a) {\n" +
" }}"
,"/A.java:2: warning: The secret construct is an OpenJML extension to JML and not allowed under " + opt,6
,"/A.java:2: warning: The secret construct is an OpenJML extension to JML and not allowed under " + optjml,6
);
}
@Test
public void testSecretB() {
main.addOptions(opt + "=false");
main.addOptions(optjmlp);
helpTCF("A.java","public class A {\n" +
" /*@ secret */ private int i;\n" +
" void m(int[] a) {\n" +
......@@ -122,13 +124,13 @@ public class strict extends TCBase {
" //@ query\n" +
" int m() { return 0; \n" +
" }}"
,"/A.java:2: warning: The query construct is an OpenJML extension to JML and not allowed under " + opt,6
,"/A.java:2: warning: The query construct is an OpenJML extension to JML and not allowed under " + optjml,6
);
}
@Test
public void testQueryB() {
main.addOptions(opt + "=false");
main.addOptions(optjmlp);
helpTCF("A.java","public class A {\n" +
" //@ query\n" +
" int m() { return 0; \n" +
......@@ -142,13 +144,13 @@ public class strict extends TCBase {
" //@ assignable a[0..];\n" +
" int m(int[] a) { return 0; \n" +
" }}"
,"/A.java:2: warning: The storeref with implied end-of-range (a[i..]) construct is an OpenJML extension to JML and not allowed under " + opt,22
,"/A.java:2: warning: The storeref with implied end-of-range (a[i..]) construct is an OpenJML extension to JML and not allowed under " + optjml,22
);
}
@Test
public void testStoreRefB() {
main.addOptions(opt + "=false");
main.addOptions(optjmlp);
helpTCF("A.java","public class A {\n" +
" //@ assignable a[0..];\n" +
" int m(int[] a) { return 0; \n" +
......
......@@ -232,9 +232,9 @@ public class typechecking extends TCBase {
}
@Test public void testInvariantFor6() {
main.addOptions("-strictJML");
main.addOptions("-lang=jml");
helpTCF("A.java","public class A { int k; Integer i; void m() { \n//@ assert \\invariant_for(Integer,k);\n}}"
,"$SPECS/specs/java/util/stream/Stream.jml:60: warning: The \\count construct is an OpenJML extension to JML and not allowed under -strictJML",37
,"$SPECS/specs/java/util/stream/Stream.jml:60: warning: The \\count construct is an OpenJML extension to JML and not allowed under -lang=jml",37
,"/A.java:2: A \\invariant_for expression expects just 1 argument, not 2", 26
,"/A.java:2: The argument of \\invariant_for must be of reference type", 27
,"/A.java:2: The argument of \\invariant_for must be of reference type", 35
......@@ -248,9 +248,9 @@ public class typechecking extends TCBase {
}
@Test public void testInvariantFor7() {
main.addOptions("-strictJML");
main.addOptions("-lang=jml");
helpTCF("A.java","public class A { int k; Integer i; void m() { \n//@ assert \\invariant_for();\n}}"
,"$SPECS/specs/java/util/stream/Stream.jml:60: warning: The \\count construct is an OpenJML extension to JML and not allowed under -strictJML",37
,"$SPECS/specs/java/util/stream/Stream.jml:60: warning: The \\count construct is an OpenJML extension to JML and not allowed under -lang=jml",37
,"/A.java:2: A \\invariant_for expression expects just 1 argument, not 0", 26
);
}
......
$SPECS/specs/java/util/stream/Stream.jml:60: warning: The \count construct is an OpenJML extension to JML and not allowed under -strictJML
$SPECS/specs/java/util/stream/Stream.jml:60: warning: The \count construct is an OpenJML extension to JML and not allowed under -lang=jml
//@ loop_invariant i == \count && 0 <= i && i <= values.length;
^
1 warning
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment