Cofoja not working in intellij

Answered

Coming from here

And tried this 

I am trying to run Cofoja contracts on Intellij. I would like to know how can I do it. Thanks

32 comments
Comment actions Permalink

I've reported a bug, see https://youtrack.jetbrains.com/v2/issue/IDEA-186050 for details.

If you replace io.konverge:cofoja:jar property with the full local path to the cofoja jar file and reimport the project, it should help.

0
Comment actions Permalink

Hi, thanks for the reply. Where do you exactly want me to change that? thanks.

0
Comment actions Permalink

Thanks for the reply.

This are my settings now: 

And the error I get

0
Comment actions Permalink

Please use the full fixed path without any properties ($MAVEN_REPOSITORY$), I tested on Windows with the following and it worked ( https://i.imgur.com/MjemFFU.png ):

c:\Users\serge\.m2\repository\io\konverge\cofoja\2.0.0\cofoja-2.0.0.jar
0
Comment actions Permalink

(in depth value of com.google.java.contract.classpath)=> $MAVEN_REPOSITORY$/io/konverge/cofoja/2.0.0/cofoja-2.0.0.jar

0
Comment actions Permalink

By the way, do you know how could I add Cofoja without Maven? 

For example, having this simple project

https://www.mediafire.com/file/ml3slbbjlk2bgjm/account+(1).zip

Is the setup going to be similar or different?

Thanks again for your help

0
Comment actions Permalink

Should be the same, you will have to add the options to the annotation processor manually.

0
Comment actions Permalink

Error:

Configuration:

Using ubuntu, as you could already realise

0
Comment actions Permalink

May I see yours? Maybe I am doing it in a wrong way

0
Comment actions Permalink

Tried this: 

And gives the same error 

0
Comment actions Permalink

I am trying to get it work in the file I attached to you:

Settings:

Error:

Error:java: java.lang.RuntimeException: java.io.FileNotFoundException: /home/ismael/Desktop/Account/account/Account/target/classes: does not exist
0
Comment actions Permalink

You need to use IntelliJ IDEA module output directory, not the target directory. target is specific to Maven.

0
Comment actions Permalink

You mean like this? : 

I wonder if you could give me an example for the "Account" project, so I can realise what do you mean

0
Comment actions Permalink

src is not the output directory, check where classes are compiled.

0
Comment actions Permalink

where or how can i check that?

0
Comment actions Permalink

Changed it

But contracts still not working

0
Comment actions Permalink

Your tests output path is different. Also not sure if cofoja.asm.jar is the same as cofoja-2.0.0.jar.

0
Comment actions Permalink

I am using the Account example I attached you before (this). 

Tests are inside src as well.

0
Comment actions Permalink

It does not work, at least properly. Let me explain myself: 

Left is eclipse, right intellij. When I use @Require and use a wrong name, notice "initialBalanceWrongVariable" Eclipse warns me that there is an error in contract while Intellij tells me nothing.

No error in contract for intellij when it actually works in eclipse

0
Comment actions Permalink

Works for me in the project I've shared above:

0
Comment actions Permalink

Hmm, you're right, it is actually working when it is run. Do you know how can I get the errors on the same line (like the ones in eclipse)? Thanks for the support. 

0
Comment actions Permalink

It works not when you run it, but when the project is compiled.

You can enable automatic compilation to get such errors on the fly: https://stackoverflow.com/questions/12744303/intellij-idea-java-classes-not-auto-compiling-on-save/.

Unlike Eclipse, IntelliJ IDEA doesn't compile the project automatically by default.

0
Comment actions Permalink

Hi. 

I have this project.

There is 4 classes, Natural, NaturalTest, NaturalList and NaturalListTest.

I wrote just a simple contract for the class Natural

@Requires("d > 0")

and a test for it inside NaturalTest.

@Test(expected = PreconditionError.class)
public void testConstructorWrong() {
Natural n = new Natural(-5);
}

In that test I am expecting for a PreconditionError, which does not throw. I wonder if you could tell me why? It works on eclipse. Thanks

0
Comment actions Permalink

What is the result in Eclipse? Do you get a error when compiling or when running? What exactly is reported?

0
Comment actions Permalink

Natural class has this precondition before the constructor method.

@Requires("d >= 0")
public Natural(int d) {
data = d;
}

However, if I create a main class and create a Natural object with value -1 it should throw a PreconditionError but it does not.

public static void main(String[] args) {
Natural n = new Natural(-1);
System.out.println(n.toString());
}

It  prints -1 in the terminal.

0

Please sign in to leave a comment.