runtimeverification / javamop

Runtime verification system for Java, using AspectJ for instrumentation.
http://fsl.cs.illinois.edu/javamop
MIT License
45 stars 37 forks source link

Random_OverrideNext property is broken #228

Closed emopers closed 8 years ago

emopers commented 8 years ago

The Random_OverrideNext property should only be violated if a subclass of java.util.Random does not override the next(int bits) method. Howerver, I have seen it violated in two perfectly legal scenarios, including PassphraseBasedPRNG.java which is a subclass of java.util.Random and clearly overrides next(int bits). Can someone please explain this?

xiaohe27 commented 8 years ago

The Random_OverrideNext property has a typo! It used a wrong data type: it used Integer instead of int, for the data type of the parameter of the method next(int bits).

A quick fix is modifying the only statement in the try block.

Method nextmethod = klass.getDeclaredMethod("next", int.class);

xiaohe27 commented 8 years ago

@emopers what do you think?

emopers commented 8 years ago

@xiaohe27 Thanks for the feedback! That fix looks good for us