Am new to the JBMC(Bounded Model Checker). We have a requirement to find out the possibilities of RunTime Exception which may occur in java program without running it. We searched some abstract interpretation framework and found JBMC would help in this case.
for Example :
public class SampleClass {
public static void main(String[] args)
{
int ar[] = {1, 2, 3, 4, 5};
for (int i=0; i<=ar.length; i++)
System.out.println(ar[i]);
}
}
In the above program, we will get the ArrayIndexOutOfBoundException when the loop runs during the 6th iteration. But how to predict this using JBMC? We have found the command sheet which provides the details of Command line options in JBMC, but we were not able to find the combinations of commands and how to use it as well. Is there any Java API or Docs available for JBMC?
Kindly suggest!!.
Differently from CBMC, JBMC does not support all the options listed here. You can notice that by running
jbmc --help
. If you run something likejbmc <class> --bounds-check
you will obtain an "usage error".About your java class: jbmc works on .jar or .class. Try generate a .class first as follows:
javac SampleClass.java
then run jbmc on
SampleClass.class
as follows:jbmc SampleClass.class --unwind N
(try with different value of N to become more confident)Below the result for N=6:
I hope this helps. I am also new to jbmc. I have used cbmc in the past, and further documentation can be found here and here, but very few documentation is available for jbmc.