[Javapathfinder-svn] SF.net SVN: javapathfinder:[1670] branches/mango/MangoJPF

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

Revision: 1670
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1670&view=rev
Author:   frankrimlinger
Date:     2009-06-20 16:44:51 +0000 (Sat, 20 Jun 2009)

Log Message:
-----------

Port of rulebase to correspond to the mangoUserHome/system port, except for some new native model rules required to support the  Object versus Object_MangoFormal issue. These must be modelled "by hand".

Ported the mango native interface rules.  Mostly just had to change signatures, but mango.lang.Mango_Class.forName actually puts an "java.lang.Class_MangoFormal" on the heap, and this literal is burned into the rule.  Also, many instances of the "java.lang.String" changed to "java.lang.String_MangoFormal"

Deleted all the java package rules.  These can be rebuilt using MangoJPF and should be anyway to get good sessions for replay.

Rulebase searches turned up numerous instances of "java.lang.Class" and "java.lang.String", for example, in the rulebase theory rules.  These were all converted.  Most of this stuff has to do with formal garbage collection.

Seach rulebase for references to all the other names requiring the _MangoFormal suffix.  This turned up lots of support for the io package that I had forgotten about.  This stuff probably still works.

The "specialHeapAddress" is still "Boolean", not "Boolean_MangoFormal".  This device is only used to distinguish the static Boolean_MangoFormal objects representing true and false, and is not logically a class name.

So, with all this in place, can finally start MangoJPF code modifications to call ClassUtil.getFormalPeer and MangoUtil.getFormalPeer as appropriate.

Modified Paths:
--------------
    branches/mango/MangoJPF/Mango/src/mango/worker/workFlow/coreTechniques/model/HeapPointer.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ClassUtil.java
    branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
    branches/mango/MangoJPF/mangoUserHome/frank/rules/rulebase.zip


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