Menu
▾
▴
[Javapathfinder-svn] SF.net SVN: javapathfinder:[1847] branches/mango/Mango
|
From: <fra...@us...> - 2009-08-21 19:36:06
|
Revision: 1847
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1847&view=rev
Author: frankrimlinger
Date: 2009-08-21 19:35:54 +0000 (Fri, 21 Aug 2009)
Log Message:
-----------
Changes to checkcast and instanceof broke equals() and compareTo() specs in String_MangoFormal.
Rebuilt the broken specs, which revealed a lot of interesting issues.
Discovered fun fact about interface templates. Suppose you have the following class
public class I implements Comparable<I>{
@Override
public int compareTo(I o) {
// TODO Auto-generated method stub
return 0;
}
}
Then the compiler generates the following, as expected:
Method: MethodInfo[I.compareTo(LI;)I]
instructions:
iconst_0
ireturn I.compareTo(LI;)I
BUT, you also get the following, FREE OF CHARGE
Method: MethodInfo[I.compareTo(Ljava/lang/Object;)I]
instructions:
aload_0
aload_1
checkcast
invokevirtual I.compareTo(LI;)I
ireturn I.compareTo(Ljava/lang/Object;)I
Similar code kept appearing during clean up of specification of String_MangoFormal class. This was really really puzzling, as the code just seemed to appear out of nowhere by magic. This is in fact the case, but not to worry. Its just compiler glue to help templates ease their way into the java world. Here is the specification generated by Mango for this glue:
Hypothesis: compareTo_LocalVar_at_offset_1_lineNumber_1 is undefined
Close Case: Returns int: 0.
Hypothesis: compareTo_LocalVar_at_offset_1_lineNumber_1 is defined
Hypothesis: Class name of compareTo_LocalVar_at_offset_1_lineNumber_1 may be cast to I
Close Case: Returns int: 0.
Hypothesis: compareTo_LocalVar_at_offset_1_lineNumber_1 is defined
Hypothesis: Class name of compareTo_LocalVar_at_offset_1_lineNumber_1 may not be cast to I
Close Case: Throws: java.lang.ClassCastException.
The spec is not pretty because there is no source code for this method. I bring this up because you can ask following question, is this spec "wrong"? A wrong answer is, "yes, because the second case is brain-dead." And the correct answer is, "the question is meaningless since it depends on the incorrect method I.compareTo(LI;)I." The point is that specification errors propagate upwards until at last somebody spots an inconsistency. This is one of the great strengths of the mango method.
Actually, case 1 is also brain-dead. For what its worth, executing "this".compareTo(null); throws NullPointerException, but you would never know it from reading the java doc for the Comparable interface. Mango is also very good at exposing all the boring cases.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/worker/Mango.java
branches/mango/Mango/Mango/src/mango/worker/Worker.java
branches/mango/Mango/Mango/src/mango/worker/utilities/MutableHitem.java
branches/mango/Mango/Mango/src/mango/worker/utilities/MutableSet.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/HeapItemModel.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/HeapObjectModel.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWCREATOR.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINIT.java
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/Mango/mangoUserHome/system/System/java/lang/String_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/SystemTests/src/I.java
Added Paths:
-----------
branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(LI;)I/
branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(LI;)I/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(Ljava.lang.Object_MangoFormal;)I/
branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(Ljava.lang.Object_MangoFormal;)I/Class name of compareTo_LocalVar_at_offset_1_lineNumber_1 may be cast to I.zip
branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(Ljava.lang.Object_MangoFormal;)I/Class name of compareTo_LocalVar_at_offset_1_lineNumber_1 may not be cast to I.zip
branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(Ljava.lang.Object_MangoFormal;)I/compareTo_LocalVar_at_offset_1_lineNumber_1 is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/compareTo(Ljava.lang.Object_MangoFormal;)I/Class name of compareTo_LocalVar_at_offset_1_lineNumber_1 may be cast to java.lang.String_MangoFormal.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/compareTo(Ljava.lang.Object_MangoFormal;)I/Class name of compareTo_LocalVar_at_offset_1_lineNumber_1 may not be cast to java.lang.String_MangoFormal.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/compareTo(Ljava.lang.Object_MangoFormal;)I/compareTo_LocalVar_at_offset_1_lineNumber_1 is undefined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/Class name of anObject may not be cast to java.lang.String_MangoFormal.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/String objects _this.value_ and _anObject.value_ are lexicographically equivalent.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/String objects _this.value_ and _anObject.value_ are lexicographically inequivalent.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/anObject is undefined.zip
Removed Paths:
-------------
branches/mango/Mango/mangoUserHome/frank/sessions/a.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/compareTo(Ljava.lang.Object_MangoFormal;)I/'x' is an instance of Class java.lang.String_MangoFormal.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/compareTo(Ljava.lang.Object_MangoFormal;)I/'x' is not an instance of Class java.lang.String_MangoFormal.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/'anObject' equals null reference.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/'anObject' is not an instance of Class java.lang.String_MangoFormal.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/String objects _'this'.value_ and _'anObject'.value_ are lexicographically equivalent.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/String objects _'this'.value_ and _'anObject'.value_ are lexicographically inequivalent.zip
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
