unable to compile JML from CVS

[Melanie Harries]

Hi, I recently downloaded the JML2 source from the CVS repository along with the
other necessary libraries according to the developer-tips document.  When I try
to  compile JML I get several errors which I've pasted below.  I'm using the
most recent version of JML and MJ, and Java 1.4.2.  If anyone could provide any
incite into what I'm doing wrong I would appreciate it.

I'm working on a model checking tool and I'm hoping to access the JML parse tree
in order to turn method pre and post conditions into a format that my model
checker can use.  As I understand it, the suggested way of doing this is to
follow the example of the jmldoc tool, specifically from Main.java.  Because
Main.java extends org.jmlspecs.checker.Main, which is not included in the
OpenJML jars, I'm trying to build JML from the source provided via CVS.  Is
this still the suggested way of accessing the JML parse tree?

Thanks,
Melanie Harries

JmlPredicate.java:95: getFANonNulls(org.multijava.mjc.CContextType) in
org.jmlspecs.checker.JmlPredicate cannot override
getFANonNulls(org.multijava.mjc.CContextType) in org.multijava.mjc.JExpression;
attempting to use incompatible return type
found   : java.lang.Object[]
required: org.multijava.mjc.JExpression[]
    public /*@pure non_null*/ Object[] getFANonNulls(/*@non_null@*/ CContextType
context) {
                                       ^
JmlPredicate.java:98: getFANulls(org.multijava.mjc.CContextType) in
org.jmlspecs.checker.JmlPredicate cannot override
getFANulls(org.multijava.mjc.CContextType) in org.multijava.mjc.JExpression;
attempting to use incompatible return type
found   : java.lang.Object[]
required: org.multijava.mjc.JExpression[]
    public /*@pure non_null*/ Object[] getFANulls(/*@non_null@*/ CContextType
context) {
                                       ^
JmlContext.java:424: getFANulls() in org.jmlspecs.checker.JmlContext cannot
implement getFANulls() in org.multijava.mjc.CContextType; attempting to use
incompatible return type
found   : java.lang.Object[]
required: org.multijava.mjc.JPhylum[]
     public /*@pure non_null*/ Object[] getFANulls() {
                                        ^
JmlContext.java:421: getFANonNulls() in org.jmlspecs.checker.JmlContext cannot
implement getFANonNulls() in org.multijava.mjc.CContextType; attempting to use
incompatible return type
found   : java.lang.Object[]
required: org.multijava.mjc.JPhylum[]
     public /*@pure non_null*/ Object[] getFANonNulls() {
                                        ^
JmlContext.java:411: isFANonNull(org.multijava.mjc.JPhylum) in
org.multijava.mjc.CContextNullity cannot be applied to
(org.multijava.mjc.CField)
          return
getContextNullity().isFANonNull(((CFieldAccessor)expr).getField());
                                  ^
JmlContext.java:413: isFANonNull(org.multijava.mjc.JPhylum) in
org.multijava.mjc.CContextNullity cannot be applied to
(org.multijava.mjc.CField)
          return getContextNullity().isFANonNull((CField)expr);
                                  ^
JmlContext.java:431: addFANonNull(org.multijava.mjc.JPhylum) in
org.multijava.mjc.CContextNullity cannot be applied to (java.lang.Object)
       getContextNullity().addFANonNull(expr);
                        ^
JmlContext.java:434: addFANull(org.multijava.mjc.JPhylum) in
org.multijava.mjc.CContextNullity cannot be applied to (java.lang.Object)
       getContextNullity().addFANull(expr);
                        ^
JmlContext.java:437: removeFANonNull(org.multijava.mjc.JPhylum) in
org.multijava.mjc.CContextNullity cannot be applied to (java.lang.Object)
       getContextNullity().removeFANonNull(expr);
                        ^
JmlContext.java:446: addFANonNulls(org.multijava.mjc.JPhylum[]) in
org.multijava.mjc.CContextNullity cannot be applied to (java.lang.Object[])
       getContextNullity().addFANonNulls(exprs);
                        ^
JmlContext.java:449: addFANulls(org.multijava.mjc.JPhylum[]) in
org.multijava.mjc.CContextNullity cannot be applied to (java.lang.Object[])
       getContextNullity().addFANulls(exprs);
                        ^
JmlExpressionContext.java:85: org.jmlspecs.checker.JmlExpressionContext is not
abstract and does not override abstract method
addFANulls(org.multijava.mjc.JPhylum[]) in org.multijava.mjc.CContextType
public class JmlExpressionContext extends JmlContext
       ^
JmlSpecExpression.java:68: getFANonNulls(org.multijava.mjc.CContextType) in
org.jmlspecs.checker.JmlSpecExpression cannot override
getFANonNulls(org.multijava.mjc.CContextType) in org.multijava.mjc.JExpression;
attempting to use incompatible return type
found   : java.lang.Object[]
required: org.multijava.mjc.JExpression[]
    public /*@pure non_null*/ Object[] getFANonNulls(/*@non_null@*/ CContextType
context) {
                                       ^
JmlSpecExpression.java:71: getFANulls(org.multijava.mjc.CContextType) in
org.jmlspecs.checker.JmlSpecExpression cannot override
getFANulls(org.multijava.mjc.CContextType) in org.multijava.mjc.JExpression;
attempting to use incompatible return type
found   : java.lang.Object[]
required: org.multijava.mjc.JExpression[]
    public /*@pure non_null*/ Object[] getFANulls(/*@non_null@*/ CContextType
context) {
                                       ^
JmlAssertOrAssumeStatement.java:123: addFANonNulls(org.multijava.mjc.JPhylum[])
in org.multijava.mjc.CContextType cannot be applied to (java.lang.Object[])
            context.addFANonNulls(predicate.getFANonNulls(ectx));
                   ^
JmlAssertOrAssumeStatement.java:124: addFANulls(org.multijava.mjc.JPhylum[]) in
org.multijava.mjc.CContextType cannot be applied to (java.lang.Object[])
            context.addFANulls(predicate.getFANulls(ectx));
                   ^
JmlTypeDeclaration.java:149: cannot resolve symbol
symbol  : method typevariables ()
location: class org.multijava.mjc.JTypeDeclaration
    return delegee.typevariables();
                  ^
JmlMethodDeclaration.java:125: cannot resolve symbol
symbol  : method typevariables ()
location: class org.multijava.mjc.JMethodDeclaration
        return delegee.typevariables();
                      ^
JmlIsInitializedExpression.java:47: cannot resolve symbol
symbol  : variable CUniverseServices
location: class org.jmlspecs.checker.JmlIsInitializedExpression
        this.referenceType =
CUniverseServices.setDefaultVariable(referenceType);
                             ^
JmlReachExpression.java:60: cannot resolve symbol
symbol  : variable CUniverseServices
location: class org.jmlspecs.checker.JmlReachExpression
        this.referenceType =
CUniverseServices.setDefaultVariable(referenceType);
                             ^
JmlSetComprehension.java:67: cannot resolve symbol
symbol  : variable CUniverseServices
location: class org.jmlspecs.checker.JmlSetComprehension
        this.type = CUniverseServices.setDefaultVariable(type);
                    ^
JmlSetComprehension.java:68: cannot resolve symbol
symbol  : variable CUniverseServices
location: class org.jmlspecs.checker.JmlSetComprehension
        this.memberType = CUniverseServices.setDefaultVariable(memberType);
                          ^
JmlTypeExpression.java:44: cannot resolve symbol
symbol  : variable CUniverseServices
location: class org.jmlspecs.checker.JmlTypeExpression
        this.type = CUniverseServices.setDefaultVariable(type);
                    ^
JmlArrayDimsAndInits.java:74: cannot resolve symbol
symbol  : constructor JArrayDimsAndInits
(org.multijava.util.compiler.TokenReference,org.multijava.mjc.CUniverse,org.multijava.mjc.CUniverse,org.multijava.mjc.JExpression[],org.multijava.mjc.JArrayInitializer)
location: class org.multijava.mjc.JArrayDimsAndInits
        super(where, array_univ, elem_univ, dims, init);
        ^
JmlArrayDimsAndInits.java:87: cannot resolve symbol
symbol  : method isNonNull (org.multijava.mjc.CContextType)
location: class org.multijava.mjc.JArrayDimsAndInits
               return super.isNonNull(context);
                           ^
JmlArrayDimsAndInits.java:120: cannot resolve symbol
symbol  : method isNonNull (org.multijava.mjc.CExpressionContextType)
location: class org.multijava.mjc.JArrayDimsAndInits
                       !this.isNonNull(context) || super.isNonNull(context),
                                                        ^
JmlMethodContext.java:38: org.jmlspecs.checker.JmlMethodContext is not abstract
and does not override abstract method addFANulls(org.multijava.mjc.JPhylum[])
in org.multijava.mjc.CContextType
public class JmlMethodContext extends JmlContext
       ^
JmlConstructorContext.java:35: org.jmlspecs.checker.JmlConstructorContext is not
abstract and does not override abstract method
addFANulls(org.multijava.mjc.JPhylum[]) in org.multijava.mjc.CContextType
public class JmlConstructorContext extends JmlMethodContext
       ^
JmlFlowControlContext.java:40: org.jmlspecs.checker.JmlFlowControlContext is not
abstract and does not override abstract method
addFANulls(org.multijava.mjc.JPhylum[]) in org.multijava.mjc.CContextType
public class JmlFlowControlContext extends JmlContext
       ^
JmlFlowControlContext.java:507: getFANulls() in
org.jmlspecs.checker.JmlFlowControlContext cannot implement getFANulls() in
org.multijava.mjc.CContextType; attempting to use incompatible return type
found   : java.lang.Object[]
required: org.multijava.mjc.JPhylum[]
     public /*@pure*/ Object[] getFANulls() {
                               ^
JmlFlowControlContext.java:504: getFANonNulls() in
org.jmlspecs.checker.JmlFlowControlContext cannot implement getFANonNulls() in
org.multijava.mjc.CContextType; attempting to use incompatible return type
found   : java.lang.Object[]
required: org.multijava.mjc.JPhylum[]
     public /*@pure*/ Object[] getFANonNulls() {
                               ^
JmlFlowControlContext.java:498: isFANonNull(org.multijava.mjc.JPhylum) in
org.multijava.mjc.CContext cannot be applied to (java.lang.Object)
          return ((CFlowControlContext)delegee).isFANonNull(expr);
                 ^
JmlFlowControlContext.java:515: addFANonNull(org.multijava.mjc.JPhylum) in
org.multijava.mjc.CContext cannot be applied to (java.lang.Object)
       ((CFlowControlContext)delegee).addFANonNull(expr);
       ^
JmlFlowControlContext.java:518: addFANull(org.multijava.mjc.JPhylum) in
org.multijava.mjc.CContext cannot be applied to (java.lang.Object)
       ((CFlowControlContext)delegee).addFANull(expr);
       ^
JmlFlowControlContext.java:521: removeFANonNull(org.multijava.mjc.JPhylum) in
org.multijava.mjc.CContext cannot be applied to (java.lang.Object)
       ((CFlowControlContext)delegee).removeFANonNull(expr);
       ^
JmlFlowControlContext.java:532: addFANonNulls(org.multijava.mjc.JPhylum[]) in
org.multijava.mjc.CContext cannot be applied to (java.lang.Object[])
       ((CFlowControlContext)delegee).addFANonNulls(exprs);
       ^
JmlFlowControlContext.java:536: addFANulls(org.multijava.mjc.JPhylum[]) in
org.multijava.mjc.CContext cannot be applied to (java.lang.Object[])
       ((CFlowControlContext)delegee).addFANulls(exprs);
       ^
JmlInitializerContext.java:33: org.jmlspecs.checker.JmlInitializerContext is not
abstract and does not override abstract method
addFANulls(org.multijava.mjc.JPhylum[]) in org.multijava.mjc.CContextType
public class JmlInitializerContext extends JmlMethodContext
       ^
JMethodDeclarationWrapper.java:121: cannot resolve symbol
symbol  : method typevariables ()
location: class org.jmlspecs.checker.JMethodDeclarationWrapper
                                      typevariables(),
                                      ^
JmlClassContext.java:35: org.jmlspecs.checker.JmlClassContext is not abstract
and does not override abstract method addFANulls(org.multijava.mjc.JPhylum[])
in org.multijava.mjc.CContextType
public class JmlClassContext extends JmlContext implements CClassContextType
       ^
JmlCompilationUnitContext.java:35:
org.jmlspecs.checker.JmlCompilationUnitContext is not abstract and does not
override abstract method addFANulls(org.multijava.mjc.JPhylum[]) in
org.multijava.mjc.CContextType
public class JmlCompilationUnitContext extends JmlContext
       ^
JmlInterfaceContext.java:34: org.jmlspecs.checker.JmlInterfaceContext is not
abstract and does not override abstract method
addFANulls(org.multijava.mjc.JPhylum[]) in org.multijava.mjc.CContextType
public class JmlInterfaceContext extends JmlClassContext
       ^
JmlParser.java:14138: jBuiltInTypeSpec(org.multijava.mjc.CUniverse) in
org.jmlspecs.checker.JmlParser cannot be applied to (<nulltype>,<nulltype>)
                                        jBuiltInTypeSpec(null,null);
                                        ^
JmlParser.java:14183: jBuiltInTypeSpec(org.multijava.mjc.CUniverse) in
org.jmlspecs.checker.JmlParser cannot be applied to
(<nulltype>,org.multijava.mjc.CUniverse)
                                dest=jBuiltInTypeSpec(null, array_univ);
                                     ^
JmlParser.java:14233: jBuiltInTypeSpec(org.multijava.mjc.CUniverse) in
org.jmlspecs.checker.JmlParser cannot be applied to (<nulltype>,<nulltype>)
                                                jBuiltInTypeSpec(null,null);
                                                ^
JmlParser.java:14279: jBuiltInTypeSpec(org.multijava.mjc.CUniverse) in
org.jmlspecs.checker.JmlParser cannot be applied to
(org.multijava.mjc.CUniverse,org.multijava.mjc.CUniverse)
                                        dest=jBuiltInTypeSpec(elem_univ,
array_univ);
                                             ^
JmlParser.java:17212: cannot resolve symbol
symbol  : constructor JArrayDimsAndInits
(org.multijava.util.compiler.TokenReference,org.multijava.mjc.CUniverse,org.multijava.mjc.CUniverse,org.multijava.mjc.JExpression[],org.multijava.mjc.JArrayInitializer)
location: class org.multijava.mjc.JArrayDimsAndInits
                                new   JArrayDimsAndInits(
utility.buildTokenReference(), array_univ, elem_univ, args, init) :
                                ^
47 errors



-------------------------------------------------------------------------
Check out the new SourceForge.net Marketplace.
It's the best place to buy or sell services for
just about anything Open Source.
http://sourceforge.net/services/buy/index.php
_______________________________________________
Jmlspecs-developers mailing list
Jmlspecs-developers@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-developers

[Gary T. Leavens-2]

Hi Melanie,

I'm not sure what the OpenJML jars have to do with this.  Are they in
your class path?

I haven't built JML2 in a few days, so I'll try building it again and will
let you know I I have a similar problem, but I haven't seen that.  But
the last time I did a build, I didn't see anything like the errors you
are having.

On Wed, 18 Jun 2008, Melanie Harries wrote:

> Hi, I recently downloaded the JML2 source from the CVS repository along with the
> other necessary libraries according to the developer-tips document.  When I try
> to  compile JML I get several errors which I've pasted below.  I'm using the
> most recent version of JML and MJ, and Java 1.4.2.  If anyone could provide any
> incite into what I'm doing wrong I would appreciate it.
>
> I'm working on a model checking tool and I'm hoping to access the JML parse tree
> in order to turn method pre and post conditions into a format that my model
> checker can use.  As I understand it, the suggested way of doing this is to
> follow the example of the jmldoc tool, specifically from Main.java.  Because
> Main.java extends org.jmlspecs.checker.Main, which is not included in the
> OpenJML jars, I'm trying to build JML from the source provided via CVS.  Is
> this still the suggested way of accessing the JML parse tree?
>
> Thanks,
> Melanie Harries
>
> JmlPredicate.java:95: getFANonNulls(org.multijava.mjc.CContextType) in
> org.jmlspecs.checker.JmlPredicate cannot override
> getFANonNulls(org.multijava.mjc.CContextType) in org.multijava.mjc.JExpression;
> attempting to use incompatible return type
> found   : java.lang.Object[]
> required: org.multijava.mjc.JExpression[]
>    public /*@pure non_null*/ Object[] getFANonNulls(/*@non_null@*/ CContextType
> context) {
>                                       ^
> JmlPredicate.java:98: getFANulls(org.multijava.mjc.CContextType) in
> org.jmlspecs.checker.JmlPredicate cannot override
> getFANulls(org.multijava.mjc.CContextType) in org.multijava.mjc.JExpression;
> attempting to use incompatible return type
> found   : java.lang.Object[]
> required: org.multijava.mjc.JExpression[]
>    public /*@pure non_null*/ Object[] getFANulls(/*@non_null@*/ CContextType
> context) {
>                                       ^
> JmlContext.java:424: getFANulls() in org.jmlspecs.checker.JmlContext cannot
> implement getFANulls() in org.multijava.mjc.CContextType; attempting to use
> incompatible return type
> found   : java.lang.Object[]
> required: org.multijava.mjc.JPhylum[]
>     public /*@pure non_null*/ Object[] getFANulls() {
>                                        ^
> JmlContext.java:421: getFANonNulls() in org.jmlspecs.checker.JmlContext cannot
> implement getFANonNulls() in org.multijava.mjc.CContextType; attempting to use
> incompatible return type
> found   : java.lang.Object[]
> required: org.multijava.mjc.JPhylum[]
>     public /*@pure non_null*/ Object[] getFANonNulls() {
>                                        ^
> JmlContext.java:411: isFANonNull(org.multijava.mjc.JPhylum) in
> org.multijava.mjc.CContextNullity cannot be applied to
> (org.multijava.mjc.CField)
>          return
> getContextNullity().isFANonNull(((CFieldAccessor)expr).getField());
>                                  ^
> JmlContext.java:413: isFANonNull(org.multijava.mjc.JPhylum) in
> org.multijava.mjc.CContextNullity cannot be applied to
> (org.multijava.mjc.CField)
>          return getContextNullity().isFANonNull((CField)expr);
>                                  ^
> JmlContext.java:431: addFANonNull(org.multijava.mjc.JPhylum) in
> org.multijava.mjc.CContextNullity cannot be applied to (java.lang.Object)
>       getContextNullity().addFANonNull(expr);
>                        ^
> JmlContext.java:434: addFANull(org.multijava.mjc.JPhylum) in
> org.multijava.mjc.CContextNullity cannot be applied to (java.lang.Object)
>       getContextNullity().addFANull(expr);
>                        ^
> JmlContext.java:437: removeFANonNull(org.multijava.mjc.JPhylum) in
> org.multijava.mjc.CContextNullity cannot be applied to (java.lang.Object)
>       getContextNullity().removeFANonNull(expr);
>                        ^
> JmlContext.java:446: addFANonNulls(org.multijava.mjc.JPhylum[]) in
> org.multijava.mjc.CContextNullity cannot be applied to (java.lang.Object[])
>       getContextNullity().addFANonNulls(exprs);
>                        ^
> JmlContext.java:449: addFANulls(org.multijava.mjc.JPhylum[]) in
> org.multijava.mjc.CContextNullity cannot be applied to (java.lang.Object[])
>       getContextNullity().addFANulls(exprs);
>                        ^
> JmlExpressionContext.java:85: org.jmlspecs.checker.JmlExpressionContext is not
> abstract and does not override abstract method
> addFANulls(org.multijava.mjc.JPhylum[]) in org.multijava.mjc.CContextType
> public class JmlExpressionContext extends JmlContext
>       ^
> JmlSpecExpression.java:68: getFANonNulls(org.multijava.mjc.CContextType) in
> org.jmlspecs.checker.JmlSpecExpression cannot override
> getFANonNulls(org.multijava.mjc.CContextType) in org.multijava.mjc.JExpression;
> attempting to use incompatible return type
> found   : java.lang.Object[]
> required: org.multijava.mjc.JExpression[]
>    public /*@pure non_null*/ Object[] getFANonNulls(/*@non_null@*/ CContextType
> context) {
>                                       ^
> JmlSpecExpression.java:71: getFANulls(org.multijava.mjc.CContextType) in
> org.jmlspecs.checker.JmlSpecExpression cannot override
> getFANulls(org.multijava.mjc.CContextType) in org.multijava.mjc.JExpression;
> attempting to use incompatible return type
> found   : java.lang.Object[]
> required: org.multijava.mjc.JExpression[]
>    public /*@pure non_null*/ Object[] getFANulls(/*@non_null@*/ CContextType
> context) {
>                                       ^
> JmlAssertOrAssumeStatement.java:123: addFANonNulls(org.multijava.mjc.JPhylum[])
> in org.multijava.mjc.CContextType cannot be applied to (java.lang.Object[])
>            context.addFANonNulls(predicate.getFANonNulls(ectx));
>                   ^
> JmlAssertOrAssumeStatement.java:124: addFANulls(org.multijava.mjc.JPhylum[]) in
> org.multijava.mjc.CContextType cannot be applied to (java.lang.Object[])
>            context.addFANulls(predicate.getFANulls(ectx));
>                   ^
> JmlTypeDeclaration.java:149: cannot resolve symbol
> symbol  : method typevariables ()
> location: class org.multijava.mjc.JTypeDeclaration
>    return delegee.typevariables();
>                  ^
> JmlMethodDeclaration.java:125: cannot resolve symbol
> symbol  : method typevariables ()
> location: class org.multijava.mjc.JMethodDeclaration
>        return delegee.typevariables();
>                      ^
> JmlIsInitializedExpression.java:47: cannot resolve symbol
> symbol  : variable CUniverseServices
> location: class org.jmlspecs.checker.JmlIsInitializedExpression
>        this.referenceType =
> CUniverseServices.setDefaultVariable(referenceType);
>                             ^
> JmlReachExpression.java:60: cannot resolve symbol
> symbol  : variable CUniverseServices
> location: class org.jmlspecs.checker.JmlReachExpression
>        this.referenceType =
> CUniverseServices.setDefaultVariable(referenceType);
>                             ^
> JmlSetComprehension.java:67: cannot resolve symbol
> symbol  : variable CUniverseServices
> location: class org.jmlspecs.checker.JmlSetComprehension
>        this.type = CUniverseServices.setDefaultVariable(type);
>                    ^
> JmlSetComprehension.java:68: cannot resolve symbol
> symbol  : variable CUniverseServices
> location: class org.jmlspecs.checker.JmlSetComprehension
>        this.memberType = CUniverseServices.setDefaultVariable(memberType);
>                          ^
> JmlTypeExpression.java:44: cannot resolve symbol
> symbol  : variable CUniverseServices
> location: class org.jmlspecs.checker.JmlTypeExpression
>        this.type = CUniverseServices.setDefaultVariable(type);
>                    ^
> JmlArrayDimsAndInits.java:74: cannot resolve symbol
> symbol  : constructor JArrayDimsAndInits
> (org.multijava.util.compiler.TokenReference,org.multijava.mjc.CUniverse,org.multijava.mjc.CUniverse,org.multijava.mjc.JExpression[],org.multijava.mjc.JArrayInitializer)
> location: class org.multijava.mjc.JArrayDimsAndInits
>        super(where, array_univ, elem_univ, dims, init);
>        ^
> JmlArrayDimsAndInits.java:87: cannot resolve symbol
> symbol  : method isNonNull (org.multijava.mjc.CContextType)
> location: class org.multijava.mjc.JArrayDimsAndInits
>               return super.isNonNull(context);
>                           ^
> JmlArrayDimsAndInits.java:120: cannot resolve symbol
> symbol  : method isNonNull (org.multijava.mjc.CExpressionContextType)
> location: class org.multijava.mjc.JArrayDimsAndInits
>                       !this.isNonNull(context) || super.isNonNull(context),
>                                                        ^
> JmlMethodContext.java:38: org.jmlspecs.checker.JmlMethodContext is not abstract
> and does not override abstract method addFANulls(org.multijava.mjc.JPhylum[])
> in org.multijava.mjc.CContextType
> public class JmlMethodContext extends JmlContext
>       ^
> JmlConstructorContext.java:35: org.jmlspecs.checker.JmlConstructorContext is not
> abstract and does not override abstract method
> addFANulls(org.multijava.mjc.JPhylum[]) in org.multijava.mjc.CContextType
> public class JmlConstructorContext extends JmlMethodContext
>       ^
> JmlFlowControlContext.java:40: org.jmlspecs.checker.JmlFlowControlContext is not
> abstract and does not override abstract method
> addFANulls(org.multijava.mjc.JPhylum[]) in org.multijava.mjc.CContextType
> public class JmlFlowControlContext extends JmlContext
>       ^
> JmlFlowControlContext.java:507: getFANulls() in
> org.jmlspecs.checker.JmlFlowControlContext cannot implement getFANulls() in
> org.multijava.mjc.CContextType; attempting to use incompatible return type
> found   : java.lang.Object[]
> required: org.multijava.mjc.JPhylum[]
>     public /*@pure*/ Object[] getFANulls() {
>                               ^
> JmlFlowControlContext.java:504: getFANonNulls() in
> org.jmlspecs.checker.JmlFlowControlContext cannot implement getFANonNulls() in
> org.multijava.mjc.CContextType; attempting to use incompatible return type
> found   : java.lang.Object[]
> required: org.multijava.mjc.JPhylum[]
>     public /*@pure*/ Object[] getFANonNulls() {
>                               ^
> JmlFlowControlContext.java:498: isFANonNull(org.multijava.mjc.JPhylum) in
> org.multijava.mjc.CContext cannot be applied to (java.lang.Object)
>          return ((CFlowControlContext)delegee).isFANonNull(expr);
>                 ^
> JmlFlowControlContext.java:515: addFANonNull(org.multijava.mjc.JPhylum) in
> org.multijava.mjc.CContext cannot be applied to (java.lang.Object)
>       ((CFlowControlContext)delegee).addFANonNull(expr);
>       ^
> JmlFlowControlContext.java:518: addFANull(org.multijava.mjc.JPhylum) in
> org.multijava.mjc.CContext cannot be applied to (java.lang.Object)
>       ((CFlowControlContext)delegee).addFANull(expr);
>       ^
> JmlFlowControlContext.java:521: removeFANonNull(org.multijava.mjc.JPhylum) in
> org.multijava.mjc.CContext cannot be applied to (java.lang.Object)
>       ((CFlowControlContext)delegee).removeFANonNull(expr);
>       ^
> JmlFlowControlContext.java:532: addFANonNulls(org.multijava.mjc.JPhylum[]) in
> org.multijava.mjc.CContext cannot be applied to (java.lang.Object[])
>       ((CFlowControlContext)delegee).addFANonNulls(exprs);
>       ^
> JmlFlowControlContext.java:536: addFANulls(org.multijava.mjc.JPhylum[]) in
> org.multijava.mjc.CContext cannot be applied to (java.lang.Object[])
>       ((CFlowControlContext)delegee).addFANulls(exprs);
>       ^
> JmlInitializerContext.java:33: org.jmlspecs.checker.JmlInitializerContext is not
> abstract and does not override abstract method
> addFANulls(org.multijava.mjc.JPhylum[]) in org.multijava.mjc.CContextType
> public class JmlInitializerContext extends JmlMethodContext
>       ^
> JMethodDeclarationWrapper.java:121: cannot resolve symbol
> symbol  : method typevariables ()
> location: class org.jmlspecs.checker.JMethodDeclarationWrapper
>                                      typevariables(),
>                                      ^
> JmlClassContext.java:35: org.jmlspecs.checker.JmlClassContext is not abstract
> and does not override abstract method addFANulls(org.multijava.mjc.JPhylum[])
> in org.multijava.mjc.CContextType
> public class JmlClassContext extends JmlContext implements CClassContextType
>       ^
> JmlCompilationUnitContext.java:35:
> org.jmlspecs.checker.JmlCompilationUnitContext is not abstract and does not
> override abstract method addFANulls(org.multijava.mjc.JPhylum[]) in
> org.multijava.mjc.CContextType
> public class JmlCompilationUnitContext extends JmlContext
>       ^
> JmlInterfaceContext.java:34: org.jmlspecs.checker.JmlInterfaceContext is not
> abstract and does not override abstract method
> addFANulls(org.multijava.mjc.JPhylum[]) in org.multijava.mjc.CContextType
> public class JmlInterfaceContext extends JmlClassContext
>       ^
> JmlParser.java:14138: jBuiltInTypeSpec(org.multijava.mjc.CUniverse) in
> org.jmlspecs.checker.JmlParser cannot be applied to (<nulltype>,<nulltype>)
>                                        jBuiltInTypeSpec(null,null);
>                                        ^
> JmlParser.java:14183: jBuiltInTypeSpec(org.multijava.mjc.CUniverse) in
> org.jmlspecs.checker.JmlParser cannot be applied to
> (<nulltype>,org.multijava.mjc.CUniverse)
>                                dest=jBuiltInTypeSpec(null, array_univ);
>                                     ^
> JmlParser.java:14233: jBuiltInTypeSpec(org.multijava.mjc.CUniverse) in
> org.jmlspecs.checker.JmlParser cannot be applied to (<nulltype>,<nulltype>)
>                                                jBuiltInTypeSpec(null,null);
>                                                ^
> JmlParser.java:14279: jBuiltInTypeSpec(org.multijava.mjc.CUniverse) in
> org.jmlspecs.checker.JmlParser cannot be applied to
> (org.multijava.mjc.CUniverse,org.multijava.mjc.CUniverse)
>                                        dest=jBuiltInTypeSpec(elem_univ,
> array_univ);
>                                             ^
> JmlParser.java:17212: cannot resolve symbol
> symbol  : constructor JArrayDimsAndInits
> (org.multijava.util.compiler.TokenReference,org.multijava.mjc.CUniverse,org.multijava.mjc.CUniverse,org.multijava.mjc.JExpression[],org.multijava.mjc.JArrayInitializer)
> location: class org.multijava.mjc.JArrayDimsAndInits
>                                new   JArrayDimsAndInits(
> utility.buildTokenReference(), array_univ, elem_univ, args, init) :
>                                ^
> 47 errors
>
>
>
> -------------------------------------------------------------------------
> Check out the new SourceForge.net Marketplace.
> It's the best place to buy or sell services for
> just about anything Open Source.
> http://sourceforge.net/services/buy/index.php
> _______________________________________________
> Jmlspecs-developers mailing list
> Jmlspecs-developers@...
> https://lists.sourceforge.net/lists/listinfo/jmlspecs-developers
>

         Gary T. Leavens
         210 Harris Center (Bldg. 116)
         School of EECS, University of Central Florida
         4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
         http://www.eecs.ucf.edu/~leavens  phone: [phone]
         leavens@...

-------------------------------------------------------------------------
Check out the new SourceForge.net Marketplace.
It's the best place to buy or sell services for
just about anything Open Source.
http://sourceforge.net/services/buy/index.php
_______________________________________________
Jmlspecs-developers mailing list
Jmlspecs-developers@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-developers

[Gary T. Leavens-2]

Hi Melanie,

I have no problems at all with building JML2 from sources using JDK
1.4.2_17.  If aking OpenJML out of your CLASSPATH doesn't help, please
send me your JDK version and your CLASSPATH along with your your
sourceme file and I'll see if I can tell anything about it.

BTW, we are in the process of building a new version of JML's parser.
See the JML4 pages from the JML Wiki at sourceforge.net for more about
it.

On Wed, 18 Jun 2008, Melanie Harries wrote:

> Hi, I recently downloaded the JML2 source from the CVS repository along with the
> other necessary libraries according to the developer-tips document.  When I try
> to  compile JML I get several errors which I've pasted below.  I'm using the
> most recent version of JML and MJ, and Java 1.4.2.  If anyone could provide any
> incite into what I'm doing wrong I would appreciate it.
>
> I'm working on a model checking tool and I'm hoping to access the JML parse tree
> in order to turn method pre and post conditions into a format that my model
> checker can use.  As I understand it, the suggested way of doing this is to
> follow the example of the jmldoc tool, specifically from Main.java.  Because
> Main.java extends org.jmlspecs.checker.Main, which is not included in the
> OpenJML jars, I'm trying to build JML from the source provided via CVS.  Is
> this still the suggested way of accessing the JML parse tree?
>
> Thanks,
> Melanie Harries
>
> JmlPredicate.java:95: getFANonNulls(org.multijava.mjc.CContextType) in
> org.jmlspecs.checker.JmlPredicate cannot override
> getFANonNulls(org.multijava.mjc.CContextType) in org.multijava.mjc.JExpression;
> attempting to use incompatible return type
> found   : java.lang.Object[]
> required: org.multijava.mjc.JExpression[]
>    public /*@pure non_null*/ Object[] getFANonNulls(/*@non_null@*/ CContextType
> context) {
>                                       ^
> JmlPredicate.java:98: getFANulls(org.multijava.mjc.CContextType) in
> org.jmlspecs.checker.JmlPredicate cannot override
> getFANulls(org.multijava.mjc.CContextType) in org.multijava.mjc.JExpression;
> attempting to use incompatible return type
> found   : java.lang.Object[]
> required: org.multijava.mjc.JExpression[]
>    public /*@pure non_null*/ Object[] getFANulls(/*@non_null@*/ CContextType
> context) {
>                                       ^
> JmlContext.java:424: getFANulls() in org.jmlspecs.checker.JmlContext cannot
> implement getFANulls() in org.multijava.mjc.CContextType; attempting to use
> incompatible return type
> found   : java.lang.Object[]
> required: org.multijava.mjc.JPhylum[]
>     public /*@pure non_null*/ Object[] getFANulls() {
>                                        ^
> JmlContext.java:421: getFANonNulls() in org.jmlspecs.checker.JmlContext cannot
> implement getFANonNulls() in org.multijava.mjc.CContextType; attempting to use
> incompatible return type
> found   : java.lang.Object[]
> required: org.multijava.mjc.JPhylum[]
>     public /*@pure non_null*/ Object[] getFANonNulls() {
>                                        ^
> JmlContext.java:411: isFANonNull(org.multijava.mjc.JPhylum) in
> org.multijava.mjc.CContextNullity cannot be applied to
> (org.multijava.mjc.CField)
>          return
> getContextNullity().isFANonNull(((CFieldAccessor)expr).getField());
>                                  ^
> JmlContext.java:413: isFANonNull(org.multijava.mjc.JPhylum) in
> org.multijava.mjc.CContextNullity cannot be applied to
> (org.multijava.mjc.CField)
>          return getContextNullity().isFANonNull((CField)expr);
>                                  ^
> JmlContext.java:431: addFANonNull(org.multijava.mjc.JPhylum) in
> org.multijava.mjc.CContextNullity cannot be applied to (java.lang.Object)
>       getContextNullity().addFANonNull(expr);
>                        ^
> JmlContext.java:434: addFANull(org.multijava.mjc.JPhylum) in
> org.multijava.mjc.CContextNullity cannot be applied to (java.lang.Object)
>       getContextNullity().addFANull(expr);
>                        ^
> JmlContext.java:437: removeFANonNull(org.multijava.mjc.JPhylum) in
> org.multijava.mjc.CContextNullity cannot be applied to (java.lang.Object)
>       getContextNullity().removeFANonNull(expr);
>                        ^
> JmlContext.java:446: addFANonNulls(org.multijava.mjc.JPhylum[]) in
> org.multijava.mjc.CContextNullity cannot be applied to (java.lang.Object[])
>       getContextNullity().addFANonNulls(exprs);
>                        ^
> JmlContext.java:449: addFANulls(org.multijava.mjc.JPhylum[]) in
> org.multijava.mjc.CContextNullity cannot be applied to (java.lang.Object[])
>       getContextNullity().addFANulls(exprs);
>                        ^
> JmlExpressionContext.java:85: org.jmlspecs.checker.JmlExpressionContext is not
> abstract and does not override abstract method
> addFANulls(org.multijava.mjc.JPhylum[]) in org.multijava.mjc.CContextType
> public class JmlExpressionContext extends JmlContext
>       ^
> JmlSpecExpression.java:68: getFANonNulls(org.multijava.mjc.CContextType) in
> org.jmlspecs.checker.JmlSpecExpression cannot override
> getFANonNulls(org.multijava.mjc.CContextType) in org.multijava.mjc.JExpression;
> attempting to use incompatible return type
> found   : java.lang.Object[]
> required: org.multijava.mjc.JExpression[]
>    public /*@pure non_null*/ Object[] getFANonNulls(/*@non_null@*/ CContextType
> context) {
>                                       ^
> JmlSpecExpression.java:71: getFANulls(org.multijava.mjc.CContextType) in
> org.jmlspecs.checker.JmlSpecExpression cannot override
> getFANulls(org.multijava.mjc.CContextType) in org.multijava.mjc.JExpression;
> attempting to use incompatible return type
> found   : java.lang.Object[]
> required: org.multijava.mjc.JExpression[]
>    public /*@pure non_null*/ Object[] getFANulls(/*@non_null@*/ CContextType
> context) {
>                                       ^
> JmlAssertOrAssumeStatement.java:123: addFANonNulls(org.multijava.mjc.JPhylum[])
> in org.multijava.mjc.CContextType cannot be applied to (java.lang.Object[])
>            context.addFANonNulls(predicate.getFANonNulls(ectx));
>                   ^
> JmlAssertOrAssumeStatement.java:124: addFANulls(org.multijava.mjc.JPhylum[]) in
> org.multijava.mjc.CContextType cannot be applied to (java.lang.Object[])
>            context.addFANulls(predicate.getFANulls(ectx));
>                   ^
> JmlTypeDeclaration.java:149: cannot resolve symbol
> symbol  : method typevariables ()
> location: class org.multijava.mjc.JTypeDeclaration
>    return delegee.typevariables();
>                  ^
> JmlMethodDeclaration.java:125: cannot resolve symbol
> symbol  : method typevariables ()
> location: class org.multijava.mjc.JMethodDeclaration
>        return delegee.typevariables();
>                      ^
> JmlIsInitializedExpression.java:47: cannot resolve symbol
> symbol  : variable CUniverseServices
> location: class org.jmlspecs.checker.JmlIsInitializedExpression
>        this.referenceType =
> CUniverseServices.setDefaultVariable(referenceType);
>                             ^
> JmlReachExpression.java:60: cannot resolve symbol
> symbol  : variable CUniverseServices
> location: class org.jmlspecs.checker.JmlReachExpression
>        this.referenceType =
> CUniverseServices.setDefaultVariable(referenceType);
>                             ^
> JmlSetComprehension.java:67: cannot resolve symbol
> symbol  : variable CUniverseServices
> location: class org.jmlspecs.checker.JmlSetComprehension
>        this.type = CUniverseServices.setDefaultVariable(type);
>                    ^
> JmlSetComprehension.java:68: cannot resolve symbol
> symbol  : variable CUniverseServices
> location: class org.jmlspecs.checker.JmlSetComprehension
>        this.memberType = CUniverseServices.setDefaultVariable(memberType);
>                          ^
> JmlTypeExpression.java:44: cannot resolve symbol
> symbol  : variable CUniverseServices
> location: class org.jmlspecs.checker.JmlTypeExpression
>        this.type = CUniverseServices.setDefaultVariable(type);
>                    ^
> JmlArrayDimsAndInits.java:74: cannot resolve symbol
> symbol  : constructor JArrayDimsAndInits
> (org.multijava.util.compiler.TokenReference,org.multijava.mjc.CUniverse,org.multijava.mjc.CUniverse,org.multijava.mjc.JExpression[],org.multijava.mjc.JArrayInitializer)
> location: class org.multijava.mjc.JArrayDimsAndInits
>        super(where, array_univ, elem_univ, dims, init);
>        ^
> JmlArrayDimsAndInits.java:87: cannot resolve symbol
> symbol  : method isNonNull (org.multijava.mjc.CContextType)
> location: class org.multijava.mjc.JArrayDimsAndInits
>               return super.isNonNull(context);
>                           ^
> JmlArrayDimsAndInits.java:120: cannot resolve symbol
> symbol  : method isNonNull (org.multijava.mjc.CExpressionContextType)
> location: class org.multijava.mjc.JArrayDimsAndInits
>                       !this.isNonNull(context) || super.isNonNull(context),
>                                                        ^
> JmlMethodContext.java:38: org.jmlspecs.checker.JmlMethodContext is not abstract
> and does not override abstract method addFANulls(org.multijava.mjc.JPhylum[])
> in org.multijava.mjc.CContextType
> public class JmlMethodContext extends JmlContext
>       ^
> JmlConstructorContext.java:35: org.jmlspecs.checker.JmlConstructorContext is not
> abstract and does not override abstract method
> addFANulls(org.multijava.mjc.JPhylum[]) in org.multijava.mjc.CContextType
> public class JmlConstructorContext extends JmlMethodContext
>       ^
> JmlFlowControlContext.java:40: org.jmlspecs.checker.JmlFlowControlContext is not
> abstract and does not override abstract method
> addFANulls(org.multijava.mjc.JPhylum[]) in org.multijava.mjc.CContextType
> public class JmlFlowControlContext extends JmlContext
>       ^
> JmlFlowControlContext.java:507: getFANulls() in
> org.jmlspecs.checker.JmlFlowControlContext cannot implement getFANulls() in
> org.multijava.mjc.CContextType; attempting to use incompatible return type
> found   : java.lang.Object[]
> required: org.multijava.mjc.JPhylum[]
>     public /*@pure*/ Object[] getFANulls() {
>                               ^
> JmlFlowControlContext.java:504: getFANonNulls() in
> org.jmlspecs.checker.JmlFlowControlContext cannot implement getFANonNulls() in
> org.multijava.mjc.CContextType; attempting to use incompatible return type
> found   : java.lang.Object[]
> required: org.multijava.mjc.JPhylum[]
>     public /*@pure*/ Object[] getFANonNulls() {
>                               ^
> JmlFlowControlContext.java:498: isFANonNull(org.multijava.mjc.JPhylum) in
> org.multijava.mjc.CContext cannot be applied to (java.lang.Object)
>          return ((CFlowControlContext)delegee).isFANonNull(expr);
>                 ^
> JmlFlowControlContext.java:515: addFANonNull(org.multijava.mjc.JPhylum) in
> org.multijava.mjc.CContext cannot be applied to (java.lang.Object)
>       ((CFlowControlContext)delegee).addFANonNull(expr);
>       ^
> JmlFlowControlContext.java:518: addFANull(org.multijava.mjc.JPhylum) in
> org.multijava.mjc.CContext cannot be applied to (java.lang.Object)
>       ((CFlowControlContext)delegee).addFANull(expr);
>       ^
> JmlFlowControlContext.java:521: removeFANonNull(org.multijava.mjc.JPhylum) in
> org.multijava.mjc.CContext cannot be applied to (java.lang.Object)
>       ((CFlowControlContext)delegee).removeFANonNull(expr);
>       ^
> JmlFlowControlContext.java:532: addFANonNulls(org.multijava.mjc.JPhylum[]) in
> org.multijava.mjc.CContext cannot be applied to (java.lang.Object[])
>       ((CFlowControlContext)delegee).addFANonNulls(exprs);
>       ^
> JmlFlowControlContext.java:536: addFANulls(org.multijava.mjc.JPhylum[]) in
> org.multijava.mjc.CContext cannot be applied to (java.lang.Object[])
>       ((CFlowControlContext)delegee).addFANulls(exprs);
>       ^
> JmlInitializerContext.java:33: org.jmlspecs.checker.JmlInitializerContext is not
> abstract and does not override abstract method
> addFANulls(org.multijava.mjc.JPhylum[]) in org.multijava.mjc.CContextType
> public class JmlInitializerContext extends JmlMethodContext
>       ^
> JMethodDeclarationWrapper.java:121: cannot resolve symbol
> symbol  : method typevariables ()
> location: class org.jmlspecs.checker.JMethodDeclarationWrapper
>                                      typevariables(),
>                                      ^
> JmlClassContext.java:35: org.jmlspecs.checker.JmlClassContext is not abstract
> and does not override abstract method addFANulls(org.multijava.mjc.JPhylum[])
> in org.multijava.mjc.CContextType
> public class JmlClassContext extends JmlContext implements CClassContextType
>       ^
> JmlCompilationUnitContext.java:35:
> org.jmlspecs.checker.JmlCompilationUnitContext is not abstract and does not
> override abstract method addFANulls(org.multijava.mjc.JPhylum[]) in
> org.multijava.mjc.CContextType
> public class JmlCompilationUnitContext extends JmlContext
>       ^
> JmlInterfaceContext.java:34: org.jmlspecs.checker.JmlInterfaceContext is not
> abstract and does not override abstract method
> addFANulls(org.multijava.mjc.JPhylum[]) in org.multijava.mjc.CContextType
> public class JmlInterfaceContext extends JmlClassContext
>       ^
> JmlParser.java:14138: jBuiltInTypeSpec(org.multijava.mjc.CUniverse) in
> org.jmlspecs.checker.JmlParser cannot be applied to (<nulltype>,<nulltype>)
>                                        jBuiltInTypeSpec(null,null);
>                                        ^
> JmlParser.java:14183: jBuiltInTypeSpec(org.multijava.mjc.CUniverse) in
> org.jmlspecs.checker.JmlParser cannot be applied to
> (<nulltype>,org.multijava.mjc.CUniverse)
>                                dest=jBuiltInTypeSpec(null, array_univ);
>                                     ^
> JmlParser.java:14233: jBuiltInTypeSpec(org.multijava.mjc.CUniverse) in
> org.jmlspecs.checker.JmlParser cannot be applied to (<nulltype>,<nulltype>)
>                                                jBuiltInTypeSpec(null,null);
>                                                ^
> JmlParser.java:14279: jBuiltInTypeSpec(org.multijava.mjc.CUniverse) in
> org.jmlspecs.checker.JmlParser cannot be applied to
> (org.multijava.mjc.CUniverse,org.multijava.mjc.CUniverse)
>                                        dest=jBuiltInTypeSpec(elem_univ,
> array_univ);
>                                             ^
> JmlParser.java:17212: cannot resolve symbol
> symbol  : constructor JArrayDimsAndInits
> (org.multijava.util.compiler.TokenReference,org.multijava.mjc.CUniverse,org.multijava.mjc.CUniverse,org.multijava.mjc.JExpression[],org.multijava.mjc.JArrayInitializer)
> location: class org.multijava.mjc.JArrayDimsAndInits
>                                new   JArrayDimsAndInits(
> utility.buildTokenReference(), array_univ, elem_univ, args, init) :
>                                ^
> 47 errors
>
>
>
> -------------------------------------------------------------------------
> Check out the new SourceForge.net Marketplace.
> It's the best place to buy or sell services for
> just about anything Open Source.
> http://sourceforge.net/services/buy/index.php
> _______________________________________________
> Jmlspecs-developers mailing list
> Jmlspecs-developers@...
> https://lists.sourceforge.net/lists/listinfo/jmlspecs-developers
>

         Gary T. Leavens
         210 Harris Center (Bldg. 116)
         School of EECS, University of Central Florida
         4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
         http://www.eecs.ucf.edu/~leavens  phone: [phone]
         leavens@...

-------------------------------------------------------------------------
Check out the new SourceForge.net Marketplace.
It's the best place to buy or sell services for
just about anything Open Source.
http://sourceforge.net/services/buy/index.php
_______________________________________________
Jmlspecs-developers mailing list
Jmlspecs-developers@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-developers