Menu
▾
▴
javapathfinder-devel — development related topics (your place if you work with the sources)
You can subscribe to this list here.
| 2005 |
Jan
|
Feb
|
Mar
|
Apr
(9) |
May
(38) |
Jun
(13) |
Jul
(3) |
Aug
(14) |
Sep
(25) |
Oct
(44) |
Nov
(6) |
Dec
(2) |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 2006 |
Jan
(4) |
Feb
(14) |
Mar
(16) |
Apr
(2) |
May
(1) |
Jun
(2) |
Jul
(2) |
Aug
(1) |
Sep
(1) |
Oct
|
Nov
(3) |
Dec
(1) |
| 2007 |
Jan
(3) |
Feb
(39) |
Mar
(30) |
Apr
(31) |
May
(20) |
Jun
(72) |
Jul
(41) |
Aug
(78) |
Sep
(48) |
Oct
(59) |
Nov
(31) |
Dec
(47) |
| 2008 |
Jan
(18) |
Feb
(37) |
Mar
(45) |
Apr
(78) |
May
(16) |
Jun
|
Jul
(8) |
Aug
(10) |
Sep
(23) |
Oct
(10) |
Nov
(12) |
Dec
(1) |
| 2009 |
Jan
(4) |
Feb
|
Mar
(3) |
Apr
(1) |
May
(1) |
Jun
(1) |
Jul
|
Aug
|
Sep
(1) |
Oct
(3) |
Nov
(2) |
Dec
|
| 2010 |
Jan
(1) |
Feb
|
Mar
|
Apr
(1) |
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
| 2013 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
(2) |
Oct
|
Nov
|
Dec
|
|
From: pcm <pcm...@us...> - 2005-12-23 19:32:02
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/bytecode In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv26358 Modified Files: MONITORENTER.java Log Message: was missing a check for NullpointerExceptions, if attempting to acquire lock for null object Index: MONITORENTER.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/bytecode/MONITORENTER.java,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -u -d -r1.1.1.1 -r1.2 --- MONITORENTER.java 26 Apr 2005 19:44:15 -0000 1.1.1.1 +++ MONITORENTER.java 23 Dec 2005 19:31:54 -0000 1.2 @@ -31,11 +31,15 @@ * ..., objectref => ... */ public class MONITORENTER extends Instruction { + public boolean isExecutable (SystemState ss, KernelState ks, ThreadInfo th) { int objref = th.peek(); - boolean isExec = ks.da.get(objref).canLock(th); - - return isExec; + if (objref == -1) { + return true; // force error + } + + ElementInfo ei = ks.da.get(objref); + return ei.canLock(th); } public void setPeer (org.apache.bcel.generic.Instruction i, ConstantPool cp) { @@ -43,14 +47,23 @@ public Instruction execute (SystemState ss, KernelState ks, ThreadInfo th) { int objref = th.pop(); - - ks.da.get(objref).lock(th); - + if (objref == -1) { + return th.createAndThrowException("java.lang.NullPointerException", + "attempt to acquire lock for null object"); + } + + ElementInfo ei = ks.da.get(objref); + ei.lock(th); + return getNext(th); } public boolean isSchedulingRelevant (SystemState ss, KernelState ks, ThreadInfo ti) { int objref = ti.peek(); + if (objref == -1) { + return true; // force error + } + ElementInfo ei = ks.da.get(objref); if (mi.isBodySchedulingRelevant(ti,ei) && (ei.getLockCount() == 0)) { |
|
From: John P. <joh...@us...> - 2005-11-21 18:51:29
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv7472/src/gov/nasa/jpf/jvm Modified Files: StaticArea.java Log Message: * removed unused parameter in call Index: StaticArea.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/StaticArea.java,v retrieving revision 1.2 retrieving revision 1.3 diff -u -d -r1.2 -r1.3 --- StaticArea.java 3 May 2005 03:31:59 -0000 1.2 +++ StaticArea.java 21 Nov 2005 18:51:22 -0000 1.3 @@ -181,7 +181,7 @@ } StaticElementInfo createElementInfo (ClassInfo ci, int classObjRef) { - Fields f = ci.createStaticFields(this); + Fields f = ci.createStaticFields(); Monitor m = new Monitor(); StaticElementInfo ei = new StaticElementInfo(f, m, classObjRef); |
|
From: John P. <joh...@us...> - 2005-11-21 18:50:13
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/bytecode In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv7285/src/gov/nasa/jpf/jvm/bytecode Modified Files: StaticFieldInstruction.java Log Message: * throw exceptions if field lookup is failing badly rather than let a null go off to be immediately dereferenced Index: StaticFieldInstruction.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/bytecode/StaticFieldInstruction.java,v retrieving revision 1.3 retrieving revision 1.4 diff -u -d -r1.3 -r1.4 --- StaticFieldInstruction.java 17 Oct 2005 04:13:13 -0000 1.3 +++ StaticFieldInstruction.java 21 Nov 2005 18:50:05 -0000 1.4 @@ -37,6 +37,14 @@ if (ci != null) { fi = ci.getStaticField(fname); } + else { + throw new gov.nasa.jpf.JPFException("could not find ClassInfo for class named "+className); + } + if (fi == null){ + throw new gov.nasa.jpf.JPFErrorException( + "could not find static field "+fname+" in class "+className); + + } } return fi; } |
|
From: John P. <joh...@us...> - 2005-11-21 18:47:39
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv6778/src/gov/nasa/jpf/jvm Modified Files: ClassInfo.java Log Message: * look for static fields in interfaces too * added some comments on interface related code * removed a random parameter that wasn't being used Index: ClassInfo.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/ClassInfo.java,v retrieving revision 1.4 retrieving revision 1.5 diff -u -d -r1.4 -r1.5 --- ClassInfo.java 23 Oct 2005 04:41:01 -0000 1.4 +++ ClassInfo.java 21 Nov 2005 18:47:32 -0000 1.5 @@ -316,7 +316,8 @@ * Loads the class specified. * @param cname The fully qualified name of the class to load. * @return Returns the ClassInfo for the classname passed in, - * or null. + * or null if null is passed in. + * @throws JPFException if class cannot be found (by BCEL) */ public static synchronized ClassInfo getClassInfo (String cname) { JavaClass jc = null; @@ -413,6 +414,14 @@ c = c.superClass; } + //interfaces can have static fields too + Iterator i = getAllInterfaces().iterator(); + while (i.hasNext()) { + String interface_name = (String)i.next(); + fi = ClassInfo.getClassInfo(interface_name).getDeclaredStaticField(fName); + if (fi != null) return fi; + } + return null; } @@ -980,6 +989,10 @@ } } + /** + * get names of all interfaces + * @return a Set of String interface names + */ Set getAllInterfaces () { if (allInterfaces == null) { HashSet set = new HashSet(); @@ -1068,7 +1081,7 @@ * Creates the fields for a class. This gets called by the StaticArea * when a class is loaded. */ - Fields createStaticFields (StaticArea staticArea) { + Fields createStaticFields () { return new StaticFields(this); } @@ -1104,6 +1117,11 @@ return new HashMap(0); } + /** + * Loads the ClassInfo for named class. + * @param set - a Set to which the interface names (String) are added + * @param ci - class to find interfaces for. + */ void loadInterfaceRec (Set set, ClassInfo ci) { if (ci != null) { Iterator it = ci.interfaces.iterator(); |
|
From: <up...@am...> - 2005-11-10 13:07:00
|
<HTML> <meta name="generator" content="Namo WebEditor v5.0(Trial)"> <IMG height=30 src="http://g-images.amazon.com/images/G/04/icons/amazon-logo.gif" width=140> <TABLE cellSpacing=0 cellPadding=0 width=600 align=center border=0> <TBODY> <TR> <TD><IMG height=2 src="pp.files/pixel.gif" width=2></TD></TR></TBODY></TABLE> <P><FONT size=2><FONT face=Verdana>Dear <STRONG><STRONG><SPAN style="FONT-SIZE: 10pt; COLOR: black; FONT-FAMILY: Verdana">Amazon<SUP>® </SUP></SPAN></STRONG> </STRONG>member</FONT>, <BR></font><BR></P> <P><FONT face=Verdana size=2>It has come to our attention that your <SPAN style="FONT-SIZE: 10pt; COLOR: black; FONT-FAMILY: Verdana"><STRONG>Amazon</STRONG></SPAN> order Information records are <BR>out of date.That requires you to update the order Information If you could <BR>please take 5-10 minutes out of your online <FONT face=Verdana size=2> experience and update <BR>your order records, you will not run into any future problems with Amazon <BR>online service. <BR> </FONT></FONT></P> <P><FONT face=Verdana size=2><FONT face=Verdana size=2>However, failure to update your records will result in account termination. <BR>Please update your records in maximum 24 hours. </FONT> <BR><BR>Once you have updated records, your <SPAN style="FONT-SIZE: 10pt; COLOR: black; FONT-FAMILY: Verdana"><STRONG>Amazon</STRONG></SPAN> session will not be <BR>interrupted and will continue as normal. </FONT></P> <P><FONT face=Verdana size=2>To update your <SPAN style="FONT-SIZE: 10pt; COLOR: black; FONT-FAMILY: Verdana"><STRONG>Amazon</STRONG></SPAN> order Information click on the following link: <BR></FONT></P> <p><FONT face=Verdana size=2> </FONT><SPAN class=treb><SPAN style="FONT-SIZE: 9pt; FONT-FAMILY: Verdana"><A onclick="return ShowLinkWarning()" href="http://212.44.154.205/icons/exec/register/login/index.html" target=_blank>http://www.amazon.com/exec/obidos/account-access-login/ref=/index</A></SPAN></SPAN></p> <P> <FONT face=Verdana size=2>Best Regards , <BR><SPAN style="FONT-SIZE: 10pt; COLOR: black; FONT-FAMILY: Verdana"><STRONG>Amazon<SUP> </SUP><SPAN style="FONT-SIZE: 10pt; COLOR: black; FONT-FAMILY: Verdana">Security </SPAN></STRONG><SPAN style="FONT-SIZE: 10pt; COLOR: black; FONT-FAMILY: Verdana"><STRONG>Departament</STRONG></SPAN></SPAN> </FONT></P> <P><FONT face=Verdana size=2> </font> <p><FONT face=Verdana size=2> <SPAN class="tiny"><A href="http://www.amazon.com/exec/obidos/tg/browse/-/508088/103-3650287-7644618"><font color="#006699" size="2">Conditions of Use</font></A><font color="#006699" size="2"> | </font><A href="http://www.amazon.com/exec/obidos/tg/browse/-/468496/103-3650287-7644618"><font color="#006699" size="2">Privacy Notice</font></A><font color="#006699" size="2"> </font><font size="2">© 1995-2005, Amazon.com, Inc. or its affiliates. </font></SPAN></p> <TABLE cellSpacing=0 cellPadding=0 width=600 align=center border=0> <TBODY> <TR> <TD><IMG height=2 src="pp.files/pixel.gif" width=2></TD></TR></TBODY></TABLE> <P> </HTML> |
|
From: John P. <joh...@na...> - 2005-11-02 00:28:40
|
Hi Marcelo,
I can at least tell you what's happening now.
The instruction code is part of JPF and is running on the normal JVM.
At this level, Verify.random() is just implemented as random - this way
you can execute a "model" on a standard JVM.
When you run code with Verify.random() on JPF, then it is trapped (look
for JPF_gov_nasa_jpf_jvm_Verify in /env/jvm) and it hooks into JPF to
create the nondeterministic choice.
You might look at that code to see how to create a choice from within
JPF, but the details of that are out of my area.
John
Marcelo d'Amorim wrote:
>
> Dear JPF developers,
>
> I downloaded the JPF distribution from sourceforge and have been working
> with it for almost 4 days. I would like if you could give me some
> guidance.
>
> I am evaluating expressions symbolically throughout the JVM. For
> instance, instead of a concrete int, we are storing an object holding a
> symbolic expression that corresponds to the int value. I managed to
> change all bytecodes but I am holding the branching instructions.
>
> I would like to make the branch instructions, say IF_ICMPEQ (which
> expects two integers on the stack), look like:
>
> if (Verify.randomBoolean()) {
> MyPath.addConstraint("something that represents x = y") ;
> } else {
> MyPath.addConstraint("something that represents x != y");
> }
>
> If I create a piece of Java code containing the piece of code above, JPF
> will indeed explore both branches. However, if I put this code inside
> the body of gov.nasa.jpf.jvm.bytecode.IF_ICMPEQ it will only explore
> _one_ (I also tried to make a call in the representation level -- see
> below).
>
> Below is a fragment of the code of IF_ICMPEQ.
>
> Suggestions appreciated.
>
> thanks,
>
> Marcelo
>
>
>
>
> public Instruction execute (SystemState ss, KernelState ks, ThreadInfo
> th) {
> int v1 = th.pop(); // reference to a symbolic expression
> int v2 = th.pop(); // reference to a ...
> // ==============================================================
> String className = SymclatVerify.class.getName();
> ClassInfo ci = ClassInfo.getClassInfo(className) ;
> // the method fork() is static and looks like the code above
> gov.nasa.jpf.jvm.MethodInfo mInfo = ci.getMethod("fork()", false);
> th.executeMethod(mInfo); // execute the method
> // the method fork() returns randomly true or false
> long resultB = th.getReturnValue() ;
> gov.nasa.jpf.jvm.ElementInfo eInfo = DynamicArea.getHeap().get((int)
> resultB); int result2 = IntExpression.getIntConstant(th , (int) resultB) ;
> //===============================================================
>
> // JPF code
> if (result2 == 1) { // if (result) {
> CoverageManager.incIFBranch(th.index, indexTrue);
> ...
>
>
> -------------------------------------------------------
> SF.Net email is sponsored by:
> Tame your development challenges with Apache's Geronimo App Server.
> Download
> it for free - -and be entered to win a 42" plasma tv or your very own
> Sony(tm)PSP. Click here to play: http://sourceforge.net/geronimo.php
> _______________________________________________
> Javapathfinder-devel mailing list
> Jav...@li...
> https://lists.sourceforge.net/lists/listinfo/javapathfinder-devel
--
John Penix PhD. john.penix+nasa.gov http://ase.arc.nasa.gov/jpenix/
Robust Software Engineering Group ph:(650)604-6576 bld:N296 rm:268
Intelligent Systems Division NASA Ames Research Center Mt.View CA
|
|
From: Marcelo d'A. <da...@cs...> - 2005-11-01 21:46:37
|
Dear JPF developers,
I downloaded the JPF distribution from sourceforge and have been working
with it for almost 4 days. I would like if you could give me some
guidance.
I am evaluating expressions symbolically throughout the JVM. For
instance, instead of a concrete int, we are storing an object holding a
symbolic expression that corresponds to the int value. I managed to
change all bytecodes but I am holding the branching instructions.
I would like to make the branch instructions, say IF_ICMPEQ (which
expects two integers on the stack), look like:
if (Verify.randomBoolean()) {
MyPath.addConstraint("something that represents x = y") ;
} else {
MyPath.addConstraint("something that represents x != y");
}
If I create a piece of Java code containing the piece of code above, JPF
will indeed explore both branches. However, if I put this code inside the
body of gov.nasa.jpf.jvm.bytecode.IF_ICMPEQ it will only explore _one_ (I
also tried to make a call in the representation level -- see below).
Below is a fragment of the code of IF_ICMPEQ.
Suggestions appreciated.
thanks,
Marcelo
public Instruction execute (SystemState ss, KernelState ks, ThreadInfo th) {
int v1 = th.pop(); // reference to a symbolic expression
int v2 = th.pop(); // reference to a ...
// ==============================================================
String className = SymclatVerify.class.getName();
ClassInfo ci = ClassInfo.getClassInfo(className) ;
// the method fork() is static and looks like the code above
gov.nasa.jpf.jvm.MethodInfo mInfo = ci.getMethod("fork()", false);
th.executeMethod(mInfo); // execute the method
// the method fork() returns randomly true or false
long resultB = th.getReturnValue() ;
gov.nasa.jpf.jvm.ElementInfo eInfo = DynamicArea.getHeap().get((int) resultB);
int result2 = IntExpression.getIntConstant(th , (int) resultB) ;
//===============================================================
// JPF code
if (result2 == 1) { // if (result) {
CoverageManager.incIFBranch(th.index, indexTrue);
...
|
|
From: Willem V. <wv...@us...> - 2005-10-25 23:36:57
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv20505/src/gov/nasa/jpf/tools Modified Files: SearchMonitor.java Log Message: * added max search depth Index: SearchMonitor.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/SearchMonitor.java,v retrieving revision 1.4 retrieving revision 1.5 diff -u -d -r1.4 -r1.5 --- SearchMonitor.java 25 Oct 2005 22:05:44 -0000 1.4 +++ SearchMonitor.java 25 Oct 2005 23:36:49 -0000 1.5 @@ -60,7 +60,8 @@ long startTime; long startFreeMemory; - int searchLevel; + int searchLevel=0; + int maxSearchLevel=0; int newStates; int endStates; @@ -95,6 +96,9 @@ if (search.isNewState()) { searchLevel = search.getSearchDepth(); + if (searchLevel > maxSearchLevel) + maxSearchLevel = searchLevel; + newStates++; currentSVLength = ((JVM)(search.getVM())).getSystemState().getCurrentStateVectorLength(); @@ -213,7 +217,10 @@ out.println(); out.print(" search depth: "); - out.println(searchLevel); + out.print(searchLevel); + out.print(" (max: "); + out.print(maxSearchLevel); + out.println(")"); out.print(" new states: "); out.println(newStates); |
|
From: Willem V. <wv...@us...> - 2005-10-25 22:05:56
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv9280/src/gov/nasa/jpf/tools Modified Files: SearchMonitor.java StateSpaceDot.java Log Message: * Made changes to allow the state vector length to be shown * by the SearchMonitor (includes the max length) Index: StateSpaceDot.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/StateSpaceDot.java,v retrieving revision 1.8 retrieving revision 1.9 diff -u -d -r1.8 -r1.9 --- StateSpaceDot.java 8 Sep 2005 18:28:12 -0000 1.8 +++ StateSpaceDot.java 25 Oct 2005 22:05:44 -0000 1.9 @@ -339,6 +339,7 @@ */ private void addNode(StateInformation state) throws IOException { if (state.is_new) { + System.out.println("Adding Node " + state.id); if (format==GDF_FORMAT) { graph.write("st" + state.id + ",\"" + state.id); if (state.error != null) { @@ -435,6 +436,7 @@ */ private void addEdge(int old_id, int new_id, Search state) throws IOException { int my_id = edge_id++; + System.out.println("Adding Edge from " + old_id + " to " + new_id); if (format==GDF_FORMAT) { Transition trans=state.getTransition(); int thread = trans.getThread(); Index: SearchMonitor.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/SearchMonitor.java,v retrieving revision 1.3 retrieving revision 1.4 diff -u -d -r1.3 -r1.4 --- SearchMonitor.java 6 Oct 2005 21:05:53 -0000 1.3 +++ SearchMonitor.java 25 Oct 2005 22:05:44 -0000 1.4 @@ -29,6 +29,7 @@ import gov.nasa.jpf.Config; import gov.nasa.jpf.JPF; +import gov.nasa.jpf.jvm.JVM; import gov.nasa.jpf.Search; import gov.nasa.jpf.SearchListener; @@ -77,6 +78,10 @@ boolean isHeuristic = false; int queueSize = 0; + int currentSVLength = 0; + int maxSVLength = 0; + + /* * SearchListener interface */ @@ -90,7 +95,12 @@ if (search.isNewState()) { searchLevel = search.getSearchDepth(); - newStates++; + newStates++; + + currentSVLength = ((JVM)(search.getVM())).getSystemState().getCurrentStateVectorLength(); + + if (currentSVLength > maxSVLength) + maxSVLength = currentSVLength; if (search.isEndState()) { endStates++; @@ -247,6 +257,12 @@ out.print(" free memory [kB]: "); out.println(freeMemory / 1024); + out.print(" StateVector Len: "); + out.print(currentSVLength); + out.print(" (max: "); + out.print(maxSVLength); + out.println(")"); + out.println(); } |
|
From: Willem V. <wv...@us...> - 2005-10-25 22:05:56
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/search/heuristic In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv9280/src/gov/nasa/jpf/search/heuristic Modified Files: HeuristicSearch.java Log Message: * Made changes to allow the state vector length to be shown * by the SearchMonitor (includes the max length) Index: HeuristicSearch.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/search/heuristic/HeuristicSearch.java,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -u -d -r1.1.1.1 -r1.2 --- HeuristicSearch.java 26 Apr 2005 19:44:19 -0000 1.1.1.1 +++ HeuristicSearch.java 25 Oct 2005 22:05:45 -0000 1.2 @@ -175,12 +175,13 @@ } } - backtrack(); // back to our parent, to get the next child - notifyStateBacktracked(); + // back to our parent, to get the next child + backtrack(); + notifyStateBacktracked(); } } else { // no next state, nothing to queue - backtrack(); + backtrack(); notifyStateBacktracked(); } } |
|
From: Willem V. <wv...@us...> - 2005-10-25 22:05:55
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv9280/src/gov/nasa/jpf/jvm Modified Files: SystemState.java Log Message: * Made changes to allow the state vector length to be shown * by the SearchMonitor (includes the max length) Index: SystemState.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/SystemState.java,v retrieving revision 1.6 retrieving revision 1.7 diff -u -d -r1.6 -r1.7 --- SystemState.java 23 Oct 2005 04:41:01 -0000 1.6 +++ SystemState.java 25 Oct 2005 22:05:44 -0000 1.7 @@ -94,6 +94,9 @@ /** set to true if garbage collection is necessary */ boolean GCNeeded = false; + + /** maximum length of the state vector encountered so far */ + int currentStateVectorLength = 0; /** * Creates a new system state. @@ -177,7 +180,13 @@ } public int[] getStoringData () { - return ks.getStoringData(); + int[] storingData = ks.getStoringData(); + currentStateVectorLength = storingData.length; + return storingData; + } + + public int getCurrentStateVectorLength() { + return currentStateVectorLength; } public ThreadInfo getThread (int index) { |
|
From: Willem V. <wv...@us...> - 2005-10-25 22:05:55
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/bytecode In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv9280/src/gov/nasa/jpf/jvm/bytecode Modified Files: ATHROW.java Log Message: * Made changes to allow the state vector length to be shown * by the SearchMonitor (includes the max length) Index: ATHROW.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/bytecode/ATHROW.java,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -u -d -r1.1.1.1 -r1.2 --- ATHROW.java 26 Apr 2005 19:44:09 -0000 1.1.1.1 +++ ATHROW.java 25 Oct 2005 22:05:44 -0000 1.2 @@ -46,4 +46,5 @@ public int getByteCode () { return 0xBF; } + } |
|
From: Willem V. <wv...@us...> - 2005-10-25 22:05:53
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/search In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv9280/src/gov/nasa/jpf/search Modified Files: AbstractSearch.java DFSearch.java Log Message: * Made changes to allow the state vector length to be shown * by the SearchMonitor (includes the max length) Index: AbstractSearch.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/search/AbstractSearch.java,v retrieving revision 1.2 retrieving revision 1.3 diff -u -d -r1.2 -r1.3 --- AbstractSearch.java 7 Oct 2005 21:27:34 -0000 1.2 +++ AbstractSearch.java 25 Oct 2005 22:05:45 -0000 1.3 @@ -404,7 +404,7 @@ return true; } - + /** * DOCUMENT ME! */ Index: DFSearch.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/search/DFSearch.java,v retrieving revision 1.2 retrieving revision 1.3 diff -u -d -r1.2 -r1.3 --- DFSearch.java 3 May 2005 03:31:59 -0000 1.2 +++ DFSearch.java 25 Oct 2005 22:05:45 -0000 1.3 @@ -68,10 +68,14 @@ int maxDepth = getMaxSearchDepth(); depth = 0; - notifySearchStarted(); while (!done) { + + + //if (depth < 0) + // System.out.println("DEPTH = " + depth + "GGGGGGGGGGGGGGGGGGGGGGGGGGG"); + if ( !isNewState || isEndState) { if (!backtrack()) { // backtrack not possible, done break; @@ -80,6 +84,10 @@ depth--; notifyStateBacktracked(); } + + //if (vm.getPathLength() != depth) + // System.out.println("path = " + vm.getPathLength() + " depth = " + depth); + if (forward()) { notifyStateAdvanced(); @@ -88,7 +96,7 @@ break; } - if (isNewState) { + //if (isNewState()) { depth++; if (depth >= maxDepth) { @@ -101,7 +109,7 @@ // can't go on, we exhausted our memory break; } - } + //} } else { // state was processed notifyStateProcessed(); } |
|
From: Willem V. <wv...@us...> - 2005-10-25 22:05:52
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv9280/src/gov/nasa/jpf Modified Files: Search.java Log Message: * Made changes to allow the state vector length to be shown * by the SearchMonitor (includes the max length) Index: Search.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/Search.java,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -u -d -r1.1.1.1 -r1.2 --- Search.java 26 Apr 2005 19:43:56 -0000 1.1.1.1 +++ Search.java 25 Oct 2005 22:05:44 -0000 1.2 @@ -92,5 +92,11 @@ * start the search process - this is the main driver for the VirtualMachine */ void search (); + + /** + * Get the VM that is used by the search + * @return + */ + VM getVM(); } |
|
From: John P. <joh...@us...> - 2005-10-23 04:41:10
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv30920/src/gov/nasa/jpf/jvm Modified Files: MJIEnv.java DynamicElementInfo.java ClassInfo.java StaticElementInfo.java SystemState.java State.java ElementInfo.java JVM.java UncaughtException.java DynamicFields.java ThreadInfo.java StaticFields.java Removed Files: Reference.java Log Message: * changed getField interface to be getField (searches up class hierarchy from current class) or getDeclared field (looks only in the specified class) no longer uses null parameter to switch between these two cases * got rid of Reference interface because it was going to have to get bigger, but it was tagged for eventual removal replaced uses of Reference with ElementInfo Index: ElementInfo.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/ElementInfo.java,v retrieving revision 1.3 retrieving revision 1.4 diff -u -d -r1.3 -r1.4 --- ElementInfo.java 7 Oct 2005 21:27:34 -0000 1.3 +++ ElementInfo.java 23 Oct 2005 04:41:01 -0000 1.4 @@ -33,7 +33,7 @@ * * @see gov.nasa.jpf.jvm.FieldInfo */ -public abstract class ElementInfo implements Storable, Reference, Cloneable { +public abstract class ElementInfo implements Storable, Cloneable { static final int storingDataLength = 3; protected static HashPool fieldsPool = new HashPool(); @@ -273,21 +273,11 @@ return fields.getClassInfo(); } - abstract protected FieldInfo getFieldInfo(String clsBase, String fname); + abstract protected FieldInfo getDeclaredFieldInfo(String clsBase, String fname); abstract protected ElementInfo getElementInfo(ClassInfo ci); - protected FieldInfo getFieldInfo(String fname) { - return getFieldInfo(null, fname); - } - - public int getIntField(String fname) { - return getIntField(fname, null); - } - - public long getLongField(String fname) { - return getLongField(fname, null); - } + abstract protected FieldInfo getFieldInfo(String fname); public void setIntField(FieldInfo fi, int value) { //checkFieldInfo(fi); // in case somebody caches and uses the wrong @@ -302,12 +292,12 @@ } } - public void setIntField(String fname, String clsBase, int value) { - setIntField(getFieldInfo(clsBase, fname), value); + public void setDeclaredIntField(String fname, String clsBase, int value) { + setIntField(getDeclaredFieldInfo(clsBase, fname), value); } public void setIntField(String fname, int value) { - setIntField(fname, null, value); + setIntField(getFieldInfo(fname), value); } public void setLongField(String fname, long value) { @@ -380,16 +370,16 @@ } } - public void setReferenceField(String fname, String clsBase, int value) { - setReferenceField(getFieldInfo(clsBase, fname), value); + public void setDeclaredReferenceField(String fname, String clsBase, int value) { + setReferenceField(getDeclaredFieldInfo(clsBase, fname), value); } public void setReferenceField(String fname, int value) { - setReferenceField(fname, null, value); + setReferenceField(getFieldInfo(fname), value); } - public int getReferenceField(String fname, String clsBase) { - FieldInfo fi = getFieldInfo(clsBase, fname); + public int getDeclaredReferenceField(String fname, String clsBase) { + FieldInfo fi = getDeclaredFieldInfo(clsBase, fname); ElementInfo ei = getElementInfo(fi.getClassInfo()); if (!fi.isReference()) { @@ -399,61 +389,118 @@ } public int getReferenceField(String fname) { - return getReferenceField(fname, null); + FieldInfo fi = getFieldInfo(fname); + ElementInfo ei = getElementInfo(fi.getClassInfo()); + + if (!fi.isReference()) { + throw new JPFException("not a reference field: " + fi.getName()); + } + return ei.fields.getIntValue(fi.getStorageOffset()); } - public int getIntField(String fname, String clsBase) { + + public int getDeclaredIntField(String fname, String clsBase) { // be aware of that static fields are not flattened (they are unique), i.e. // the FieldInfo might actually refer to another ClassInfo/StaticElementInfo - FieldInfo fi = getFieldInfo(clsBase, fname); + FieldInfo fi = getDeclaredFieldInfo(clsBase, fname); ElementInfo ei = getElementInfo(fi.getClassInfo()); return ei.fields.getIntValue(fi.getStorageOffset()); } - public void setLongField(String fname, String clsBase, long value) { - FieldInfo fi = getFieldInfo(clsBase, fname); + public int getIntField(String fname) { + // be aware of that static fields are not flattened (they are unique), i.e. + // the FieldInfo might actually refer to another ClassInfo/StaticElementInfo + FieldInfo fi = getFieldInfo(fname); + ElementInfo ei = getElementInfo(fi.getClassInfo()); + return ei.fields.getIntValue(fi.getStorageOffset()); + } + + public void setDeclaredLongField(String fname, String clsBase, long value) { + FieldInfo fi = getDeclaredFieldInfo(clsBase, fname); ElementInfo ei = getElementInfo(fi.getClassInfo()); ei.cloneFields().setLongValue(fi.getStorageOffset(), value); } - public long getLongField(String fname, String clsBase) { - FieldInfo fi = getFieldInfo(clsBase, fname); + public long getDeclaredLongField(String fname, String clsBase) { + FieldInfo fi = getDeclaredFieldInfo(clsBase, fname); ElementInfo ei = getElementInfo(fi.getClassInfo()); return ei.fields.getLongValue(fi.getStorageOffset()); } - public boolean getBooleanField(String fname, String refType) { - FieldInfo fi = getFieldInfo(refType, fname); + public long getLongField(String fname) { + FieldInfo fi = getFieldInfo(fname); + ElementInfo ei = getElementInfo(fi.getClassInfo()); + return ei.fields.getLongValue(fi.getStorageOffset()); + } + + public boolean getDeclaredBooleanField(String fname, String refType) { + FieldInfo fi = getDeclaredFieldInfo(refType, fname); ElementInfo ei = getElementInfo(fi.getClassInfo()); return ei.fields.getBooleanValue(fi.getStorageOffset()); } - public byte getByteField(String fname, String refType) { - FieldInfo fi = getFieldInfo(refType, fname); + public boolean getBooleanField(String fname) { + FieldInfo fi = getFieldInfo(fname); + ElementInfo ei = getElementInfo(fi.getClassInfo()); + return ei.fields.getBooleanValue(fi.getStorageOffset()); + } + + public byte getDeclaredByteField(String fname, String refType) { + FieldInfo fi = getDeclaredFieldInfo(refType, fname); ElementInfo ei = getElementInfo(fi.getClassInfo()); return ei.fields.getByteValue(fi.getStorageOffset()); } - public char getCharField(String fname, String refType) { - FieldInfo fi = getFieldInfo(refType, fname); + public byte getByteField(String fname) { + FieldInfo fi = getFieldInfo(fname); + ElementInfo ei = getElementInfo(fi.getClassInfo()); + return ei.fields.getByteValue(fi.getStorageOffset()); + } + + public char getDeclaredCharField(String fname, String refType) { + FieldInfo fi = getDeclaredFieldInfo(refType, fname); + ElementInfo ei = getElementInfo(fi.getClassInfo()); + return ei.fields.getCharValue(fi.getStorageOffset()); + } + + public char getCharField(String fname) { + FieldInfo fi = getFieldInfo(fname); ElementInfo ei = getElementInfo(fi.getClassInfo()); return ei.fields.getCharValue(fi.getStorageOffset()); } - public double getDoubleField(String fname, String refType) { - FieldInfo fi = getFieldInfo(refType, fname); + public double getDeclaredDoubleField(String fname, String refType) { + FieldInfo fi = getDeclaredFieldInfo(refType, fname); ElementInfo ei = getElementInfo(fi.getClassInfo()); return ei.fields.getDoubleValue(fi.getStorageOffset()); } - public float getFloatField(String fname, String refType) { - FieldInfo fi = getFieldInfo(refType, fname); + public double getDoubleField(String fname) { + FieldInfo fi = getFieldInfo(fname); + ElementInfo ei = getElementInfo(fi.getClassInfo()); + return ei.fields.getDoubleValue(fi.getStorageOffset()); + } + + public float getDeclaredFloatField(String fname, String refType) { + FieldInfo fi = getDeclaredFieldInfo(refType, fname); ElementInfo ei = getElementInfo(fi.getClassInfo()); return ei.fields.getFloatValue(fi.getStorageOffset()); } - public short getShortField(String fname, String refType) { - FieldInfo fi = getFieldInfo(refType, fname); + public float getFloatField(String fname) { + FieldInfo fi = getFieldInfo(fname); + ElementInfo ei = getElementInfo(fi.getClassInfo()); + return ei.fields.getFloatValue(fi.getStorageOffset()); + } + + public short getDeclaredShortField(String fname, String refType) { + FieldInfo fi = getDeclaredFieldInfo(refType, fname); + ElementInfo ei = getElementInfo(fi.getClassInfo()); + return ei.fields.getShortValue(fi.getStorageOffset()); + } + + public short getShortField(String fname) { + FieldInfo fi = getFieldInfo(fname); ElementInfo ei = getElementInfo(fi.getClassInfo()); return ei.fields.getShortValue(fi.getStorageOffset()); } @@ -619,8 +666,12 @@ return (index == -1); } - public Reference getObjectField(String fname, String referenceType) { - return area.ks.da.get(getIntField(fname, referenceType)); + public ElementInfo getDeclaredObjectField(String fname, String referenceType) { + return area.ks.da.get(getDeclaredIntField(fname, referenceType)); + } + + public ElementInfo getObjectField(String fname) { + return area.ks.da.get(getIntField(fname)); } // <2do> just here for the Storable interface - it's NOT the one that is @@ -653,8 +704,8 @@ return fields.getHeapSize(); } - public String getStringField(String fname, String referenceType) { - int ref = getIntField(fname, referenceType); + public String getStringField(String fname) { + int ref = getIntField(fname); if (ref != -1) { ElementInfo ei = area.ks.da.get(ref); @@ -684,9 +735,9 @@ throw new JPFException("object is not of type java.lang.String"); } - int value = getIntField("value", "java.lang.String"); - int length = getIntField("count", "java.lang.String"); - int offset = getIntField("offset", "java.lang.String"); + int value = getDeclaredIntField("value", "java.lang.String"); + int length = getDeclaredIntField("count", "java.lang.String"); + int offset = getDeclaredIntField("offset", "java.lang.String"); ElementInfo e = area.get(value); Index: SystemState.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/SystemState.java,v retrieving revision 1.5 retrieving revision 1.6 diff -u -d -r1.5 -r1.6 --- SystemState.java 6 Oct 2005 21:05:53 -0000 1.5 +++ SystemState.java 23 Oct 2005 04:41:01 -0000 1.6 @@ -135,7 +135,7 @@ return boring; } - public Reference getClass (String name) { + public ElementInfo getClass (String name) { if (ks.sa.containsClass(name)) { return ks.sa.get(name); } @@ -159,7 +159,7 @@ return ks.tl.getNonDaemonThreadCount(); } - public Reference getObject (int reference) { + public ElementInfo getObject (int reference) { return ks.da.get(reference); } @@ -184,8 +184,8 @@ return ks.tl.get(index); } - public ThreadInfo getThread (Reference reference) { - return getThread(((ElementInfo) reference).getIndex()); + public ThreadInfo getThread (ElementInfo reference) { + return getThread(reference.getIndex()); } public int getThreadCount () { Index: ThreadInfo.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/ThreadInfo.java,v retrieving revision 1.12 retrieving revision 1.13 diff -u -d -r1.12 -r1.13 --- ThreadInfo.java 7 Oct 2005 21:27:34 -0000 1.12 +++ ThreadInfo.java 23 Oct 2005 04:41:01 -0000 1.13 @@ -466,7 +466,7 @@ return top().getCalleeThis(size); } - public boolean isCalleeThis (Reference r) { + public boolean isCalleeThis (ElementInfo r) { if ((stack.length == 0) || (r == null)) { return false; } @@ -819,19 +819,19 @@ return !getPC().isDeterministic(list.ks.ss, list.ks, this); } - public Reference getObjectLocal (String lname) { + public ElementInfo getObjectLocal (String lname) { return list.ks.da.get(getLocalVariable(lname)); } - public Reference getObjectLocal (int lindex) { + public ElementInfo getObjectLocal (int lindex) { return list.ks.da.get(getLocalVariable(lindex)); } - public Reference getObjectLocal (int fr, String lname) { + public ElementInfo getObjectLocal (int fr, String lname) { return list.ks.da.get(getLocalVariable(fr, lname)); } - public Reference getObjectLocal (int fr, int lindex) { + public ElementInfo getObjectLocal (int fr, int lindex) { return list.ks.da.get(getLocalVariable(fr, lindex)); } @@ -842,7 +842,7 @@ return threadData.objref; } - public Reference getObjectReturnValue () { + public ElementInfo getObjectReturnValue () { return list.ks.da.get(peek()); } @@ -1100,7 +1100,7 @@ return top().getThis(); } - public boolean isThis (Reference r) { + public boolean isThis (ElementInfo r) { if (r == null) { return false; } @@ -1412,7 +1412,7 @@ // for the Throwable (for now, we just explicitly set the details) if (details != null) { msgref = da.newString(details, this); - ei.setReferenceField("detailMessage", "java.lang.Throwable", msgref); + ei.setDeclaredReferenceField("detailMessage", "java.lang.Throwable", msgref); } return throwException(objref); @@ -1876,7 +1876,7 @@ // the stack dump is accessible for the application, so we have to // create it in JPF object land int stRef = getStackTrace(objref); - ei.setReferenceField("stackTrace", "java.lang.Throwable", stRef); + ei.setDeclaredReferenceField("stackTrace", "java.lang.Throwable", stRef); // but we still keep this in JPF itself too, so that it's more accessible // for post-mortem 'debugging', and preserves as much JPF execution Index: State.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/State.java,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -u -d -r1.1.1.1 -r1.2 --- State.java 26 Apr 2005 19:44:05 -0000 1.1.1.1 +++ State.java 23 Oct 2005 04:41:01 -0000 1.2 @@ -23,13 +23,13 @@ * <2do> only used by LTLSearch, so we might scrub it */ public interface State { - Reference getClass (String name); + ElementInfo getClass (String name); - Reference getObject (int reference); + ElementInfo getObject (int reference); ThreadInfo getThread (int index); - ThreadInfo getThread (Reference reference); + ThreadInfo getThread (ElementInfo reference); int getThreadCount (); } \ No newline at end of file Index: DynamicElementInfo.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/DynamicElementInfo.java,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -u -d -r1.1.1.1 -r1.2 --- DynamicElementInfo.java 26 Apr 2005 19:43:59 -0000 1.1.1.1 +++ DynamicElementInfo.java 23 Oct 2005 04:41:01 -0000 1.2 @@ -44,14 +44,22 @@ return getClassInfo().getInstanceField(fieldIndex); } - protected FieldInfo getFieldInfo (String clsBase, String fname) { - FieldInfo fi = getClassInfo().getInstanceField(clsBase, fname); + protected FieldInfo getFieldInfo (String fname) { + FieldInfo fi = getClassInfo().getInstanceField(fname); if (fi == null) { throw new JPFException( "class " + getClassInfo().getName() + " has no field " + fname); } return fi; } + protected FieldInfo getDeclaredFieldInfo (String clsBase, String fname) { + FieldInfo fi = ClassInfo.getClassInfo(clsBase).getDeclaredInstanceField(fname); + if (fi == null) { + throw new JPFException( "class " + clsBase + + " has no field " + fname); + } + return fi; + } protected ElementInfo getElementInfo (ClassInfo ci) { // DynamicElementInfo fields are always flattened, so there is no need to Index: StaticFields.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/StaticFields.java,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -u -d -r1.1.1.1 -r1.2 --- StaticFields.java 26 Apr 2005 19:44:05 -0000 1.1.1.1 +++ StaticFields.java 23 Oct 2005 04:41:01 -0000 1.2 @@ -38,10 +38,6 @@ ci.initializeStaticData(this); } - public FieldInfo getFieldInfo (String clsBase, String fname) { - return ci.getStaticField(clsBase, fname); - } - public String getLogChar () { return "@"; } Index: MJIEnv.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/MJIEnv.java,v retrieving revision 1.5 retrieving revision 1.6 diff -u -d -r1.5 -r1.6 --- MJIEnv.java 20 Oct 2005 11:02:23 -0000 1.5 +++ MJIEnv.java 23 Oct 2005 04:41:01 -0000 1.6 @@ -151,33 +151,35 @@ } public void setIntField (int objref, String fname, int val) { - setIntField(objref, null, fname, val); + ElementInfo ei = da.get(objref); + ei.setIntField(fname, val); } // these two are the workhorses - public void setIntField (int objref, String refType, String fname, int val) { + public void setDeclaredIntField (int objref, String refType, String fname, int val) { ElementInfo ei = da.get(objref); - ei.setIntField(fname, refType, val); + ei.setDeclaredIntField(fname, refType, val); } public int getIntField (int objref, String fname) { - return getIntField(objref, null, fname); + ElementInfo ei = da.get(objref); + return ei.getIntField(fname); } - public int getIntField (int objref, String refType, String fname) { + public int getDeclaredIntField (int objref, String refType, String fname) { ElementInfo ei = da.get(objref); - - return ei.getIntField(fname, refType); + return ei.getDeclaredIntField(fname, refType); } // these two are the workhorses - public void setReferenceField (int objref, String refType, String fname, int val) { + public void setDeclaredReferenceField (int objref, String refType, String fname, int val) { ElementInfo ei = da.get(objref); - ei.setReferenceField(fname, refType, val); + ei.setDeclaredReferenceField(fname, refType, val); } public void setReferenceField (int objref, String fname, int ref) { - setReferenceField(objref, null, fname, ref); + ElementInfo ei = da.get(objref); + ei.setReferenceField(fname, ref); } public int getReferenceField (int objref, String fname) { @@ -228,24 +230,25 @@ } public void setLongField (int objref, String fname, long val) { - setLongField(objref, null, fname, val); - } - - public void setLongField (int objref, String refType, String fname, long val) { ElementInfo ei = da.get(objref); - ei.setLongField(fname, refType, val); + ei.setLongField(fname, val); } - public long getLongField (int objref, String fname) { - return getLongField(objref, null, fname); - } +// public void setLongField (int objref, String refType, String fname, long val) { +// ElementInfo ei = da.get(objref); +// ei.setLongField(fname, refType, val); +// } - public long getLongField (int objref, String refType, String fname) { + public long getLongField (int objref, String fname) { ElementInfo ei = da.get(objref); - - return ei.getLongField(fname, refType); + return ei.getLongField(fname); } +// public long getLongField (int objref, String refType, String fname) { +// ElementInfo ei = da.get(objref); +// return ei.getLongField(fname, refType); +// } + public void setReferenceArrayElement (int objref, int index, int eRef) { da.get(objref).setElement(index, eRef); } Index: JVM.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/JVM.java,v retrieving revision 1.12 retrieving revision 1.13 diff -u -d -r1.12 -r1.13 --- JVM.java 7 Oct 2005 21:27:34 -0000 1.12 +++ JVM.java 23 Oct 2005 04:41:01 -0000 1.13 @@ -563,7 +563,7 @@ return ss.getBoring(); } - public Reference getClassReference (String name) { + public ElementInfo getClassReference (String name) { if (ClassInfo.exists(name)) { return ss.ks.sa.get(name); } @@ -699,11 +699,17 @@ return path.length(); } - public Reference getReference (String name) { + + /** + * Gets reference (element info) for + * @param name - gov.my.class my.var.name + * @return - + */ + public ElementInfo getReference (String name) { // first of all I have to get to a class StringTokenizer st = new StringTokenizer(name, "."); StringBuffer sb = new StringBuffer(); - Reference r = null; + ElementInfo r = null; while (st.hasMoreTokens()) { sb.append(st.nextToken()); @@ -719,9 +725,9 @@ throw new JPFException("invalid argument: " + name); } - // now walk thought the fields + // now walk through the fields while (st.hasMoreTokens()) { - r = r.getObjectField(st.nextToken(), sb.toString()); + r = r.getDeclaredObjectField(st.nextToken(), sb.toString()); } return r; Index: DynamicFields.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/DynamicFields.java,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -u -d -r1.1.1.1 -r1.2 --- DynamicFields.java 26 Apr 2005 19:43:59 -0000 1.1.1.1 +++ DynamicFields.java 23 Oct 2005 04:41:01 -0000 1.2 @@ -41,10 +41,14 @@ // the FieldInfo accessors are just here to hide the Dynamic/StaticFieldInfo // anomaly, remove once we have this solved - public FieldInfo getFieldInfo (String clsBase, String fname) { - return ci.getInstanceField(clsBase, fname); + public FieldInfo getDeclaredFieldInfo (String fname) { + return ci.getDeclaredInstanceField(fname); } - + + public FieldInfo getFieldInfo (String fname) { + return ci.getInstanceField(fname); + } + public int getNumberOfFields() { return ci.getNumberOfInstanceFields(); } Index: StaticElementInfo.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/StaticElementInfo.java,v retrieving revision 1.2 retrieving revision 1.3 diff -u -d -r1.2 -r1.3 --- StaticElementInfo.java 25 Aug 2005 17:19:49 -0000 1.2 +++ StaticElementInfo.java 23 Oct 2005 04:41:01 -0000 1.3 @@ -40,9 +40,21 @@ classObjectRef = classObjRef; } - protected FieldInfo getFieldInfo (String clsBase, String fname) { + + protected FieldInfo getDeclaredFieldInfo (String clsBase, String fname) { + ClassInfo ci = ClassInfo.getClassInfo(clsBase); + FieldInfo fi = ci.getDeclaredStaticField(fname); + + if (fi == null) { + throw new JPFException("class " + ci.getName() + + " has no static field " + fname); + } + return fi; + } + + protected FieldInfo getFieldInfo (String fname) { ClassInfo ci = getClassInfo(); - FieldInfo fi = ci.getStaticField(clsBase, fname); + FieldInfo fi = ci.getStaticField(fname); if (fi == null) { throw new JPFException("class " + ci.getName() + Index: UncaughtException.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/UncaughtException.java,v retrieving revision 1.2 retrieving revision 1.3 diff -u -d -r1.2 -r1.3 --- UncaughtException.java 9 Jun 2005 16:29:23 -0000 1.2 +++ UncaughtException.java 23 Oct 2005 04:41:01 -0000 1.3 @@ -45,7 +45,7 @@ ElementInfo ei = DynamicArea.getHeap().get(xObjRef); xClsName = ei.getClassInfo().getName(); - details = ei.getStringField("detailMessage", null); + details = ei.getStringField("detailMessage"); } public boolean isAssertionError () { Index: ClassInfo.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/ClassInfo.java,v retrieving revision 1.3 retrieving revision 1.4 diff -u -d -r1.3 -r1.4 --- ClassInfo.java 17 Oct 2005 04:05:12 -0000 1.3 +++ ClassInfo.java 23 Oct 2005 04:41:01 -0000 1.4 @@ -400,13 +400,12 @@ /** * Search up the class hierarchy to find a static field - * @param clsBase - name of class to start looking from * @param fName - name of field * @return returns null if field name not found (not declared) */ - public FieldInfo getStaticField (String clsBase, String fName) { + public FieldInfo getStaticField (String fName) { FieldInfo fi; - ClassInfo c = getClassBase(clsBase); + ClassInfo c = this; while (c != null) { fi = c.getDeclaredStaticField(fName); @@ -416,14 +415,6 @@ return null; } - /** - * Search up hierarchy to find static field starting from this class - * @param fname - * @return - */ - public FieldInfo getStaticField (String fname) { - return getStaticField(null, fname); - } /** * FieldInfo lookup in the static fields that are declared in this class @@ -444,9 +435,9 @@ * @param clsBase - the class where we start the lookup (self or some super) * @param fName - the field name */ - public FieldInfo getInstanceField (String clsBase, String fName) { + public FieldInfo getInstanceField (String fName) { FieldInfo fi; - ClassInfo c = getClassBase(clsBase); + ClassInfo c = this; while (c != null) { fi = c.getDeclaredInstanceField(fName); @@ -458,13 +449,6 @@ } /** - * complete bottom-up FieldInfo lookup - */ - public FieldInfo getInstanceField (String fName) { - return getInstanceField(null, fName); - } - - /** * FieldInfo lookup in the fields that are declared in this class */ public FieldInfo getDeclaredInstanceField (String fName) { @@ -869,23 +853,7 @@ int getInstanceDataOffset () { return instanceDataOffset; } - - /** - * Search up class hierarchy for a parent class - * @param clsBase name of class to find - * @return - return current(this) class if clsBase is null. - * - return null if class not found - */ - ClassInfo getClassBase (String clsBase) { - if ((clsBase == null) || (name.equals(clsBase))) return this; - - if (superClass != null) { - return superClass.getClassBase(clsBase); - } - return null; // Eeek - somebody asked for a class that isn't in the base list - } - int computeInstanceDataSize () { int n = getDataSize( iFields); --- Reference.java DELETED --- |
|
From: John P. <joh...@us...> - 2005-10-23 04:41:09
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/search/heuristic In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv30920/src/gov/nasa/jpf/search/heuristic Modified Files: UserHeuristic.java Log Message: * changed getField interface to be getField (searches up class hierarchy from current class) or getDeclared field (looks only in the specified class) no longer uses null parameter to switch between these two cases * got rid of Reference interface because it was going to have to get bigger, but it was tagged for eventual removal replaced uses of Reference with ElementInfo Index: UserHeuristic.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/search/heuristic/UserHeuristic.java,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -u -d -r1.1.1.1 -r1.2 --- UserHeuristic.java 26 Apr 2005 19:44:20 -0000 1.1.1.1 +++ UserHeuristic.java 23 Oct 2005 04:41:01 -0000 1.2 @@ -20,7 +20,7 @@ import gov.nasa.jpf.VM; import gov.nasa.jpf.jvm.JVM; -import gov.nasa.jpf.jvm.Reference; +import gov.nasa.jpf.jvm.ElementInfo; import gov.nasa.jpf.jvm.SystemState; @@ -42,14 +42,15 @@ public int heuristicValue () { // <2do> pcm - BAD, remove the VM nuts-and-bolts dependencies SystemState ss = (SystemState) ((JVM) vm).getSystemState(); - Reference p = ss.getClass("Main"); + ElementInfo p = ss.getClass("Main"); + // this code is ugly because of the Reference interface if (p != null) { - Reference b = p.getObjectField("buffer", null); + ElementInfo b = p.getObjectField("buffer"); if (b != null) { - int current = b.getIntField("current", null); - int capacity = b.getIntField("capacity", null); + int current = b.getIntField("current"); + int capacity = b.getIntField("capacity"); return (capacity - current); } |
|
From: John P. <joh...@us...> - 2005-10-23 04:21:35
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/choice In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv27934/src/gov/nasa/jpf/jvm/choice Modified Files: IntSpec.java Log Message: * added copyright Index: IntSpec.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/choice/IntSpec.java,v retrieving revision 1.1 retrieving revision 1.2 diff -u -d -r1.1 -r1.2 --- IntSpec.java 19 Oct 2005 22:12:41 -0000 1.1 +++ IntSpec.java 23 Oct 2005 04:21:27 -0000 1.2 @@ -1,9 +1,22 @@ -/* - * Created on Oct 19, 2005 - * - * TODO To change the template for this generated file go to - * Window - Preferences - Java - Code Style - Code Templates - */ +// +//Copyright (C) 2005 United States Government as represented by the +//Administrator of the National Aeronautics and Space Administration +//(NASA). All Rights Reserved. +// +//This software is distributed under the NASA Open Source Agreement +//(NOSA), version 1.3. The NOSA has been approved by the Open Source +//Initiative. See the file NOSA-1.3-JPF at the top of the distribution +//directory tree for the complete NOSA document. +// +//THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY +//KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT +//LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO +//SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR +//A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT +//THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT +//DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. +//package gov.nasa.jpf.jvm; +// package gov.nasa.jpf.jvm.choice; import gov.nasa.jpf.JPFException; |
|
From: Peter C. M. <pcm...@em...> - 2005-10-21 23:15:07
|
added to .../doc. While it is a step back in printing, it definitely helps if everybody can edit/add pages, and we care for print quality later. The original commit message was discarded, to save you from a several hundred Kb message. Content has only been slightly changed/ updated so far -- Peter |
Update of /cvsroot/javapathfinder/javapathfinder/doc/JPF_files In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv18432/JPF_files Added Files: DFSListener.png GenPeer.png GenPeerDispatcher.png JPF-mod.css RIACS.png arc.png banner_title.png choicegen-example.png dir-tree.png interleavings.png jpf-abstractions.png jpf-config.png jpf-intro.png jpf-layers.png jpf-listener.png meatball.png mji-call.png mji-functions.png mji-mangling.png por-mark.png por-scheduling-relevance.png spiral-of-death.png Log Message: cleaned up the html docu (which was extracted from a Pages markup), and added all the pages to CVS. Graphics are only stored as PNGs, so that's the last thing missing before everything is CVS-safe (but the sources are *.graffle files which require a Mac & OmniGraffle, so I don't know what it would be good for). Anyways, everybody can now edit and add documentation, so please do! --- NEW FILE: GenPeer.png --- (This appears to be a binary file; contents omitted.) --- NEW FILE: jpf-layers.png --- (This appears to be a binary file; contents omitted.) --- NEW FILE: jpf-abstractions.png --- (This appears to be a binary file; contents omitted.) --- NEW FILE: RIACS.png --- (This appears to be a binary file; contents omitted.) --- NEW FILE: meatball.png --- (This appears to be a binary file; contents omitted.) --- NEW FILE: dir-tree.png --- (This appears to be a binary file; contents omitted.) --- NEW FILE: mji-call.png --- (This appears to be a binary file; contents omitted.) --- NEW FILE: jpf-config.png --- (This appears to be a binary file; contents omitted.) --- NEW FILE: DFSListener.png --- (This appears to be a binary file; contents omitted.) --- NEW FILE: jpf-listener.png --- (This appears to be a binary file; contents omitted.) --- NEW FILE: JPF-mod.css --- .code { background: #e3e3e3; color: #0000ff; font-family: 'Courier', 'Courier'; font-size: 9.00pt; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: 0; line-height: 1.22; margin-bottom: 10.0pt; margin-left: 8.0pt; margin-right: 8.0pt; margin-top: 0.0pt; padding-bottom: 4.0pt; padding-top: 4.0pt; padding-left: 8.0pt; padding-right: 8pt; text-align: left; text-decoration: none; text-indent: 0.00pt; text-transform: none; vertical-align: 0.000000em; white-space: pre; } .news { color: #0000ff; border: 1px solid #0000ff; background: #aaaaff; background-color: #ddddff; } .NavList_Body { color: #000000; font-family: arial, sans-serif; font-size: 9.00pt; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: 0; line-height: 1.22; margin-bottom: 0.000000pt; margin-left: 0.00pt; margin-right: 0.00pt; margin-top: 0.000000pt; padding-bottom: 2.000000pt; padding-top: 0.000000pt; text-align: left; text-decoration: none; text-indent: 0.00pt; text-transform: none; vertical-align: 0.000000em; } h1 { color: #000000; font-family: 'TimesNewRomanPS-BoldMT', 'Times New Roman'; font-size: 16.00pt; font-style: normal; font-variant: normal; font-weight: bold; letter-spacing: 0; line-height: 1.17; margin-bottom: 0.000000pt; margin-left: 3pt; margin-right: 3.00pt; margin-top: 0.000000pt; padding-bottom: 4.000000pt; padding-top: 12.000000pt; text-align: left; text-decoration: none; text-indent: 0.00pt; text-transform: none; vertical-align: 0.000000em; } h2 { color: #000000; font-family: 'TimesNewRomanPS-BoldMT', 'Times New Roman'; font-size: 13.00pt; font-style: normal; font-variant: normal; font-weight: bold; letter-spacing: 0; line-height: 1.23; margin-bottom: 0.000000pt; margin-left: 3.00pt; margin-right: 3.00pt; margin-top: 0.000000pt; padding-bottom: 2.000000pt; padding-top: 8.000000pt; text-align: left; text-decoration: none; text-indent: 0.00pt; text-transform: none; vertical-align: 0.000000em; } body { color: #000000; font-family: 'TimesNewRomanPSMT', 'Times New Roman'; font-size: 11.00pt; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: 0; line-height: 1.09; margin-bottom: 3.00pt; margin-left: 3.00pt; margin-right: 3.00pt; margin-top: 3.00pt; padding-bottom: 0.000000pt; padding-top: 0.000000pt; text-align: left; text-decoration: none; text-indent: 0.00pt; text-transform: none; vertical-align: 0.000000em; } .comment { color: #a00000; font-family: 'TimesNewRomanPSMT', 'Times New Roman'; font-size: 10.00pt; font-style: oblique; } .big_diagram { color: #000000; font-family: 'TimesNewRomanPSMT', 'Times New Roman'; font-size: 11.00pt; font-style: italic; font-variant: normal; font-weight: normal; letter-spacing: 0; line-height: 1.09; margin-bottom: 0.000000pt; margin-left: 0.00pt; margin-right: 0.00pt; margin-top: 0.000000pt; padding-bottom: 12.000000pt; padding-top: 0.000000pt; text-align: center; text-decoration: none; text-indent: 0.00pt; text-transform: none; vertical-align: 0.000000em; } ul { list-style: disc; list-style-position: outside; margin-top: 0.000000pt; margin-bottom: 12.000000pt; margin-left: 30.0pt; margin-right: 3.00pt; margin-top: 0.000000pt; padding: 0pt; text-align: left; text-decoration: none; text-indent: 0.00pt; text-transform: none; } li { margin-top: 4pt; margin-bottom: 4pt; } ol { list-style: decimal; list-style-position: outside; margin-bottom: 0.000000pt; margin-left: 30.000000pt; margin-right: 3pt; margin-top: 0.000000pt; padding-left: 0pt; text-indent: 0.000000pt; } .NavList { list-style: disc; font-family: arial, sans-serif; font-size: 9.00pt; margin-bottom: 0.000000pt; margin-left: 5.000000pt; margin-top: 0.000000pt; padding-left: 8pt; text-indent: 0.000000pt; text-decoration: none; } .NavList a:link { text-decoration: none; } .NavList a:hover { color: #ff0000; text-decoration: underline; } .NavTop { font-family: arial, sans-serif; font-size: 10.00pt; font-weight: normal; background: #f5f5f5; color: #0000ff; border-top: 1px solid #a0a0ff; border-bottom: 1px solid #a0a0ff; border-left: 1px solid #a0a0ff; border-right: 1px solid #a0a0ff; } .NavTop a:link { text-decoration: none; } .NavTop a:hover { color: #ff0000; text-decoration: underline; } --- NEW FILE: mji-functions.png --- (This appears to be a binary file; contents omitted.) --- NEW FILE: por-scheduling-relevance.png --- (This appears to be a binary file; contents omitted.) --- NEW FILE: arc.png --- (This appears to be a binary file; contents omitted.) --- NEW FILE: jpf-intro.png --- (This appears to be a binary file; contents omitted.) --- NEW FILE: por-mark.png --- (This appears to be a binary file; contents omitted.) --- NEW FILE: GenPeerDispatcher.png --- (This appears to be a binary file; contents omitted.) --- NEW FILE: spiral-of-death.png --- (This appears to be a binary file; contents omitted.) --- NEW FILE: choicegen-example.png --- (This appears to be a binary file; contents omitted.) --- NEW FILE: mji-mangling.png --- (This appears to be a binary file; contents omitted.) --- NEW FILE: banner_title.png --- (This appears to be a binary file; contents omitted.) --- NEW FILE: interleavings.png --- (This appears to be a binary file; contents omitted.) |
|
From: pcm <pcm...@us...> - 2005-10-21 22:42:21
|
Update of /cvsroot/javapathfinder/javapathfinder/doc/JPF_files In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv15280/JPF_files Log Message: Directory /cvsroot/javapathfinder/javapathfinder/doc/JPF_files added to the repository |
|
From: John P. <joh...@us...> - 2005-10-20 11:02:32
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv31086/src/gov/nasa/jpf/jvm Modified Files: MJIEnv.java Log Message: * use existing methods that insert null rather than passing null Index: MJIEnv.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/MJIEnv.java,v retrieving revision 1.4 retrieving revision 1.5 diff -u -d -r1.4 -r1.5 --- MJIEnv.java 20 Oct 2005 10:50:17 -0000 1.4 +++ MJIEnv.java 20 Oct 2005 11:02:23 -0000 1.5 @@ -91,7 +91,7 @@ // the instance field setters public void setBooleanField (int objref, String fname, boolean val) { - setIntField(objref, null, fname, Types.booleanToInt(val)); + setIntField(objref, fname, Types.booleanToInt(val)); } public boolean getBooleanField (int objref, String fname) { @@ -99,7 +99,7 @@ } public void setByteField (int objref, String fname, byte val) { - setIntField(objref, null, fname, (int) val); + setIntField(objref, fname, (int) val); } public byte getByteField (int objref, String fname) { @@ -107,7 +107,7 @@ } public void setCharField (int objref, String fname, char val) { - setIntField(objref, null, fname, (int) val); + setIntField(objref, fname, (int) val); } public char getCharField (int objref, String fname) { @@ -115,7 +115,7 @@ } public void setDoubleField (int objref, String fname, double val) { - setLongField(objref, null, fname, Types.doubleToLong(val)); + setLongField(objref, fname, Types.doubleToLong(val)); } public double getDoubleField (int objref, String fname) { @@ -123,7 +123,7 @@ } public void setFloatField (int objref, String fname, float val) { - setIntField(objref, null, fname, Types.floatToInt(val)); + setIntField(objref, fname, Types.floatToInt(val)); } public float getFloatField (int objref, String fname) { @@ -255,7 +255,7 @@ } public void setShortField (int objref, String fname, short val) { - setIntField(objref, null, fname, (int) val); + setIntField(objref, fname, (int) val); } public short getShortField (int objref, String fname) { @@ -315,7 +315,7 @@ public void setStaticIntField (String clsName, String fname, int value) { ClassInfo ci = ClassInfo.getClassInfo(clsName); - sa.get(ci.getName()).setIntField(fname, null, value); + sa.get(ci.getName()).setIntField(fname, value); } public void setStaticIntField (int clsObjRef, String fname, int val) { |
|
From: John P. <joh...@us...> - 2005-10-20 10:50:26
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv28131/src/gov/nasa/jpf/jvm Modified Files: MJIEnv.java Log Message: * use existing method that inserts null rather than passing null Index: MJIEnv.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/MJIEnv.java,v retrieving revision 1.3 retrieving revision 1.4 diff -u -d -r1.3 -r1.4 --- MJIEnv.java 19 Oct 2005 11:25:02 -0000 1.3 +++ MJIEnv.java 20 Oct 2005 10:50:17 -0000 1.4 @@ -95,7 +95,7 @@ } public boolean getBooleanField (int objref, String fname) { - return Types.intToBoolean(getIntField(objref, null, fname)); + return Types.intToBoolean(getIntField(objref, fname)); } public void setByteField (int objref, String fname, byte val) { @@ -103,7 +103,7 @@ } public byte getByteField (int objref, String fname) { - return (byte) getIntField(objref, null, fname); + return (byte) getIntField(objref, fname); } public void setCharField (int objref, String fname, char val) { @@ -111,7 +111,7 @@ } public char getCharField (int objref, String fname) { - return (char) getIntField(objref, null, fname); + return (char) getIntField(objref, fname); } public void setDoubleField (int objref, String fname, double val) { @@ -119,7 +119,7 @@ } public double getDoubleField (int objref, String fname) { - return Types.longToDouble(getLongField(objref, null, fname)); + return Types.longToDouble(getLongField(objref, fname)); } public void setFloatField (int objref, String fname, float val) { @@ -127,7 +127,7 @@ } public float getFloatField (int objref, String fname) { - return Types.intToFloat(getIntField(objref, null, fname)); + return Types.intToFloat(getIntField(objref, fname)); } public void setByteArrayElement (int objref, int index, byte value) { @@ -181,7 +181,7 @@ } public int getReferenceField (int objref, String fname) { - return getIntField(objref, null, fname); + return getIntField(objref, fname); } @@ -259,7 +259,7 @@ } public short getShortField (int objref, String fname) { - return (short) getIntField(objref, null, fname); + return (short) getIntField(objref, fname); } public String getTypeName (int objref) { |
|
From: John P. <joh...@us...> - 2005-10-19 11:25:19
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv11962/src/gov/nasa/jpf/jvm Modified Files: MJIEnv.java Log Message: * use alternate ElementInfo method rather than pass null Index: MJIEnv.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/MJIEnv.java,v retrieving revision 1.2 retrieving revision 1.3 diff -u -d -r1.2 -r1.3 --- MJIEnv.java 30 Apr 2005 06:44:38 -0000 1.2 +++ MJIEnv.java 19 Oct 2005 11:25:02 -0000 1.3 @@ -331,7 +331,7 @@ ClassInfo ci = ClassInfo.getClassInfo(clsName); StaticElementInfo ei = sa.get(ci.getName()); - return ei.getIntField(fname, null); + return ei.getIntField(fname); } public void setStaticLongField (String clsName, String fname, long value) { @@ -343,7 +343,7 @@ ClassInfo ci = ClassInfo.getClassInfo(clsName); StaticElementInfo ei = sa.get(ci.getName()); - return ei.getLongField(fname, null); + return ei.getLongField(fname); } public void setStaticReferenceField (String clsName, String fname, int objref) { @@ -575,7 +575,7 @@ ElementInfo getClassElementInfo (int clsObjRef) { ElementInfo ei = da.get(clsObjRef); - int cref = ei.getIntField("cref", null); + int cref = ei.getIntField("cref"); ElementInfo cei = sa.get(cref); |
|
From: John P. <joh...@us...> - 2005-10-18 11:44:59
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv14730/src/gov/nasa/jpf/jvm Modified Files: Fields.java Log Message: * remove unused method Index: Fields.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/jvm/Fields.java,v retrieving revision 1.3 retrieving revision 1.4 diff -u -d -r1.3 -r1.4 --- Fields.java 29 Jul 2005 21:09:43 -0000 1.3 +++ Fields.java 18 Oct 2005 11:44:42 -0000 1.4 @@ -83,9 +83,6 @@ return ci; } - // <2do> pcm - Grr, this is only here to hide the Dynamic/StaticFieldInfo branching - // remove once this is gone! - public abstract FieldInfo getFieldInfo (String clsBase, String fname); public abstract int getNumberOfFields (); // NOTE - fieldIndex (ClassInfo) != storageOffset (Fields). We *don't pad anymore! public abstract FieldInfo getFieldInfo (int fieldIndex); |
|
From: John P. <joh...@us...> - 2005-10-17 11:23:05
|
Update of /cvsroot/javapathfinder/javapathfinder/test/gov/nasa/jpf/jvm In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv10177/test/gov/nasa/jpf/jvm Modified Files: TestMethod.java Log Message: * added comment that static call via object is intentional Index: TestMethod.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/test/gov/nasa/jpf/jvm/TestMethod.java,v retrieving revision 1.1.1.1 retrieving revision 1.2 diff -u -d -r1.1.1.1 -r1.2 --- TestMethod.java 26 Apr 2005 19:44:25 -0000 1.1.1.1 +++ TestMethod.java 17 Oct 2005 11:22:56 -0000 1.2 @@ -196,7 +196,7 @@ assert TestMethodBase.sData == 24; TestMethod o = new TestMethod(); - o.taz(); + o.taz(); // intentional static access via object assert TestMethodBase.sData == 9; } |
![http://g-images.amazon.com/images/G/04/icons/amazon-logo.gif"](http://g-images.amazon.com/images/G/04/icons/amazon-logo.gif"){kind=link}