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

Four properties do not report correct violation locations #225

Open emopers opened 8 years ago

emopers commented 8 years ago

For the following 4 properties: File_DeleteTempFile, ObjectInput_Close, StringBuffer_SingleThreadUsage, ObjectOutput_Close, violation locations would be shown as "Unknown." instead of the FQN of the Java file with line number. Though we understand due to the formation of such properties it is hard to point out the exact place where the violation happens immediately, but at least it would be good if it could capture the location of TempFile creation or ObjectOutput opening and report it later. For example, we conceive is there any way to improve File_DeleteTempFile like:

File_DeleteTempFile(File f) {
         Location l;
         event create after returning(File f) :
                 call(File+ File.createTempFile(..)) { l = MOPLogging.getLocation(); }
         ...
         @violation {
                 MOPLogging.out.println(Level.CRITICAL, __DEFAULT_MESSAGE);
                 MOPLogging.out.println(Level.CRITICAL, "A temporary file created at " + l + " has not been deleted.");
         }
}

Is this feasible in JavaMOP? Thanks!