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: <st...@us...> - 2009-07-01 23:40:08
|
Revision: 1714
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1714&view=rev
Author: staats
Date: 2009-07-01 23:39:07 +0000 (Wed, 01 Jul 2009)
Log Message:
-----------
Fixed path constraint stuff
Modified Paths:
--------------
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/heuristic/PathConstraint.java-needsJava6JDK
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-07-01 23:16:08
|
Revision: 1713
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1713&view=rev
Author: staats
Date: 2009-07-01 23:16:07 +0000 (Wed, 01 Jul 2009)
Log Message:
-----------
Path constraint stuff works
Modified Paths:
--------------
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/heuristic/JavaSourceUtils.java-needsJava6JDK
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/heuristic/PathConstraint.java-needsJava6JDK
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/heuristic/PathConstraintHeuristic.java-needsJava6JDK
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-07-01 21:34:12
|
Revision: 1712
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1712&view=rev
Author: staats
Date: 2009-07-01 21:34:11 +0000 (Wed, 01 Jul 2009)
Log Message:
-----------
Added Paths:
-----------
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/heuristic/JavaSourceUtils.java-needsJava6JDK
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/heuristic/PathConstraint.java-needsJava6JDK
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/heuristic/PathConstraintHeuristic.java-needsJava6JDK
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-07-01 21:33:35
|
Revision: 1711
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1711&view=rev
Author: staats
Date: 2009-07-01 21:33:34 +0000 (Wed, 01 Jul 2009)
Log Message:
-----------
Hacked solution around need for Java 6 JDK
Removed Paths:
-------------
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/heuristic/JavaSourceUtils.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/heuristic/PathConstraint.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/heuristic/PathConstraintHeuristic.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-01 21:03:13
|
Revision: 1710
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1710&view=rev
Author: frankrimlinger
Date: 2009-07-01 21:03:05 +0000 (Wed, 01 Jul 2009)
Log Message:
-----------
Each invocation is followed by an ACATCHHANDLER which handles exceptions thrown by callee but not caught in callee. Each instruction which potentially throws and exception directly is followed by an ATHROWCREATOR. The purpose of these synthetic instructions is to route the exception to the correct handler instuctions embedded in the code block, or to the synthetic ATHROWHANDLER instruction to handle the finally clause and/or uncaught exceptions.
Fix in progress so that the ACATCHHANLDER and ATHROWCREATORs are
a) created before referenced
b) passed to the choice generator of the instruction which invokes, in the case of ACATCHHANDLER, or throws, in the case of ATHROWCREATOR, and,
c) endowed with their branches prior to scanner execution, so that scanner flow through all the handlers is accomplished.
INVOKEINTERFACE conforms to the new scheme, remains to rewire the rest of the invocations and then all the other methods throwing exceptions.
Some comments to clear up the vast cloud of confusion that has accompanied this issue.
The theory of return points is thus: each invocation in the modeled code determines which methods it potentially calls. So we get a map invocation --> {potentially_called_method}. Inverting this map gives method --> {potential_invocation_point}. By considering the next instruction after the point of invocation, we get method-->{potential_return_point}.
There are two tricky observations to make:
1) The universal connector (ucon) for a return instruction has the form OR_i (and invocation_i return_point_i). In a flat calling space, this ucon is never actually applied, because the state transition of the invoked method is already known, and so it is just applied along the branch from invocation to next instruction. However, in the case of mutual co-recursion, the return branch condition is in play. To resolve this condition the invocation point became part of the "context" of the callee frame. This context was then dragged along ball-and-chain style as the state transitions of the callee were composed, vastly increasing the complexity of the rewrite rules. But in the brave new jpf world, we have look-behind, so we can go *get* the invocation point in the rare event we need to resolve a return condition. Otherwise, we don't trouble ourselves about it at all.
2) The logic of the return point system implements (1). The reason some of this logic is commented out is historical. ATHROWCREATOR creates the branch conditions required to route an exception thrown by a non-invocation instruction. Ditto ACATCHHANDLER for invoke instructions. Originally, ATHROWCREATOR and ACATCHHANDLER folded in the return branch condition of (1) in the case of an uncaught exception. But then Marc thought, "we need to implement finally". So the return logic was commented out and replaced by a branch to the unique ATHROWHANDLER for the method.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/Invocation.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInterface.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINIT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEINTERFACE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESPECIAL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-07-01 17:18:47
|
Revision: 1709
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1709&view=rev
Author: staats
Date: 2009-07-01 17:18:35 +0000 (Wed, 01 Jul 2009)
Log Message:
-----------
fixing multi-core test gen
Modified Paths:
--------------
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/JPF_gov_nasa_jpf_complexcoverage_Debug.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/LocalJPFListener.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/MCDCTracker.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/MCDCTrackerRemote.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/ReceiveRemoteOutput.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/parallel/StartJPFManager.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-07-01 04:40:01
|
Revision: 1708
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1708&view=rev
Author: frankrimlinger
Date: 2009-07-01 04:39:26 +0000 (Wed, 01 Jul 2009)
Log Message:
-----------
Bug #1 was that the branch from an invocation instruction to the ACATCHHANDLER was not fed to the choice generated, so the SCANNER never had a chance to scan the exception handler code. There is a subtle point here. If you feed a branch to the choice generator, then updateMangoModel will be called automatically for that branch, so DO NOT call it directly. On the other hand, the branch from an invocation to the (potentially) called routine(s) are NOT passed to the choice generator since method entrypoints are handled separately by the TargetChoiceGenerator. So for these branches, you MUST call updateMangoModel directly.
Bug #2 was that the ACATCHHANDLER execute routine was just returning null. What it is supposed to do is feed the branches to the choice generated that were created by the invocation instruction buildFormalPeer call to createACatchHandlerBranching(). Ditto for ATHROWCREATOR
The fix for bug#2 is in place. Bug#1 is harder because it involves some tricky chicken-and-egg issues. This fix is in progress.
Some parts of the returnPointLink mechanism appear to be obsolete in the C++ code. Some parts of the returnPointLink mechanism are definitely still functional. Eventually this murky issue must be unravelled.
Modified Paths:
--------------
branches/mango/Mango/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ACATCHHANDLER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWCREATOR.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROWHANDLER.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKECLINIT.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEINTERFACE.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESPECIAL.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKESTATIC.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-07-01 02:37:11
|
Revision: 1707
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1707&view=rev
Author: staats
Date: 2009-07-01 01:01:09 +0000 (Wed, 01 Jul 2009)
Log Message:
-----------
Commented out errors
Modified Paths:
--------------
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/heuristic/JavaSourceUtils.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/heuristic/PathConstraint.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/heuristic/PathConstraintHeuristic.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-07-01 02:13:06
|
Revision: 1706
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1706&view=rev
Author: staats
Date: 2009-07-01 00:19:37 +0000 (Wed, 01 Jul 2009)
Log Message:
-----------
Added user-definable constraint
Modified Paths:
--------------
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/heuristic/PathConstraint.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/heuristic/PathConstraintHeuristic.java
Added Paths:
-----------
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/heuristic/JavaSourceUtils.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-30 20:52:45
|
Revision: 1705
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1705&view=rev
Author: frankrimlinger
Date: 2009-06-30 20:52:44 +0000 (Tue, 30 Jun 2009)
Log Message:
-----------
rev to marc's code to support exception handler debugging
Modified Paths:
--------------
branches/mango/MangoJPF/mangoUserHome/marc/.classpath
branches/mango/MangoJPF/mangoUserHome/marc/hypo2/src/extest/hypo2.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-30 20:50:39
|
Revision: 1704
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1704&view=rev
Author: frankrimlinger
Date: 2009-06-30 20:50:37 +0000 (Tue, 30 Jun 2009)
Log Message:
-----------
ATHROWHANDLER is not branching correctly, so that instructions (like ASTORE) that handlers normally flow into are unreachable. The problem is that the ReturnPointLinkSym mechanism is not implemented. Probably need to go back to the original C++ to figure out what is going on here. The place to start is ClassParsingAlg::linkAthrowHandler. Working with marc's hypo2 test code.
Looking ahead, some details of the jpf rewriter are becoming clear. Phase2 will terminate prior to stratification, just emitting a set of components. The component selection algorithm will pick the "best" independent component, meaning a component "near" the target method which does not depend on any non-abstracted module. A synthetic MethodInfo will be created whose "instructions" are just proxies for the vertices of this component. A new extension of JPF, called REWRITER, will be instantiated. REWRITER will just act directly on the instructions of the synthetic MethodInfo, bypassing the class loading phase altogether. The different types of component vertices will give rise to different instructions, so that component connectors can be properly interpreted and loop vertices can orchestrate the "look-behind" strategy for invariant computation. Since this strategy only involves looking backward along a single execution path, it doesn't really need the full weight of the backtracking mechanism. But the backtracking mechanism will still have its traditional role of exhausting all paths, or at least all "interesting" paths, so that targeted module will be specified in a single REWRITER pass. This will make the process much more efficient as common initial paths no longer require re-tracing for each case. An "ordinary" instruction will just handle composition with the forward predicate transformer B* ^ I*. For non-trivial non-loop-dependent branch predicates B=b1 v .. V bn, the branch condition bi can just be automatically translated and assumed, displaying automatically in the specification window. The updated state can also be translated to check for a "translation halt". Whenever there is a translation halt, the user will intervene with appropriate definitions and translation rules. Once the situation is rectified, then REWRITER will fire back up and continue generating the specification. For loop-dependent branches B, REWRITER will first try invariant look-behind to eliminate the loops. If this fails, there will be an "invariance halt". In the case of loop termination, B will consist of a set of alternative ways to exit a loop, and the user then must choose the nominal exit condition as the "termination conjecture". (In the uncommon case of more than one nominal exit, the user can declare a backtracking point to get the opportunity to explore it later.) In any case, the user must formulate a conjecture that ensures deterministic forward execution, so that mango knows what branch to take. The user must also volunteer hypotheses on the module input parameters that make the conjecture true. This is on a best-effort basis, proof of conjectures is sub-contracted to a theorem prover. Since at all times REWRITER "knows where we are", context can be zippered on as needed for computations which require context. In particular, context does not need to be present during state composition, so the whole "context resolution" issue goes away. There will also be the existing halt for module instantiation. Note that the strategies which require halting should be handled by listeners so that the instructions can concentrate on the basic issue of state transition.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/CodeSurvey.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ExceptionHandlerUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-30 15:40:44
|
Revision: 1703
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1703&view=rev
Author: frankrimlinger
Date: 2009-06-30 15:40:38 +0000 (Tue, 30 Jun 2009)
Log Message:
-----------
TheMangoFormal aliased classes in the java package were not being modeled because the java package was specified as a "mango native" package. This feature was originally introduced to allow selective modeling of a "blended" jpf/formal environment. Since blending is not a good idea, the jpf environment should always be masked in its entirety, so this feature has been eliminated. Instead, all packages in the bootclasspath are designated as mango native, and then classes within a native class are modeled if they contain "_MangoFormal" in their name. This is a temporary solution. A better solution is to introduce a "user class loader" to jpf to allow for a "user environment" that can occupy the same namespace as the boot loader. Then it will not be necessary to alias the class names and many nasty technical issues will go away. But moving on for now.
Next bug, for some reason, the total vertex for an ASTORE fails to get created during phase1. Maybe some kind of exception handler bug??
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Worker.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/CodeSurvey.java
branches/mango/MangoJPF/src/mango/intro/ConfigurationDetails.java
branches/mango/MangoJPF/src/mango/intro/LoginDialog.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-06-30 07:09:16
|
Revision: 1702
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1702&view=rev
Author: staats
Date: 2009-06-30 07:07:58 +0000 (Tue, 30 Jun 2009)
Log Message:
-----------
fixed minor bugs
Modified Paths:
--------------
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/evaluation/EvaluateParallelGeneration.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/heuristic/RandomizedSymbolicSearch.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-30 04:22:10
|
Revision: 1701
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1701&view=rev
Author: frankrimlinger
Date: 2009-06-30 04:21:40 +0000 (Tue, 30 Jun 2009)
Log Message:
-----------
Fixed various code survey bugs, so that only formal peer methods and methods which have no formal peer are added to the survey. The formal java code is still not being modeled, so this bug is still outstanding. Need to investigate the target launcher to see what is going wrong.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ClassUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/CodeSurvey.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-29 18:48:55
|
Revision: 1700
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1700&view=rev
Author: frankrimlinger
Date: 2009-06-29 18:48:51 +0000 (Mon, 29 Jun 2009)
Log Message:
-----------
Fixed various bugs. Scanner now survives both rkrug and system mangoUserHome code. However, in the system, none of the java package XXX_MangoFormal classes are modeled. Don't know why yet, but surely has something to do with the formal peer method stuff. The rest of the code appears to be modeled.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/Mango/src/mango/worker/mangoModel/BackupAlg.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MangoInvokeInstruction.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ATHROW.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-29 05:06:50
|
Revision: 1699
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1699&view=rev
Author: frankrimlinger
Date: 2009-06-29 05:06:49 +0000 (Mon, 29 Jun 2009)
Log Message:
-----------
Rewiring of MangoJPF to call ClassUtil.getFormalPeer and MethodUtil.getFormalPeer in progress. As expected, a number of subtle issues are involved. The ideal of aliasing the class names of System classes is ugly, and will stunt the growth of the formal system code. A much better solution would be to have a separate class loader for loading the formal system classes, so that the namespace collision problem goes away. However, jpf would have to be aware of this classloader as a critical requirement is that the formal system classes are also interpreted and processed at the jpf level. So for now just plow ahead with the stop-gap solution with a view to developing a precise feature request for jpf.
Modified Paths:
--------------
branches/mango/MangoJPF/Mango/src/mango/worker/Mango.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/ClassUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/CodeSurvey.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/InvocationUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/MethodUtil.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/ALOAD.java
branches/mango/MangoJPF/javapathfinder-mango-bridge/mango/scanner/bytecode/INVOKEVIRTUAL.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <fra...@us...> - 2009-06-28 15:05:10
|
Revision: 1698
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1698&view=rev
Author: frankrimlinger
Date: 2009-06-28 15:04:04 +0000 (Sun, 28 Jun 2009)
Log Message:
-----------
Modified Paths:
--------------
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.
|
|
From: <st...@us...> - 2009-06-26 23:35:22
|
Revision: 1697
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1697&view=rev
Author: staats
Date: 2009-06-26 23:35:21 +0000 (Fri, 26 Jun 2009)
Log Message:
-----------
Added path constraint stuff
Added Paths:
-----------
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/heuristic/PathConstraint.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/heuristic/PathConstraintHeuristic.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <ppa...@us...> - 2009-06-26 14:07:04
|
Revision: 1696
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1696&view=rev
Author: pparizek
Date: 2009-06-26 13:44:29 +0000 (Fri, 26 Jun 2009)
Log Message:
-----------
test programs for the RTEmbed extension,
Ant targets to run the tests
Modified Paths:
--------------
trunk/extensions/rtembed/build.xml
Added Paths:
-----------
trunk/extensions/rtembed/lib/
trunk/extensions/rtembed/lib/ant-contrib-1.0b3.jar
trunk/extensions/rtembed/test/
trunk/extensions/rtembed/test/gov/
trunk/extensions/rtembed/test/gov/nasa/
trunk/extensions/rtembed/test/gov/nasa/jpf/
trunk/extensions/rtembed/test/gov/nasa/jpf/rtembed/
trunk/extensions/rtembed/test/gov/nasa/jpf/rtembed/memory/
trunk/extensions/rtembed/test/gov/nasa/jpf/rtembed/memory/AreasCheck1.java
trunk/extensions/rtembed/test/gov/nasa/jpf/rtembed/memory/AssignmentError1.java
trunk/extensions/rtembed/test/gov/nasa/jpf/rtembed/memory/AssignmentError2.java
trunk/extensions/rtembed/test/gov/nasa/jpf/rtembed/memory/AssignmentError3.java
trunk/extensions/rtembed/test/gov/nasa/jpf/rtembed/memory/AssignmentError4.java
trunk/extensions/rtembed/test/gov/nasa/jpf/rtembed/memory/AssignmentError5.java
trunk/extensions/rtembed/test/gov/nasa/jpf/rtembed/memory/AssignmentError6.java
trunk/extensions/rtembed/test/gov/nasa/jpf/rtembed/memory/InaccessibleAreaError.java
trunk/extensions/rtembed/test/gov/nasa/jpf/rtembed/memory/NHRTError1.java
trunk/extensions/rtembed/test/gov/nasa/jpf/rtembed/memory/NHRTError2.java
trunk/extensions/rtembed/test/gov/nasa/jpf/rtembed/memory/NHRTError3.java
trunk/extensions/rtembed/test/gov/nasa/jpf/rtembed/memory/ThreadStateError.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <ppa...@us...> - 2009-06-26 07:16:24
|
Revision: 1695
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1695&view=rev
Author: pparizek
Date: 2009-06-26 07:16:19 +0000 (Fri, 26 Jun 2009)
Log Message:
-----------
initial import of the RTEmbed extension
Added Paths:
-----------
trunk/extensions/rtembed/
trunk/extensions/rtembed/Readme
trunk/extensions/rtembed/build.xml
trunk/extensions/rtembed/env/
trunk/extensions/rtembed/env/jpf/
trunk/extensions/rtembed/env/jpf/javax/
trunk/extensions/rtembed/env/jpf/javax/realtime/
trunk/extensions/rtembed/env/jpf/javax/realtime/AbsoluteTime.java
trunk/extensions/rtembed/env/jpf/javax/realtime/AsyncEventHandler.java
trunk/extensions/rtembed/env/jpf/javax/realtime/Clock.java
trunk/extensions/rtembed/env/jpf/javax/realtime/HeapMemory.java
trunk/extensions/rtembed/env/jpf/javax/realtime/HighResolutionTime.java
trunk/extensions/rtembed/env/jpf/javax/realtime/ImmortalMemory.java
trunk/extensions/rtembed/env/jpf/javax/realtime/LTMemory.java
trunk/extensions/rtembed/env/jpf/javax/realtime/MemoryArea.java
trunk/extensions/rtembed/env/jpf/javax/realtime/MemoryParameters.java
trunk/extensions/rtembed/env/jpf/javax/realtime/NoHeapRealtimeThread.java
trunk/extensions/rtembed/env/jpf/javax/realtime/PeriodicParameters.java
trunk/extensions/rtembed/env/jpf/javax/realtime/PriorityParameters.java
trunk/extensions/rtembed/env/jpf/javax/realtime/ProcessingGroupParameters.java
trunk/extensions/rtembed/env/jpf/javax/realtime/RealtimeThread.java
trunk/extensions/rtembed/env/jpf/javax/realtime/RelativeTime.java
trunk/extensions/rtembed/env/jpf/javax/realtime/ReleaseParameters.java
trunk/extensions/rtembed/env/jpf/javax/realtime/SchedulingParameters.java
trunk/extensions/rtembed/env/jpf/javax/realtime/ScopedMemory.java
trunk/extensions/rtembed/env/jvm/
trunk/extensions/rtembed/env/jvm/gov/
trunk/extensions/rtembed/env/jvm/gov/nasa/
trunk/extensions/rtembed/env/jvm/gov/nasa/jpf/
trunk/extensions/rtembed/env/jvm/gov/nasa/jpf/rtembed/
trunk/extensions/rtembed/env/jvm/gov/nasa/jpf/rtembed/JPF_javax_realtime_MemoryArea.java
trunk/extensions/rtembed/env/jvm/gov/nasa/jpf/rtembed/JPF_javax_realtime_RealtimeThread.java
trunk/extensions/rtembed/src/
trunk/extensions/rtembed/src/gov/
trunk/extensions/rtembed/src/gov/nasa/
trunk/extensions/rtembed/src/gov/nasa/jpf/
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/memory/
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/memory/MemoryAreaInfo.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/memory/MemoryAreasChecker.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/memory/RealtimeThreadInfo.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/PlatformSpecificInstructionFactory.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/PlatformSpecificSchedulerFactory.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/ThreadChoiceWithFixedProcessorCount.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/ARETURN.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/ATHROW.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/DRETURN.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/FRETURN.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/GOTO.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/GOTO_W.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/IFEQ.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/IFGE.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/IFGT.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/IFLE.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/IFLT.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/IFNE.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/IFNONNULL.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/IFNULL.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/IF_ACMPEQ.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/IF_ACMPNE.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/IF_ICMPEQ.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/IF_ICMPGE.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/IF_ICMPGT.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/IF_ICMPLE.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/IF_ICMPLT.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/IF_ICMPNE.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/INVOKEINTERFACE.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/INVOKESPECIAL.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/INVOKESTATIC.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/INVOKEVIRTUAL.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/IRETURN.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/IfInstructionAsYieldPoint.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/JSR.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/JSR_W.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/LRETURN.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/restrictpar/bytecode/RETURN.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/utils/
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/utils/StateSpaceTraversalMon.java
trunk/extensions/rtembed/src/gov/nasa/jpf/rtembed/utils/TimeConstrainedJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-06-26 05:57:00
|
Revision: 1694
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1694&view=rev
Author: staats
Date: 2009-06-26 05:56:58 +0000 (Fri, 26 Jun 2009)
Log Message:
-----------
fixed bugs in concretization heuristic
Modified Paths:
--------------
trunk/extensions/complexcoverage/launch/CompCov TestFun Normal.launch
trunk/extensions/complexcoverage/launch/CompCov TestFun Symbolic Concretize.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/StartJPFManager.java
trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/test/ASWMainClass.java
Added Paths:
-----------
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/evaluation/
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/evaluation/EvaluateParallelGeneration.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2009-06-26 05:33:36
|
Revision: 1693
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1693&view=rev
Author: pcmehlitz
Date: 2009-06-26 05:33:34 +0000 (Fri, 26 Jun 2009)
Log Message:
-----------
* swapped ResourceBundle (which is a base class) with a native peer for java.util.logging.Level to make basic logging work (seems it just needs the localized Level name). It's not producing any output, but it also doesn't choke. Since ResourceBundles are heavily used, and ResourceBundle itself is an abstract base, we should not replace it with a partial model that breaks the hierarchy. It certainly makes sense to have a full model of the whole hierarchy at some point
Added Paths:
-----------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_util_logging_Level.java
Removed Paths:
-------------
trunk/env/jpf/java/util/ResourceBundle.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-06-26 01:14:34
|
Revision: 1691
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1691&view=rev
Author: staats
Date: 2009-06-26 00:40:46 +0000 (Fri, 26 Jun 2009)
Log Message:
-----------
Added backtracking to concretization
Modified Paths:
--------------
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/JPF_gov_nasa_jpf_complexcoverage_Debug.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/TestSuite.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/heuristic/ConcretizeVariables.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <tel...@us...> - 2009-06-26 01:08:48
|
Revision: 1692
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1692&view=rev
Author: telcontar
Date: 2009-06-26 01:08:42 +0000 (Fri, 26 Jun 2009)
Log Message:
-----------
* *.java: Added Copyright/license headers, indented file with two spaces each.
Modified Paths:
--------------
trunk/env/jpf/java/util/ResourceBundle.java
trunk/env/jpf/java/util/logging/FileHandler.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <st...@us...> - 2009-06-25 23:36:57
|
Revision: 1690
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1690&view=rev
Author: staats
Date: 2009-06-25 23:36:23 +0000 (Thu, 25 Jun 2009)
Log Message:
-----------
Added concretize heuristic
Modified Paths:
--------------
trunk/extensions/complexcoverage/launch/CompCov Parallel Client.launch
trunk/extensions/complexcoverage/launch/CompCov TestFun Normal.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/choice/SymbolicChoiceGenerator.java
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/heuristic/SymbolicSearchHeuristicBase.java
trunk/extensions/complexcoverage/test/gov/nasa/jpf/complexcoverage/test/TestFile.java
Added Paths:
-----------
trunk/extensions/complexcoverage/launch/CompCov TestFun Symbolic Concretize.launch
trunk/extensions/complexcoverage/src/gov/nasa/jpf/complexcoverage/heuristic/ConcretizeVariables.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
