[Javapathfinder-svn] SF.net SVN: javapathfinder:[1867] branches/mango/Mango

[<fra...@us...>]

Revision: 1867
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1867&view=rev
Author:   frankrimlinger
Date:     2009-08-29 22:01:41 +0000 (Sat, 29 Aug 2009)

Log Message:
-----------
Added logic to use the declared type of a local variable when resolving possible methods for getVirtualRunTimeMethod.  This is just a patch, don't really intend to settle this issue in MangoBaseline.  Once jpf simulation is driving specification, it will be possible just to specify all the plausible choices without a lot of user interaction.

Rebuilt all sessions.  System methods and signatures are no longer burdened with the _MangoFormal notation, so now the system specification should grow rapidly.

Modified Paths:
--------------
    branches/mango/Mango/Mango/src/mango/worker/engine/rule/AssumeEquivRule.java
    branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/agent/AutoAssumeEquivalenceAgent.java
    branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/agent/TranslateModuleAgent.java
    branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip

Added Paths:
-----------
    branches/mango/Mango/mangoUserHome/frank/sessions/Casting/
    branches/mango/Mango/mangoUserHome/frank/sessions/Casting/<init>()V/
    branches/mango/Mango/mangoUserHome/frank/sessions/Casting/<init>()V/Final case.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/
    branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/Final case. objI may be cast to I.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/objI is undefined.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/Casting/cast(DFILI;)LI;/objI may not be cast to I.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/I/
    branches/mango/Mango/mangoUserHome/frank/sessions/I/<init>()V/
    branches/mango/Mango/mangoUserHome/frank/sessions/I/<init>()V/Final case.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(LI;)I/
    branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(LI;)I/Final case.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(Ljava.lang.Object;)I/
    branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(Ljava.lang.Object;)I/Final case. 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;)I/compareTo_LocalVar_at_offset_1_lineNumber_1 is undefined.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/I/compareTo(Ljava.lang.Object;)I/compareTo_LocalVar_at_offset_1_lineNumber_1 may be cast to I.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens()Ljava.lang.Class;/
    branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens()Ljava.lang.Class;/Final case.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens1()Ljava.lang.Class;/
    branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens1()Ljava.lang.Class;/Final case.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens2()Ljava.lang.Class;/
    branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens2()Ljava.lang.Class;/Final case.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens3()Ljava.lang.Class;/
    branches/mango/Mango/mangoUserHome/frank/sessions/I/whatHappens3()Ljava.lang.Class;/Final case.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/getComponentType()Ljava.lang.Class;/
    branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/getComponentType()Ljava.lang.Class;/Final case. this is not an array.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/getComponentType()Ljava.lang.Class;/this is an array.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/isAssignableFrom(Ljava.lang.Class;)Z/
    branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/isAssignableFrom(Ljava.lang.Class;)Z/Final case. cls is defined.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/isAssignableFrom(Ljava.lang.Class;)Z/cls is undefined.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/equals(Ljava.lang.Object;)Z/
    branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/equals(Ljava.lang.Object;)Z/Final case. this does not equal obj.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/equals(Ljava.lang.Object;)Z/this equals obj.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/<init>()V/
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/<init>()V/Final case.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleFalse()Z/
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleFalse()Z/Final case.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleFalse(Ljava.lang.Class;Ljava.lang.Class;)Z/
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleFalse(Ljava.lang.Class;Ljava.lang.Class;)Z/Final case. x is defined, y is defined.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleTrue()Z/
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/compatibleTrue()Z/Final case.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType()Ljava.lang.Class;/
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType()Ljava.lang.Class;/Final case.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType(Ljava.lang.Class;)Ljava.lang.Class;/
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType(Ljava.lang.Class;)Ljava.lang.Class;/Final case. clazz is not an array.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType(Ljava.lang.Class;)Ljava.lang.Class;/clazz is an array.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType(Ljava.lang.Class;)Ljava.lang.Class;/clazz is undefined.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType2()Ljava.lang.Class;/
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getComponentType2()Ljava.lang.Class;/Final case.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getName()Ljava.lang.String;/
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/getName()Ljava.lang.String;/Final case.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/intComponentTest()Ljava.lang.String;/
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/intComponentTest()Ljava.lang.String;/Final case.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/intComponentTest2()Ljava.lang.String;/
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/intComponentTest2()Ljava.lang.String;/Final case.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterface(Ljava.lang.Class;)Z/
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterface(Ljava.lang.Class;)Z/Final case. clazz is defined.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterface(Ljava.lang.Class;)Z/clazz is undefined.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterfaceIsFalse()Z/
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterfaceIsFalse()Z/Final case.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterfaceIsTrue()Z/
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isInterfaceIsTrue()Z/Final case.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitive(Ljava.lang.Class;)Z/
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitive(Ljava.lang.Class;)Z/Final case. clazz is defined.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitive(Ljava.lang.Class;)Z/clazz is undefined.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitiveFalse()Z/
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitiveFalse()Z/Final case.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitiveTrue()Z/
    branches/mango/Mango/mangoUserHome/frank/sessions/systemTests/ClassTests/isPrimitiveTrue()Z/Final case.zip


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.