JPF seems unable to handle local variable annotations

[y553546436]

I added the logic to print local variable annotation information in the JPF listener and tried to run something like this in JPF:

public static void main(String[] args) {
  @BitFlip int a;
  int a=0;
}

The result shows that there is no AnnotationInfo for this local variable a. Therefore, our @bitflip annotation cannot work with local variables now.

[y553546436]

The problem is not with JPF, but it is because that "Local variable annotations are not retained in class files (or at runtime) regardless of the retention policy set on the annotation type." (from eclipse doc), which means any bytecode analyzer cannot process the local variable annotations. The local variable annotations are designed mainly for checking at compilation time.
A workaround could be to annotate the local variables with type annotations, which is retained in the bytecode.