How to generate unit test?

[Moondee]

Running DART successfully!
running ./filter-jpf-tests.sh returns:
Usage: ./filter-jpf-tests.sh JPF_OUTPUT_FILE
JPF_OUTPUT_FILE should be of form 'FooTest.java.log'.
The script will derive the class name from the file name'

Where should I find dart.java.log
any comment? Thanks

[pdinges]

Hi,

I am sorry for the very late reply.

The JPF_OUTPUT_FILE argument simply refers to a file that contains the text output generated by JPF, piped into a file. You would do something like this:

$ jpf DART.jpf > DART.java.log

Then you call filter-jpf-tests.sh on the DART.java.log file. Please note that the script is very hacky and fragile. It works by transforming (the Method Summaries section of) JPF's output text into Java code. However, because JPF's output is not always correct, the code may not compile without you editing it a little bit. Two common errors are:

• JPF sometimes claims the wrong number of parameters for methods.
• JPF does not add the required f suffix for float literals: you get 0.0 instead of 0.0f. In some cases, javac complains about this. If you have float arguments, just add the f suffix to the number literals.

As a word of warning: if JPF crashed for some reason or does not generate a Method Summaries section, the script may produce nonsensical output.

Hope that helps,
-Peter

[mousavian]

Hi Peter (@pdinges) ,
I've build and run all the tests successfully based on the README of this repo.
And also I followed the procedure you've explained here to generate tests.
But with neither DART nor any other example file (existing in test or experiments directory), I am not able to get Method Summaries section in the output.
Do you have any Idea why?

Thanks