dimanche 26 février 2017

Is there a way to stop JML runtime from catching its own Errors and Exceptions?

I'm trying to use JML and even though it seems somewhat obsolete (am I wrong?) it works decently. However, I want to run a series of tests from within a program of my own and to analyze the result, I want to catch the Errors and Exceptions sent by the JML Runtime Checker myself. It seems the JML Runtime catches the errors itself and prints information to the screen and then allows execution to go on. For example:

>java -cp .;openjml.jar L2
[1, 2, 5, 8, 10, 13, 15, 18, 21, 22, 28, 30]
1
[1, 3, 4, 6, 3, 2, 4, 5, 6, 9, 787, 6, 4, 3, 2, 3, 45, 4, 3, 2, 3, 4, 5, 54, 0]
MergeSort.java:15: JML postcondition is false
    private static void mergeSort(int[] arr, int offset, int length, int[] buf) {

... (more JML Runtime output along with actual program output)

Anyone knows how to achieve my desired behaviour? I have attempted to put tryand catchblocks outside method calls but it seems like every JML checked method is in some sort of wrapper that catches errors and exceptions before if reaches any try and catchblock in the caller.

I compile with:

java -jar opemjml.jar -rac <FILES>

And I run it with:

java -cp .;openjml.jar <FILE>

Aucun commentaire:

Enregistrer un commentaire