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 try
and catch
blocks 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 catch
block 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