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

Parameter access issue in ltl violation #242

Open TaylorHarvin opened 8 years ago

TaylorHarvin commented 8 years ago

Given code such as the example on the Javamop site below, I am not able to access Object o in the @violation section as shown below. The JavaMOP compiler generates the aspectJ code without any errors, but the aspectJ compiler flags it as unrecognized (apparently scoping issues). Is this a known issue in JavaMOP? It is accessible in the event advice when passed as a target, but not in @violation.

SafeHashSet(HashSet t, Object o) { int hashcode;

... ... ... ltl : add => (not bad_use U remove)

@violation{ System.err.println("HashCode changed for Object " + o + " while being in a Hashtable!"); System.exit(1); } }