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

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

Revision: 1663
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1663&view=rev
Author:   frankrimlinger
Date:     2009-06-19 01:04:19 +0000 (Fri, 19 Jun 2009)

Log Message:
-----------
Quickly realized that the formal requirement of Mango and the operational requirements of JPF just will not blend, so abandoning attempts to create a hybrid environment.  The new plan is to introduce

ClassInfo ClassUtil.getFormalPeer(ClassInfo clazz)
MethodInfo MethodUtil. getFormalPeer(MethodInfo method)

These routines prepend "MangoFormal." to the name of the class of the passed object if not already present.  So, for example, java.lang.Boolean.toString becomes java.lang.MangoFormalBoolean.toString.  If the Class or Method with the revised name is found, then the corresponding ClassInfo or MethodInfo is returned.  Otherwise the input value is returned.  This allows classes designed to support formal analysis to mask previously existing classes.  

The point is that mango knows when it wants the formal version and can ask for it, just like jpf "knows" when it wants MethodInfo instead of Method. The new strategy is completely transparent to jpf, unlike the misguided attempt to blend.  However, in the MangoJPF code base, except for some code which actually controls the jpf operation, all access to MethodInfo and ClassInfo objects must be routed through the above methods. ?\194?\160?\194?\160This is going to be a fair amount of work to get right, but the payoff will be complete flexibility to mask or not mask the jpf environment without ever interfering with jpf internals.

Deleted existing mangoUserHome/system code to get a fresh start for conversion to MangoFormal names.

Modified Paths:
--------------
    branches/mango/MangoJPF/mangoUserHome/system/.classpath

Added Paths:
-----------
    branches/mango/Mango/mangoUserHome/frank/sessions/system.zip

Removed Paths:
-------------
    branches/mango/Mango/mangoUserHome/frank/sessions/a.zip
    branches/mango/Mango/mangoUserHome/frank/sessions/lptry1.zip
    branches/mango/MangoJPF/mangoUserHome/system/System/
    branches/mango/MangoJPF/mangoUserHome/system/SystemTests/src/


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