Menu
▾
▴
javapathfinder-svn — source repository related messages (SVN)
You can subscribe to this list here.
| 2008 |
Jan
|
Feb
|
Mar
|
Apr
|
May
(16) |
Jun
(42) |
Jul
(46) |
Aug
(48) |
Sep
(33) |
Oct
(26) |
Nov
(28) |
Dec
(38) |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 2009 |
Jan
(35) |
Feb
(80) |
Mar
(112) |
Apr
(108) |
May
(102) |
Jun
(126) |
Jul
(89) |
Aug
(82) |
Sep
(36) |
Oct
(7) |
Nov
(1) |
Dec
(4) |
| 2010 |
Jan
(87) |
Feb
|
Mar
(2) |
Apr
(1) |
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
|
From: <fra...@us...> - 2009-07-16 17:37:36
|
Revision: 1764
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1764&view=rev
Author: frankrimlinger
Date: 2009-07-16 17:37:29 +0000 (Thu, 16 Jul 2009)
Log Message:
-----------
More array rehab. It is not necessary to create intermediate subarray objects just so they can be retrieved. The retrieval mechanism has all the information necessary to manufacture such objects as required. So "pushRefH" has been retired. This impacts
AALOAD
AASTORE
ARRAYLENGTH
The new scheme also impacts valueH semantics, and works like so. Suppose X is a class and we create x=new X[][][] and then access x[1][2][3]. This should be the default value null. First, multinewarray updates the heap:
H1 = (pusH (refH 'nH ^className ) "X[][][]" 'H)
There is also info about sublengths which we suppress. Now we have aaload 1, which updates the opstack like so
(push (valueH (refH 'nH 1) H1) opStack )
The point is that valueH can inspect H1, discover that 'nH is a multiarray and that x[1] is not initialized, so it can just manufacture the object (array 'nH 1), so the opstack rewrites to
(push (array 'nH 1) opStack)
Now we have aaload 2, so
(push (valueH (refH (array 'nH 1) 2) H1) opStack)
Once again, valueH can dig down to 'nH, inspect H1, so we get
(push (array 'nH 1 2) opStack)
because we have the normalization (array (array obj i_1 ... i_n) i_n+1) = (array obj i_1 ... i_n+1)
Finally aaload 3 gives
(push (valueH (refH (array 'nH 1 2) 3) H1) opStack)
but this time, valueH realizes that H1 is three dimensional, and so (array 'nH 1 2 3) is uninitialized, hence we punch in the default to get
(push ^null opStack) as desired.
Observe that by putting more smarts in valueH, we make the formal semantics much more uniform, which helps out both the rewriter and ACL2 theorem prover. Any entry in a multi-array gets a canonical home if it wants it.
NB: the old "ptr" rulekey is now the more descriptive "array". The old usage for "array" is obsolete and has already been retired. valueH will get its smarts when we hit the multiarray class in mangoModelTest. For now, we just rehab the formal semantics of the affected instructions.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/Checkcast.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/Instanceof.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/comparison/InequivalentPtr.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashEngine.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashMangoModel.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashOpcodeSyms.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashRewriter.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/agent/CheckCast_getValueAgent.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/agent/InstanceOfAgent.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/HeapModel.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/HeapObjectModel.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/form/sym/binder/executable/HeapSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/model/TranslationManager.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/sym/TranslationSym.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/Invocation.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/AALOAD.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/AASTORE.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ANEWARRAY.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ARRAYLENGTH.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWCREATOR.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/BALOAD.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/BASTORE.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/CALOAD.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/CASTORE.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/DALOAD.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/DASTORE.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/FALOAD.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/FASTORE.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IALOAD.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/IASTORE.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/LALOAD.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/LASTORE.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/LDC_W.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/MULTIANEWARRAY.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/NEW.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/NEWARRAY.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/SALOAD.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/SASTORE.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/sym/JclassSym.java
Removed Paths:
-------------
branches/mango/Mango/Mango/src/mango/ruleAction/form/binder/PushRefH.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-16 13:17:11
|
Revision: 1763
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1763&view=rev
Author: frankrimlinger
Date: 2009-07-16 13:17:06 +0000 (Thu, 16 Jul 2009)
Log Message:
-----------
Rehab of the rulebase for the new typing system underway. All ports of entry for class names within the SCANNER bytecode classes are being tested, and these names are now all to be resolved at the java source code level. Examples:
NEW: mangoModelTest.multiarray
NEWARRAY: int
ANEWARRAY: mangoModelTest.RefBuster
MULTIANEWARRAY: mangoModelTest.multiarray[][][][]
The issue then becomes, how to unresolve a resolved name, so it becomes suitable input for ClassInfo.getClassInfo()? One might hope that Types.getTypeCode(className, true) would do the trick, but this [[[[null for className= mangoModelTest.multiarray[][][][]. Sadly, getTypeCode expects the input LmangoModelTest.multiarray;[][][][] in order to produce [[[[LmangoModelTest.multiarray; Instead, use FormalTypes.getTypeCode, which inserts the L and ; in the array case before calling super.getTypeCode, (but only if !isBasicType)
All the class name conversion code and code to syntactically detect arrays from array names must be rehabilitated to conform to the new standard. Also, all class names are formally introduced as ClassNameSym objects, which have formal type className. Maintaining discipline with the typing of class names will really help out down the road.
With the rationalization of class names, there is no longer any need for the formal ^Array_Type_Marker subaddress. Instead, the ^className subaddress (changed from ^Type), will just be set up correctly in the first place. Also, the following subaddresses containing information about arrays are renamed as follows:
h.ALength ^Array_Length_Marker -->h.arrayLength ^arrayLength
h.ADimension ^Array_Dimension_Marker --> h.arrayDimension ^arrayDimension
h.ASubLengths ^SubArray_Length_List_Marker --> h.arraySubLengths ^arraySubLengths
The JVM and Module function spaces have been thinned out. Removed functions mostly dealt with cleaning up all the problems with arrays that never will happen now. A rational set of functions can be developed as the system is rebuilt.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/core/CoreSym.java
branches/mango/Mango/Mango/src/mango/core/RuleResourceManager.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/ClassPtrAsString.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/GetComponentType.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/IsArrayClassPtr.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/MakeClassPtr.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/RemoveBracket.java
branches/mango/Mango/Mango/src/mango/ruleAction/form/binder/PushRefH.java
branches/mango/Mango/Mango/src/mango/ruleAction/translate/engine/TranslateValueH.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/IntegralArrayFieldType.java
branches/mango/Mango/Mango/src/mango/worker/Worker.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashCoreParser.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashEnterpriseAndTranslation.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashLogicAndArithmetic.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashOpcodeSyms.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/model/HeapPointer.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/model/HeapTracer.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/HeapObjectModel.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/FormalTypes.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoMethodPeer.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/ANEWARRAY.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/MULTIANEWARRAY.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/NEW.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/NEWARRAY.java
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/Mango/mangoUserHome/system/System/java/lang/Object_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_Object.java
Added Paths:
-----------
branches/mango/Mango/Mango/src/mango/ruleRequirement/symbols/ClassNameType.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashTyping.java
branches/mango/Mango/Mango/src/mango/worker/engine/sym/ClassNameSym.java
branches/mango/Mango/javapathfinder-mango-bridge/mangoModelTest/
branches/mango/Mango/javapathfinder-mango-bridge/mangoModelTest/multiarray.java
branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_String.arraySyntax worksheet.txt
Removed Paths:
-------------
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/string/StripObjectSyntax.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/symbols/ClassPtrType.java
branches/mango/Mango/Mango/src/mango/worker/engine/sym/ClassPtrSym.java
branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_String.leftBracket worksheet.txt
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-07-15 05:27:21
|
Revision: 1762
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1762&view=rev
Author: staats
Date: 2009-07-15 05:27:16 +0000 (Wed, 15 Jul 2009)
Log Message:
-----------
whoops, fixed experiments
Modified Paths:
--------------
trunk/extensions/complexcoverage/bin/asw-concretize-config.txt
trunk/extensions/complexcoverage/bin/asw-random-config.txt
trunk/extensions/complexcoverage/bin/asw-reorder-config.txt
trunk/extensions/complexcoverage/bin/asw-trim-config.txt
trunk/extensions/complexcoverage/bin/binheap-concretize-config.txt
trunk/extensions/complexcoverage/bin/binheap-random-config.txt
trunk/extensions/complexcoverage/bin/binheap-reorder-config.txt
trunk/extensions/complexcoverage/bin/binheap-trim-config.txt
trunk/extensions/complexcoverage/bin/bintree-concretize-config.txt
trunk/extensions/complexcoverage/bin/bintree-random-config.txt
trunk/extensions/complexcoverage/bin/bintree-reorder-config.txt
trunk/extensions/complexcoverage/bin/bintree-trim-config.txt
trunk/extensions/complexcoverage/bin/fibheap-concretize-config.txt
trunk/extensions/complexcoverage/bin/fibheap-random-config.txt
trunk/extensions/complexcoverage/bin/fibheap-reorder-config.txt
trunk/extensions/complexcoverage/bin/fibheap-trim-config.txt
trunk/extensions/complexcoverage/bin/treemap-concretize-config.txt
trunk/extensions/complexcoverage/bin/treemap-random-config.txt
trunk/extensions/complexcoverage/bin/treemap-reorder-config.txt
trunk/extensions/complexcoverage/bin/treemap-trim-config.txt
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-15 03:39:52
|
Revision: 1761
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1761&view=rev
Author: frankrimlinger
Date: 2009-07-15 03:39:50 +0000 (Wed, 15 Jul 2009)
Log Message:
-----------
Migration of code base to new typing system complete. Now for the rulebase. This will require hacking into the core factories and punching in the new type names. Also AbstractSym needs to be changed to InvocationNameSym. Also map the following requirements:
InstantiatedHeap --> Instantiated
InstantiatedStack --> Instantiated
InstantiatedStat --> Instantiated
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/ruleAction/translate/engine/TranslateHeapObject1.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/linearArithmetic/InequationValue.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/linearArithmetic/LinearVariable.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/linearArithmetic/NotEquationValue.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/naturalLanguage/Instantiated.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/ArithmeticFieldType.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/DoubleReq.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/FloatReq.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/GstackReq.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/HeapPointerReq.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/IntReq.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/IntegralArrayFieldType.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/IntegralFieldType.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/IntegralValue.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/InvocationNameReq.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/JavaButNotJVMtype.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/LongReq.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/PredTransformerReq.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/PredicateReq.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/StateReq.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/StringValue.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/UconReq.java
branches/mango/Mango/Mango/src/mango/worker/Worker.java
branches/mango/Mango/Mango/src/mango/worker/engine/sym/InvocationNameSym.java
branches/mango/Mango/Mango/src/mango/worker/utilities/Util.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/sym/EquationSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/sym/InequationSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/HeapItemModel.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/HeapModel.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/HeapObjectModel.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/LocalVarModel.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/form/sym/binder/ContextBinderSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/functionSpace/sym/ModuleHypothesisSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/functionSpace/sym/ModuleInvocationSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/model/InvariantModel.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/ShowTypeRequestMsg.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/FormalTypes.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoMethodPeer.java
Removed Paths:
-------------
branches/mango/Mango/Mango/src/mango/ruleRequirement/naturalLanguage/InstantiatedHeap.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/naturalLanguage/InstantiatedStack.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/naturalLanguage/InstantiatedStat.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/PushHvalue.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-07-15 00:03:18
|
Revision: 1760
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1760&view=rev
Author: staats
Date: 2009-07-15 00:03:09 +0000 (Wed, 15 Jul 2009)
Log Message:
-----------
added even more experiments
Modified Paths:
--------------
trunk/extensions/complexcoverage/bin/asw-concretize-config.txt
trunk/extensions/complexcoverage/bin/bintree-concretize-config.txt
trunk/extensions/complexcoverage/bin/fibheap-concretize-config.txt
trunk/extensions/complexcoverage/bin/launch-parallel-experiment.py
trunk/extensions/complexcoverage/bin/treemap-concretize-config.txt
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/heuristic/ConcretizeVariables.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/RemoteJPF.java
trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/test/BinomialHeap.java
trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/test/FibHeap.java
trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/test/TreeMap.java
Added Paths:
-----------
trunk/extensions/complexcoverage/bin/asw-constrain-config.txt
trunk/extensions/complexcoverage/bin/binheap-concretize-config.txt
trunk/extensions/complexcoverage/bin/binheap-random-config.txt
trunk/extensions/complexcoverage/bin/binheap-reorder-config.txt
trunk/extensions/complexcoverage/bin/binheap-trim-config.txt
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-14 21:20:15
|
Revision: 1759
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1759&view=rev
Author: frankrimlinger
Date: 2009-07-14 21:20:08 +0000 (Tue, 14 Jul 2009)
Log Message:
-----------
Type system rehab is now nearing completion, at least in the code base. There will also be a
lot of work in the rulebase due to rationalization of requirement names.
All type requirements now defer to FormalTypes. Also introduced getTypeDelegate() method for Hitems that want to punt. This is definitely better-faster-cheaper.
ArithmeticLocalVar --> ArithmeticValue
FoundationSym no longer has type formal_predicate.
This is a long-standing hack that needs to be addressed in a saner manner.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/core/sym/RuleKey.java
branches/mango/Mango/Mango/src/mango/enterprise/sym/ExpLevelSym.java
branches/mango/Mango/Mango/src/mango/module/definition/sym/ParamSym.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/InheritTypeFromThirdArg.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/TypeAssignmentRule.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/comparison/Equals.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/comparison/InequivalentRef.java
branches/mango/Mango/Mango/src/mango/ruleAction/form/binder/PushRefH.java
branches/mango/Mango/Mango/src/mango/ruleAction/translate/engine/BoolRecapture.java
branches/mango/Mango/Mango/src/mango/ruleAction/translate/engine/BoolRecaptureAndNegate.java
branches/mango/Mango/Mango/src/mango/ruleAction/translate/engine/CharRecapture.java
branches/mango/Mango/Mango/src/mango/ruleAction/translate/engine/CharRecaptureAndNegate.java
branches/mango/Mango/Mango/src/mango/ruleAction/translate/engine/TranslateValueH.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/linearArithmetic/CoefficientValue.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/linearArithmetic/ConjunctionValue.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/linearArithmetic/EquationValue.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/ArithmeticValue.java
branches/mango/Mango/Mango/src/mango/worker/Worker.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/DoubleH.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/FloatH.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/Hitem.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/IntegerH.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/Kons.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/LongH.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/Number.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/csym/Csym.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHash.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashInitialize.java
branches/mango/Mango/Mango/src/mango/worker/engine/rule/Rule.java
branches/mango/Mango/Mango/src/mango/worker/engine/sym/InterpretableSym.java
branches/mango/Mango/Mango/src/mango/worker/engine/sym/Sym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/GateSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/CodeSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/EdgeSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/LoopSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/PathSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/ucon/MethodEntrySym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/ucon/UconSym.java
branches/mango/Mango/Mango/src/mango/worker/utilities/Util.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/agent/WithAgent.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/model/HeapTracer.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/sym/ConjunctionSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/sym/EquationSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/sym/FoundationSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/sym/InequationSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/form/sym/binder/executable/LocalVarSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/functionSpace/sym/FunctionSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/functionSpace/sym/ModuleHypothesisSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/ShowTypeRequestMsg.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/FormalTypes.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoMethodPeer.java
Removed Paths:
-------------
branches/mango/Mango/Mango/src/mango/ruleRequirement/linearArithmetic/ArithmeticLocalVar.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-14 04:43:30
|
Revision: 1758
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1758&view=rev
Author: frankrimlinger
Date: 2009-07-14 04:43:27 +0000 (Tue, 14 Jul 2009)
Log Message:
-----------
Type system rehab and cleanup. In FormalTypes class, added partial orderings of types for making positive inferences about implied type. This needs to be hooked up to the typing requirements, replacing the old "satisfies" system, which is obsolete.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/core/util/CoreUtilities.java
branches/mango/Mango/Mango/src/mango/enterprise/sym/ExpLevelSym.java
branches/mango/Mango/Mango/src/mango/module/definition/msg/AddEquivalenceRequestMsg.java
branches/mango/Mango/Mango/src/mango/module/instance/model/InstanceManager.java
branches/mango/Mango/Mango/src/mango/module/instance/msg/SubmitStandingHypothesisMsg.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/BuildAbstractSym.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/BuildAbstractUcon.java
branches/mango/Mango/Mango/src/mango/ruleAction/translate/engine/TranslateType.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/backflow/BlockedUcon.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/leadingKey/NotResolvedAbstractUcon.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/linearArithmetic/CoefficientValue.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/symbols/AbstractSymbolReq.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/symbols/NotAbstractSym.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/symbols/ResolvedAbstractSym.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/ArithmeticFieldType.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/Hitem.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/Kons.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashCoreParser.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashLogicAndArithmetic.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashMangoModel.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashRewriter.java
branches/mango/Mango/Mango/src/mango/worker/engine/rule/AssumeEquivRule.java
branches/mango/Mango/Mango/src/mango/worker/engine/rule/Rule.java
branches/mango/Mango/Mango/src/mango/worker/engine/sym/Sym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/functionSpace/sym/FunctionSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/invariant/agent/InvariantHypoAgent.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/FormalTypes.java
Added Paths:
-----------
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/InvocationNameReq.java
branches/mango/Mango/Mango/src/mango/worker/engine/sym/InvocationNameSym.java
Removed Paths:
-------------
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/AbstractSymTypeReq.java
branches/mango/Mango/Mango/src/mango/worker/engine/sym/AbstractSym.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-07-13 23:39:22
|
Revision: 1757
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1757&view=rev
Author: staats
Date: 2009-07-13 23:39:19 +0000 (Mon, 13 Jul 2009)
Log Message:
-----------
More experiments to run
Modified Paths:
--------------
trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/test/FibHeap.java
trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/test/FibHeapNode.java
trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/test/TreeMap.java
Added Paths:
-----------
trunk/extensions/complexcoverage/bin/fibheap-concretize-config.txt
trunk/extensions/complexcoverage/bin/fibheap-random-config.txt
trunk/extensions/complexcoverage/bin/fibheap-reorder-config.txt
trunk/extensions/complexcoverage/bin/fibheap-trim-config.txt
trunk/extensions/complexcoverage/bin/treemap-concretize-config.txt
trunk/extensions/complexcoverage/bin/treemap-random-config.txt
trunk/extensions/complexcoverage/bin/treemap-reorder-config.txt
trunk/extensions/complexcoverage/bin/treemap-trim-config.txt
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-13 21:52:04
|
Revision: 1756
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1756&view=rev
Author: frankrimlinger
Date: 2009-07-13 21:51:58 +0000 (Mon, 13 Jul 2009)
Log Message:
-----------
Only the "valueOf" methods of String_MangoFormal still lack native abstraction. But before doing this, a much more significant issue needs attention. The overhaul of the type system, long overdue, is finally underway. Historically, several competing systems grew up, all represented in the code base in various stages of decay. The goal is a single typing system with flat primitive name space. Several comments are in order.
The type of an object was stored in the rulebase like so
(pushH (refH ref ^Type) stripped-object-syntax heap)
so that the type of a string becomes java.lang.String, as opposed to
Ljava.langString; or java/lang/String or even Ljava/lang/String;
This choice was made long ago, when the what-you-see-is-what-you-should-store idea was very much in vogue.
Give this, what is the type of an integer field x? The choice was "I", as opposed to "int". This was the wrong choice, because now there is no way to distinguish the class named "I" from an integer. So now is the time to fix this problem. For primitive types, we switch to java language level syntax: byte, short, int, etc for B,S,I etc. Fortunately, jpf FieldInfo.getType() is returning java language level anyway, so this is good.
As for the type of an array of integers, it is now
int[]
as opposed to "[I" or "L[I;" because this is what is specified at the java language level. This means that the syntactic test for array type, given a type name, is now endsWith(typeName,"]"), as opposed to startsWith(typeName,"["). This change must be propagated through the rulebase and the code base.
NB: for arrays, FieldInfo.getType() does the right thing, because this traces all the way back to gov.nasa.jpf.jvm.Types.getTypeName(String type), which contains the desired conversion.
if (c == '[') {
return getTypeName(type.substring(1)) + "[]";
}
if (type.charAt(len - 1) == ';') {
return type.substring(1, type.indexOf(';')).replace('/', '.');
}
This is clearly doing what we want. In other words, "type" and "java type" have now converged to the same thing, so the horrible JavaType class has been retired. This functionality is now in the mango.FormalTypes in the javapathfinder-mango-bridge, which extends gov.nasa.jpf.jvm.Types. The FormalTypes class completely rationalizes the computation of type inequivalence by reference to so-called "instance equivalence classes" of types.
Needless to say, the "formal types" like heap, stack, string, and so on, now have names that collide with the java class names in the brave new flattened name space. All of these have been converted to from X to <X>, which is the jvm strategy for avoiding namespace collision.
Consistent with the strategy of flattening the type space, the LogicaKey extension of RuleKey has been abandoned. A RuleKey now represents a type if and only if its typeFlag is set. All of the defX rulekeys in the rulebase have been replaced by the Y or <Y> rulekey counterpart, where the binding from X to Y was determined by the now obsolete buildLogicalKey method.
NB: This discussion only applies to the type as stored in formal heap. Method signatures are *always* stored and displayed in internal formal. A rose by any other name would small as sweet.
It will probably take some time for typing to settle down, but at least now the path is clear and the foundations are firm.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/Resources/IconIndex.java
branches/mango/Mango/Mango/src/mango/core/sym/RuleKey.java
branches/mango/Mango/Mango/src/mango/module/definition/loop/LoopDefinitionManager.java
branches/mango/Mango/Mango/src/mango/module/definition/method/MethodDefinitionManager.java
branches/mango/Mango/Mango/src/mango/module/definition/model/DefinitionManager.java
branches/mango/Mango/Mango/src/mango/module/definition/sym/ParamSym.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/conditional/Free.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefArithmeticValue.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefCoefficientValue.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefConjunctionValue.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefDouble.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefEquationValue.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefFloat.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefGstack.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefInequationValue.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefInt.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefIntegralValue.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefLong.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefStringValue.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/InheritTypeFromThirdArg.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/classModel/GetVirtualRunTimeException.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/comparison/InequivalentRef.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/function/FunctionSpaceTypeName.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/linearArithmetic/CoefficientValue.java
branches/mango/Mango/Mango/src/mango/ruleRequirement/typing/ArithmeticValue.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/DoubleH.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/FloatH.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/Hitem.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/IntegerH.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/Kons.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/LongH.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/Number.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/csym/Csym.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashInitialize.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashLogicAndArithmetic.java
branches/mango/Mango/Mango/src/mango/worker/engine/rule/Rule.java
branches/mango/Mango/Mango/src/mango/worker/engine/rule/RuleAction.java
branches/mango/Mango/Mango/src/mango/worker/engine/sym/Sym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/GateSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/CodeSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/EdgeSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/LoopSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/graphic/PathSym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/ucon/MethodEntrySym.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/sym/ucon/UconSym.java
branches/mango/Mango/Mango/src/mango/worker/utilities/Util.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/sym/ConjunctionSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/sym/EquationSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/sym/FoundationSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/sym/FreeVariableSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/coreTechniques/sym/InequationSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/HeapItemModel.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/HeapModel.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/form/model/LocalVarModel.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/form/sym/binder/executable/LocalVarSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/functionSpace/agent/StabilizeParameterAgent.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/functionSpace/sym/FunctionSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/functionSpace/sym/ModuleHypothesisSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/functionSpace/sym/ModuleInvocationSym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/model/HitemUtil.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/msg/ShowTypeRequestMsg.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/MangoMethodPeer.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/sym/JclassSym.java
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/Mango/mangoUserHome/frank/rules/substring param.zip
branches/mango/Mango/mangoUserHome/system/System/mango/cheat_sheet.txt
Added Paths:
-----------
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefObject.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefPredicate.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefPredicateTransformer.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefState.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefUcon.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/TypeAssignmentRule.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/csym/TypeAssignmentCsym.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/FormalTypes.java
branches/mango/Mango/mangoUserHome/frank/rules/hypothese for bounds.zip
branches/mango/Mango/mangoUserHome/frank/rules/substring hypo.zip
Removed Paths:
-------------
branches/mango/Mango/Mango/src/mango/core/sym/LogicalKey.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefAbstractSym.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefHP.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefP.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefPT.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefPushHvalue.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefS.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/DefU.java
branches/mango/Mango/Mango/src/mango/ruleAction/conditionalTechniques/type/LogicalKeyRule.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/csym/LogicalKeyCsym.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/model/JavaType.java
branches/mango/Mango/mangoUserHome/frank/rules/backupString.zip
branches/mango/Mango/mangoUserHome/frank/rules/concatParam.zip
branches/mango/Mango/mangoUserHome/frank/rules/parameters.zip
branches/mango/Mango/mangoUserHome/frank/rules/tier.zip
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-13 06:07:36
|
Revision: 1755
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1755&view=rev
Author: frankrimlinger
Date: 2009-07-13 06:07:35 +0000 (Mon, 13 Jul 2009)
Log Message:
-----------
Created native abstraction for String_MangoFormal.toCharArray(). This is a little tricky because it involved new semantics for the heap. First, a "smart" reference
( toArray "@#0" '@this '@inputHeap )
which bundles the newly created reference @#0 with the information required to extract its contents, in the event it ever became defined (from the past, of course) and it is ever accessed (in the future).
THe other thing is
(pushH '@genericLocation '@genericItem '@inputHeap )
These generic parameters depend on the smart reference, and represent data that is potentially on the heap that we know something about (where it came from, what its type is.). This has implications for garbage collection that will unfold as they may.
The rest of the native String methods should be EZ.
Modified Paths:
--------------
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/Mango/mangoUserHome/system/System/mango/cheat_sheet.txt
Added Paths:
-----------
branches/mango/Mango/config docs/
branches/mango/Mango/config docs/branding.tiff
branches/mango/Mango/config docs/launching page.tiff
branches/mango/Mango/config docs/splash page.tiff
branches/mango/Mango/mangoUserHome/frank/rules/backupString.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/toString_MangoFormal()Ljava.lang.String_MangoFormal;/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/toString_MangoFormal()Ljava.lang.String_MangoFormal;/case.zip
branches/mango/Mango/mangoUserHome/system/System/mango/lang/toCharArray Worksheet (Autosaved)
branches/mango/Mango/mangoUserHome/system/System/mango/lang/toCharArray Worksheet.txt
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-07-13 05:27:52
|
Revision: 1754
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1754&view=rev
Author: staats
Date: 2009-07-13 05:27:47 +0000 (Mon, 13 Jul 2009)
Log Message:
-----------
More experiments
Modified Paths:
--------------
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/RemoteJPF.java
trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/test/BinTree.java
Added Paths:
-----------
trunk/extensions/complexcoverage/bin/bintree-concretize-config.txt
trunk/extensions/complexcoverage/bin/bintree-random-config.txt
trunk/extensions/complexcoverage/bin/bintree-reorder-config.txt
trunk/extensions/complexcoverage/bin/bintree-trim-config.txt
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-07-12 06:50:28
|
Revision: 1753
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1753&view=rev
Author: staats
Date: 2009-07-12 06:50:22 +0000 (Sun, 12 Jul 2009)
Log Message:
-----------
Ready to run experiments. :)
Modified Paths:
--------------
trunk/extensions/complexcoverage/bin/launch-parallel-experiment.py
trunk/extensions/complexcoverage/launch/CompCov TestFun Symbolic Concretize.launch
trunk/extensions/complexcoverage/launch/CompCov TestFun Symbolic PathConstraint.launch
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/heuristic/ReorderingSymbolicSearch.java
trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/test/ASWMainClass.java
trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/test/asw.java
Added Paths:
-----------
trunk/extensions/complexcoverage/bin/asw-concretize-config.txt
trunk/extensions/complexcoverage/bin/asw-random-config.txt
trunk/extensions/complexcoverage/bin/asw-reorder-config.txt
trunk/extensions/complexcoverage/bin/asw-trim-config.txt
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-07-12 03:27:52
|
Revision: 1752
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1752&view=rev
Author: staats
Date: 2009-07-12 03:27:44 +0000 (Sun, 12 Jul 2009)
Log Message:
-----------
Updated experimental scripts
Modified Paths:
--------------
trunk/extensions/complexcoverage/launch/CompCov Parallel Client.launch
trunk/extensions/complexcoverage/launch/CompCov Parallel Manager ASW MCDC.launch
trunk/extensions/complexcoverage/launch/CompCov Parallel Manager Testfile.launch
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/RemoteJPF.java
trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/test/TestFile.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-11 19:32:26
|
Revision: 1751
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1751&view=rev
Author: frankrimlinger
Date: 2009-07-11 19:32:22 +0000 (Sat, 11 Jul 2009)
Log Message:
-----------
Added more String method native abstractions. This effort moving along nicely now, but don't forget to punch in arroybounds hypotheses for methods that need them.
Modified Paths:
--------------
branches/mango/Mango/META-INF/Mango.product
branches/mango/Mango/Mango/src/mango/worker/Worker.java
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/Mango/mangoUserHome/system/System/mango/cheat_sheet.txt
branches/mango/Mango/plugin.xml
Added Paths:
-----------
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/string/EndsWith.java
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/string/IndexOf.java
branches/mango/Mango/mangoUserHome/frank/rules/concatParam.zip
branches/mango/Mango/mangoUserHome/frank/rules/parameters.zip
branches/mango/Mango/mangoUserHome/frank/rules/substring param.zip
branches/mango/Mango/mangoUserHome/frank/rules/this is defined standing.zip
branches/mango/Mango/mangoUserHome/frank/rules/x is defined.zip
branches/mango/Mango/mangoUserHome/frank/rules/x parameters.zip
Removed Paths:
-------------
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/string/IndexOfChar.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-11 02:54:59
|
Revision: 1750
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1750&view=rev
Author: frankrimlinger
Date: 2009-07-11 02:54:56 +0000 (Sat, 11 Jul 2009)
Log Message:
-----------
Slash versus dot issue appears to be resolved. Wrote native abstraction for compareTo(String) and used tool to generate abstraction for compareTo(Object) and the four cases of String.equals(). No new bugs. This is very encouraging. The rest of the String class is all native, about fifteen methods to go.
Modified Paths:
--------------
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/Mango/mangoUserHome/frank/rules/tier.zip
Added Paths:
-----------
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/string/CompareToIgnoreCase.java
branches/mango/Mango/mangoUserHome/frank/sessions/java/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/compareTo(Ljava.lang.Object_MangoFormal;)I/
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/compareToIgnoreCase(Ljava.lang.String_MangoFormal;)I/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/compareToIgnoreCase(Ljava.lang.String_MangoFormal;)I/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/
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.
|
|
From: <fra...@us...> - 2009-07-11 01:29:15
|
Revision: 1749
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1749&view=rev
Author: frankrimlinger
Date: 2009-07-11 01:29:07 +0000 (Sat, 11 Jul 2009)
Log Message:
-----------
Fix for dot versus slash issue has invalidated existing sessions. No great loss. Clearing them all out.
Removed Paths:
-------------
branches/mango/Mango/mangoUserHome/frank/sessions/baseline/
branches/mango/Mango/mangoUserHome/frank/sessions/java/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-11 01:25:36
|
Revision: 1748
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1748&view=rev
Author: frankrimlinger
Date: 2009-07-11 01:25:33 +0000 (Sat, 11 Jul 2009)
Log Message:
-----------
Fix for dot versus slash issue has invalidated existing sessions. No great loss. Clearing them all out.
Modified Paths:
--------------
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
Removed Paths:
-------------
branches/mango/Mango/mangoUserHome/frank/sessions/a.zip
branches/mango/Mango/mangoUserHome/frank/sessions/extest/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-07-11 00:54:36
|
Revision: 1747
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1747&view=rev
Author: staats
Date: 2009-07-11 00:54:27 +0000 (Sat, 11 Jul 2009)
Log Message:
-----------
Add CPU usage based timeout and debug time info
Modified Paths:
--------------
trunk/extensions/complexcoverage/launch/CompCov Parallel Manager Testfile.launch
trunk/extensions/complexcoverage/launch/CompCov TestFun Measure Reduced.launch
trunk/extensions/complexcoverage/launch/CompCov TestFun SimpleCoverage.launch
trunk/extensions/complexcoverage/launch/CompCov TestFun Symbolic.launch
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/JPF_gov_nasa_jpf_complexcoverage_Debug.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/LocalJPFManager.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/RemoteJPF.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/StartJPFManager.java
trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/test/TestFile.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-10 21:21:16
|
Revision: 1746
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1746&view=rev
Author: frankrimlinger
Date: 2009-07-10 21:21:15 +0000 (Fri, 10 Jul 2009)
Log Message:
-----------
OK, the CHECKCAST instruction in jpf uses something called "canonical" type, which is like stripped regular type except it used the Lxxx; notation for arrays. Hmmm... this is probably ok, just weird. However, jpf INSTANCEOF explicitly changes "." back to "/". This feels a little buggy to me, but oh well. In my version of jpf version of INSTANCEOF, I introduce an explicit canonicalType field, which the mango version of INSTANCEOF uses in buildFormalPeer.
Hopefully this clears up my problem. SUN is no more, so can't them for internal format.
Modified Paths:
--------------
branches/mango/Mango/javapathfinder-mango-bridge/gov/nasa/jpf/jvm/bytecode_mango_formal_language/INSTANCEOF.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/INSTANCEOF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-10 20:37:48
|
Revision: 1745
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1745&view=rev
Author: frankrimlinger
Date: 2009-07-10 20:37:43 +0000 (Fri, 10 Jul 2009)
Log Message:
-----------
All targeted String constructors now have native abstractions. Unfortunately, an ancient nightmare has returned. Sometimes class names are in "stripped regular form", java.lang.String, and sometimes in "internal form", Ljava/lang/String; This is causing havoc in trying to relieve hypotheses.
So what is the ideal? Internal form is really bad because it makes a class name look like a path name. Stripped regular form is bad because you can't tell syntactically whether char is a primitive type or really Lchar;. However, you can't make the class Lchar; at the compiler level, so if you assume compiled code then stripped regular is ok.
Need to hunt down all the internal forms and change them to stripped regular.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/worker/Worker.java
branches/mango/Mango/Mango/src/mango/worker/mangoModel/agent/CheckCast_getValueAgent.java
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/Mango/mangoUserHome/frank/sessions/a.zip
branches/mango/Mango/mangoUserHome/system/System/java/lang/String_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/mango/cheat_sheet.txt
Added Paths:
-----------
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/string/ExtractStringFromCharArray.java
branches/mango/Mango/mangoUserHome/frank/rules/tier.zip
branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/clear([I)V/loops/-baseline.itsAWrap.clear([I)V#8- dload_i_Code_01/
branches/mango/Mango/mangoUserHome/frank/sessions/baseline/itsAWrap/clear([I)V/loops/-baseline.itsAWrap.clear([I)V#8- dload_i_Code_01/op0 is less than 10.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/ClassCastException_MangoFormal/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/ClassCastException_MangoFormal/<init>()V/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/ClassCastException_MangoFormal/<init>()V/case.zip
branches/mango/Mango/mangoUserHome/system/System/java/lang/ClassCastException_MangoFormal.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-07-10 16:27:28
|
Revision: 1744
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1744&view=rev
Author: staats
Date: 2009-07-10 16:27:17 +0000 (Fri, 10 Jul 2009)
Log Message:
-----------
Modified Paths:
--------------
trunk/extensions/complexcoverage/bin/launch-parallel-experiment.py
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-10 04:35:27
|
Revision: 1743
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1743&view=rev
Author: frankrimlinger
Date: 2009-07-10 04:35:17 +0000 (Fri, 10 Jul 2009)
Log Message:
-----------
Added stability and composition rules for sting utility rulekeys. Fixed another virtual invocation bug. Stubbed out most of the String_MangoFormal methods, about twenty of them require native abstraction. The new stubs just throw IllegalStateException(), so pay-as-you-go is safer now. Wrote native abstractions for <init>(C) and init([C).
Start with <init>([CII). Use utitility rulekey substring.
CAVEAT EMPTOR: Don't get lulled into thinking <init> knows the type of this. Only newly minted addresses created by the new family know the type. Formal peer builders do this, not you. You really only specify type when punching in a final object by hand, like a String literal.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/core/gui/window/CoreRuleBaseWindowFactory.java
branches/mango/Mango/Mango/src/mango/worker/WorkerControl.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/Invocation.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/Mango/mangoUserHome/system/System/java/lang/String_MangoFormal.java
Added Paths:
-----------
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Exception_MangoFormal/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Exception_MangoFormal/<init>()V/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Exception_MangoFormal/<init>()V/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/IllegalStateException_MangoFormal/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/IllegalStateException_MangoFormal/<init>()V/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/IllegalStateException_MangoFormal/<init>()V/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/NullPointerException_MangoFormal/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/NullPointerException_MangoFormal/<init>()V/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/NullPointerException_MangoFormal/<init>()V/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/RuntimeException_MangoFormal/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/RuntimeException_MangoFormal/<init>()V/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/RuntimeException_MangoFormal/<init>()V/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/<init>()V/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/<init>()V/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/<init>(C)V/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/<init>(C)V/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/<init>(Ljava.lang.StringBuffer_MangoFormal;)V/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/<init>(Ljava.lang.StringBuffer_MangoFormal;)V/'buffer' equals null reference.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/<init>(Ljava.lang.StringBuffer_MangoFormal;)V/'buffer' is defined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/<init>(Ljava.lang.String_MangoFormal;)V/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/<init>(Ljava.lang.String_MangoFormal;)V/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/<init>([C)V/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/<init>([C)V/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/<init>([CII)V/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/<init>([CII)V/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/charAt(I)C/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/charAt(I)C/'buffer' is defined.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/charAt(I)C/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/compareTo(Ljava.lang.String_MangoFormal;)I/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/compareTo(Ljava.lang.String_MangoFormal;)I/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/compareToIgnoreCase(Ljava.lang.String_MangoFormal;)I/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/compareToIgnoreCase(Ljava.lang.String_MangoFormal;)I/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/concat(Ljava.lang.String_MangoFormal;)Ljava.lang.String_MangoFormal;/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/concat(Ljava.lang.String_MangoFormal;)Ljava.lang.String_MangoFormal;/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/endsWith(Ljava.lang.String_MangoFormal;)Z/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/endsWith(Ljava.lang.String_MangoFormal;)Z/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/indexOf(I)I/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/indexOf(I)I/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/length()I/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/length()I/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/startsWith(Ljava.lang.String_MangoFormal;)Z/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/startsWith(Ljava.lang.String_MangoFormal;)Z/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/subSequence(II)Ljava.lang.CharSequence_MangoFormal;/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/subSequence(II)Ljava.lang.CharSequence_MangoFormal;/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/substring(I)Ljava.lang.String_MangoFormal;/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/substring(I)Ljava.lang.String_MangoFormal;/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/substring(II)Ljava.lang.String_MangoFormal;/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/substring(II)Ljava.lang.String_MangoFormal;/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/toCharArray()[C/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/toCharArray()[C/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/toString_MangoFormal()Ljava.lang.String_MangoFormal;/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/toString_MangoFormal()Ljava.lang.String_MangoFormal;/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/toUpperCase()Ljava.lang.String_MangoFormal;/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/toUpperCase()Ljava.lang.String_MangoFormal;/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/trim()Ljava.lang.String_MangoFormal;/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/trim()Ljava.lang.String_MangoFormal;/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/valueOf(C)Ljava.lang.String_MangoFormal;/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/valueOf(C)Ljava.lang.String_MangoFormal;/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/valueOf(D)Ljava.lang.String_MangoFormal;/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/valueOf(D)Ljava.lang.String_MangoFormal;/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/valueOf(F)Ljava.lang.String_MangoFormal;/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/valueOf(F)Ljava.lang.String_MangoFormal;/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/valueOf(I)Ljava.lang.String_MangoFormal;/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/valueOf(I)Ljava.lang.String_MangoFormal;/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/valueOf(J)Ljava.lang.String_MangoFormal;/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/valueOf(J)Ljava.lang.String_MangoFormal;/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/valueOf(Z)Ljava.lang.String_MangoFormal;/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/String_MangoFormal/valueOf(Z)Ljava.lang.String_MangoFormal;/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Throwable_MangoFormal/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Throwable_MangoFormal/<init>()V/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Throwable_MangoFormal/<init>()V/case.zip
branches/mango/Mango/mangoUserHome/system/System/java/lang/IllegalStateException_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/Worksheet for String._MangoFormal<init>(C)V.txt
Removed Paths:
-------------
branches/mango/Mango/mangoUserHome/frank/rules/param.zip
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-07-10 01:09:39
|
Revision: 1742
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1742&view=rev
Author: staats
Date: 2009-07-10 01:09:35 +0000 (Fri, 10 Jul 2009)
Log Message:
-----------
added experiment launch scripts
Modified Paths:
--------------
trunk/extensions/complexcoverage/launch/CompCov Parallel Manager Testfile MCDC.launch
trunk/extensions/complexcoverage/launch/CompCov TestFun Normal.launch
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/StartJPFManager.java
trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/test/ASWMainClass.java
trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/test/TestFile.java
Added Paths:
-----------
trunk/extensions/complexcoverage/bin/jpf-parallel-multicore
trunk/extensions/complexcoverage/bin/launch-parallel-experiment.py
trunk/extensions/complexcoverage/launch/CompCov Parallel Manager ASW MCDC.launch
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-09 21:02:05
|
Revision: 1741
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1741&view=rev
Author: frankrimlinger
Date: 2009-07-09 21:02:04 +0000 (Thu, 09 Jul 2009)
Log Message:
-----------
Fixed some problems with the new "location" type parameter. This is now working correctly and improves readability of formal expressions. Some native abstractions (hand written specifications) for Mango_String were not present, and these have been added. At this point all native abstactions in the mango package have been written, I *think*. However, there are still some methods of java.lang.String_MangoFormal and StringBuffer_MangoFormal to write before the foundation of string manipulation is solid. Then it should be possible to use the tool to build the rest of Object_MangoFormal and Class_MangoFormal.
Added stubs for the MangoFormal version of certain exception classes. The presence of these stubs is all that mango needs to create exception objects for explicitly thrown exceptions. This allowed abstraction of the NullPointerException case of Class_MangoFormal.forName(), which might come up occasionally in nominal execution flow.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/module/definition/sym/ParamSym.java
branches/mango/Mango/Mango/src/mango/ruleAction/translate/engine/TranslateValueH.java
branches/mango/Mango/Mango/src/mango/worker/engine/hash/symbolHash/SymbolHashEnterpriseAndTranslation.java
branches/mango/Mango/Mango/src/mango/worker/utilities/Util.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/translate/sym/TranslationSym.java
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
branches/mango/Mango/mangoUserHome/frank/sessions/a.zip
branches/mango/Mango/mangoUserHome/system/System/java/lang/Object_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/String_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_String.java
Added Paths:
-----------
branches/mango/Mango/Mango/src/mango/ruleAction/translate/engine/TranslateLocation.java
branches/mango/Mango/mangoUserHome/frank/rules/param.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/<init>()V/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/<init>()V/case.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/forName(Ljava.lang.String_MangoFormal;)Ljava.lang.Class_MangoFormal;/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/forName(Ljava.lang.String_MangoFormal;)Ljava.lang.Class_MangoFormal;/'className' equals null reference.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Class_MangoFormal/forName(Ljava.lang.String_MangoFormal;)Ljava.lang.Class_MangoFormal;/'className' is defined.zip
branches/mango/Mango/mangoUserHome/system/System/java/lang/Exception_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/NullPointerException_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/RuntimeException_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/java/lang/Throwable_MangoFormal.java
branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_String.append(str1,str2) worksheet.txt
branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_String.charAt worksheet.txt
branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_String.leftBracket worksheet.txt
branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_String.setValueFromStringBuffer worksheet.txt
Removed Paths:
-------------
branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_String.charAt worksheet.rtf
branches/mango/Mango/mangoUserHome/system/System/mango/lang/Mango_String.setValueFromStringBuffer worksheet.rtf
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-09 05:26:23
|
Revision: 1740
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1740&view=rev
Author: frankrimlinger
Date: 2009-07-09 05:26:16 +0000 (Thu, 09 Jul 2009)
Log Message:
-----------
Auto reset now working for cases. Fixed (another) invocation frame bug. Refined procedure for detecting thrown exception. Completed spec for <init> and hashCode() in Object_MangoFormal.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/ruleAction/coreRewriter/clinit/ThrewException.java
branches/mango/Mango/Mango/src/mango/script/gui/action/ScriptSaveAction.java
branches/mango/Mango/Mango/src/mango/worker/Worker.java
branches/mango/Mango/Mango/src/mango/worker/workFlow/model/HitemUtil.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/Invocation.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEINTERFACE.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESPECIAL.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATIC.java
branches/mango/Mango/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java
branches/mango/Mango/mangoUserHome/frank/rules/rulebase.zip
Added Paths:
-----------
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/'this' does not equal 'obj'.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/equals(Ljava.lang.Object_MangoFormal;)Z/'this' equals 'obj'.zip
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/hashCode()I/
branches/mango/Mango/mangoUserHome/frank/sessions/java/lang/Object_MangoFormal/hashCode()I/case.zip
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
