Menu
▾
▴
javapathfinder-devel
|
From: <pcm...@us...> - 2007-09-07 20:07:51
|
Revision: 553
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=553&view=rev
Author: pcmehlitz
Date: 2007-09-07 13:07:49 -0700 (Fri, 07 Sep 2007)
Log Message:
-----------
* added a pre-invoke goal check, for goals that need to capture before/after states (incl target object)
* turned Goal into an abstract, since it's getting more and more public methods
* added a generic backdoor for new Goals w/o the need to modify the parser. The "satisfies" clause
now takes an id and an optional arglist, which are instantiated via the TestContext, which now really
becomes a factory for all sort of test things
* with that, implemented a simple MemoryGoal. It kind of works standalone, but since normal VMs
don't keep track of heap memory on a per object basis, the granularity is probably not enough. Makes
a good example of how to use JPF to be more precise
* added a generic "createObject" to Misc, to factorize the common case of looking up ctors, and
instantiating objects with various argument lists
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/test/CompareGoal.java
trunk/src/gov/nasa/jpf/test/Goal.java
trunk/src/gov/nasa/jpf/test/NoThrowsGoal.java
trunk/src/gov/nasa/jpf/test/RegexGoal.java
trunk/src/gov/nasa/jpf/test/TestContext.java
trunk/src/gov/nasa/jpf/test/TestSpec.g
trunk/src/gov/nasa/jpf/test/TestSpecLexer.java
trunk/src/gov/nasa/jpf/test/TestSpecParser.java
trunk/src/gov/nasa/jpf/test/ThrowsGoal.java
trunk/src/gov/nasa/jpf/test/WithinGoal.java
trunk/src/gov/nasa/jpf/tools/MethodTester.java
trunk/src/gov/nasa/jpf/util/Misc.java
trunk/test/gov/nasa/jpf/test/TestMethodTest.java
Added Paths:
-----------
trunk/src/gov/nasa/jpf/test/MemoryGoal.java
trunk/src/gov/nasa/jpf/test/TestException.java
Removed Paths:
-------------
trunk/src/gov/nasa/jpf/test/ObjectException.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-09-10 15:11:13
|
Revision: 559
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=559&view=rev
Author: pcmehlitz
Date: 2007-09-10 08:11:10 -0700 (Mon, 10 Sep 2007)
Log Message:
-----------
* weird - the multi-goal extension seem to not have made it into the last commit. Here it
is again: multiple goals per TestSpec, all checked in different executions
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/tools/MethodTester.java
trunk/test/gov/nasa/jpf/test/TestMethodTest.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-09-11 21:40:25
|
Revision: 560
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=560&view=rev
Author: pcmehlitz
Date: 2007-09-11 14:40:23 -0700 (Tue, 11 Sep 2007)
Log Message:
-----------
the grand scheme is to make the MethodTester run under JPF. For that we need a lot more reflection..
* added synthetic, on-the-fly creation of Annotation proxy classes, turning annotation entries into
field/accessor pairs. Some functionality resides in an actificial AnnotationProxyBase, so that we don't
have to generate too much code. And since it's not subject to verification, the code is actually
in a NativePeer
* added initialize(..) methods for ALOAD,GETFIELD so that we can instantiate them in synthetic methods
* added missing Array.get()
* added missing Class.getAnnotation() (Method/Field.getAnnotation() still missing, but the same)
* added MethodTester and MemoryGoal NativePeers, to facilitate execution under JPF. native peers are
the preferred way to add JPF specific behavior
* added a DynamicArea.getHeapSize() for statistical purposes
Modified Paths:
--------------
trunk/env/jpf/java/lang/Class.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Array.java
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/DynamicArea.java
trunk/src/gov/nasa/jpf/jvm/FieldInfo.java
trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
trunk/src/gov/nasa/jpf/jvm/bytecode/ALOAD.java
trunk/src/gov/nasa/jpf/jvm/bytecode/GETFIELD.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IRETURN.java
trunk/src/gov/nasa/jpf/test/Goal.java
trunk/src/gov/nasa/jpf/tools/MethodTester.java
Added Paths:
-----------
trunk/env/jpf/gov/nasa/jpf/AnnotationProxyBase.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_AnnotationProxyBase.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_test_MemoryGoal.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_tools_MethodTester.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-09-11 23:35:27
|
Revision: 561
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=561&view=rev
Author: pcmehlitz
Date: 2007-09-11 16:35:26 -0700 (Tue, 11 Sep 2007)
Log Message:
-----------
* the missing Field/Method.getAnnotation()
* ..and the Class/Field/Method.getAnnotations() - it's not really correct yet, since we have to
distinguish between declared and inherited annotations for classes, but that should be rather
exotic
what's still missing for annotation modeling are enums
Modified Paths:
--------------
trunk/env/jpf/java/lang/reflect/Field.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_AnnotationProxyBase.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Field.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Method.java
trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-09-12 19:09:24
|
Revision: 562
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=562&view=rev
Author: pcmehlitz
Date: 2007-09-12 12:09:22 -0700 (Wed, 12 Sep 2007)
Log Message:
-----------
* better support for Enums - added a ClassInfo.isEnum to easily identify enum const objects
* <sigh> had to add a "longjmp" exception (gov.nasa.jpf.jvm.ClinitRequired) to handle clinit
requests from deep inside of the stack, where we can't simply use a return value or even know
what the executed insn was that caused the request. This is for instance required if we reference
class fields & arrays of Annotation proxy objects (how obvious!). It's used in the
getAnnotation()/getAnnotations() methods
Not so nice.
Also refactored some of the repeatInvocation() handling into MJIEnv, since it's most likely
going to be used from native peer methods (the bytecodes are mostly simple)
* and with all this, implemented Enum and Class and Class[] Annotation elements, both on the JPF
(AnnotationInfo) and the modeling side. AnnotationInfo stores class elements as ClassInfo references,
and Enums as FieldInfo references (not sure if there could be other field refs in Annotations, but
assume not). This was quite a tour de force
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_AnnotationProxyBase.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
trunk/src/gov/nasa/jpf/jvm/AnnotationInfo.java
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
Added Paths:
-----------
trunk/src/gov/nasa/jpf/jvm/ClinitRequired.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-09-14 02:19:40
|
Revision: 564
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=564&view=rev
Author: pcmehlitz
Date: 2007-09-13 19:19:39 -0700 (Thu, 13 Sep 2007)
Log Message:
-----------
a rather large set of reflection related fixes to make MethodTester run under JPF
among the more serious ones:
* Class.forName() didn't throw a ClassNotfoundException!! ..and nobody noticed this?
* of course we should only unbox box types in Method.invoke() if the argument type
is not a box type reference
* some missing methods in Contructor/Method
* the AnnotationProxy methods have to get the right operand and local slots
now it runs, including the Antlr parser. But the MemoryGoal needs a listener implementation
to not count the MethodTester itself
Modified Paths:
--------------
trunk/env/jpf/java/lang/reflect/Constructor.java
trunk/env/jpf/java/lang/reflect/Field.java
trunk/env/jpf/java/lang/reflect/Method.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_test_MemoryGoal.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Class.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_Math.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Constructor.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Field.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Method.java
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
trunk/src/gov/nasa/jpf/test/MemoryGoal.java
trunk/src/gov/nasa/jpf/test/TestContext.java
trunk/src/gov/nasa/jpf/tools/MethodTester.java
trunk/test/gov/nasa/jpf/test/TestMethodTest.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-09-17 18:51:43
|
Revision: 569
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=569&view=rev
Author: pcmehlitz
Date: 2007-09-17 11:51:35 -0700 (Mon, 17 Sep 2007)
Log Message:
-----------
* slightly extended the MJIEnv interface, adding add/removeListener() and getMethodInfo(ref)
* there was no JPF.removeListener - strange
* with that, implemented the precise ...test.MemoryGoal native peer as a listener. Well, almost precise,
because object heap size is of course VM specific. But the point is that we can keep track of
allocation/deallocation on a per-object basis. This should be good enough for an initial example
of how (and why) to do JPF specific goal implementations
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_test_MemoryGoal.java
trunk/src/gov/nasa/jpf/JPF.java
trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
trunk/test/gov/nasa/jpf/test/TestMethodTest.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-09-18 00:56:08
|
Revision: 571
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=571&view=rev
Author: pcmehlitz
Date: 2007-09-17 17:56:04 -0700 (Mon, 17 Sep 2007)
Log Message:
-----------
* fixed pretty bad and subtle bug with Method/Contructor.getParameterTypes(), which is supposed to return
an array of class objects. However, if the classes are not initilialized yet, we have nulls in there.
So it needs a ClinitRequired exception from env.getParameterTypes(). But that just unveiled another bug
in env.handleClinitRequired() - no matter if we pushed clinit frames, we have to do a repeatInvocation() because
this is called from a handler context, and if we only had to create the class objects and hence go on,
we are in a gloriously inconsistent program state
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Constructor.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Method.java
trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-09-21 21:17:49
|
Revision: 573
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=573&view=rev
Author: pcmehlitz
Date: 2007-09-21 14:17:48 -0700 (Fri, 21 Sep 2007)
Log Message:
-----------
* apparently forgot to update the MemoryGoal, JPF version
* core support for getting field/local values by name, and turning them
into Objects (required for the upcoming contracts). Required some refactoring
to get object sizes via polymorphism (pushed down into the FieldInfos)
* MJIEnv had a dependency on JPF_java_lang_reflect_Method, which is
of course illegal
* build.xml wasn't aware of the 'app' dir, which unfurtunately contains things
(Annotations) that are used by the core (the 'gov.nasa.jpf.test' stuff). But since
'app' is not allowed to use JPF specifics, I guess it's Ok to make the core
depend on it. Again, the purpose of 'app' is to use it for classes/interfaces/annotations
that can also be used by applications w/o JPF
Modified Paths:
--------------
trunk/build.xml
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_test_MemoryGoal.java
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/jvm/DoubleFieldInfo.java
trunk/src/gov/nasa/jpf/jvm/DynamicElementInfo.java
trunk/src/gov/nasa/jpf/jvm/ElementInfo.java
trunk/src/gov/nasa/jpf/jvm/FieldInfo.java
trunk/src/gov/nasa/jpf/jvm/FloatFieldInfo.java
trunk/src/gov/nasa/jpf/jvm/IntegerFieldInfo.java
trunk/src/gov/nasa/jpf/jvm/LongFieldInfo.java
trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
trunk/src/gov/nasa/jpf/jvm/ReferenceFieldInfo.java
trunk/src/gov/nasa/jpf/jvm/Types.java
trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKESPECIAL.java
trunk/src/gov/nasa/jpf/jvm/bytecode/INVOKESTATIC.java
trunk/src/gov/nasa/jpf/jvm/bytecode/InvokeInstruction.java
trunk/src/gov/nasa/jpf/jvm/bytecode/VirtualInvocation.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-09-25 00:31:49
|
Revision: 577
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=577&view=rev
Author: pcmehlitz
Date: 2007-09-24 17:31:45 -0700 (Mon, 24 Sep 2007)
Log Message:
-----------
* implementation for a simple contract grammar, including semantic actions to
construct a Contract object out of the specs
* the ContractVerifier is still a stub
Added Paths:
-----------
trunk/app/gov/nasa/jpf/Requires.java
trunk/src/gov/nasa/jpf/test/Contract.java
trunk/src/gov/nasa/jpf/test/ContractAnd.java
trunk/src/gov/nasa/jpf/test/ContractException.java
trunk/src/gov/nasa/jpf/test/ContractOr.java
trunk/src/gov/nasa/jpf/test/ContractSpec.g
trunk/src/gov/nasa/jpf/test/ContractSpecLexer.java
trunk/src/gov/nasa/jpf/test/ContractSpecParser.java
trunk/src/gov/nasa/jpf/test/SimpleContract.java
trunk/src/gov/nasa/jpf/tools/ContractVerifier.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-09-25 03:27:39
|
Revision: 578
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=578&view=rev
Author: pcmehlitz
Date: 2007-09-24 20:27:38 -0700 (Mon, 24 Sep 2007)
Log Message:
-----------
* some more work on the ContractVerifier, which now parses and stores preconditions
* super contract handling. comes quite easy
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
trunk/src/gov/nasa/jpf/test/Contract.java
trunk/src/gov/nasa/jpf/tools/ContractVerifier.java
Added Paths:
-----------
trunk/src/gov/nasa/jpf/test/EmptyContract.java
trunk/test/gov/nasa/jpf/test/TestContracts.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-09-25 05:52:11
|
Revision: 579
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=579&view=rev
Author: pcmehlitz
Date: 2007-09-24 22:52:10 -0700 (Mon, 24 Sep 2007)
Log Message:
-----------
* couldn't help it - first stab at precond evaluation. Works, but has to be more
efficient, which also involves changing the syntax a bit to allow things like
"a within 0,42". The 'operand' rule needs to be widened, but that's why we
employ ANTLR
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
trunk/src/gov/nasa/jpf/jvm/bytecode/Instruction.java
trunk/src/gov/nasa/jpf/test/Contract.java
trunk/src/gov/nasa/jpf/test/ContractAnd.java
trunk/src/gov/nasa/jpf/test/ContractOr.java
trunk/src/gov/nasa/jpf/test/EmptyContract.java
trunk/src/gov/nasa/jpf/test/SimpleContract.java
trunk/src/gov/nasa/jpf/tools/ContractVerifier.java
trunk/test/gov/nasa/jpf/test/TestContracts.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-09-25 22:07:11
|
Revision: 580
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=580&view=rev
Author: pcmehlitz
Date: 2007-09-25 15:07:07 -0700 (Tue, 25 Sep 2007)
Log Message:
-----------
* missed a bunch of box class constructors in MJIEnv
* likewise, primitive type field accessors in ElementInfo
* String.matches(regex) wasn't native? where did it go??
* fixed the Field.get(o) to do autoboxing and handle static fields
the FieldInfo tree needs to be extended to avoid these silly type.equals(..) checks. Not very OOPish
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_String.java
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_reflect_Field.java
trunk/src/gov/nasa/jpf/jvm/ElementInfo.java
trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
trunk/test/gov/nasa/jpf/test/TestMethodTest.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-09-26 19:16:17
|
Revision: 581
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=581&view=rev
Author: pcmehlitz
Date: 2007-09-26 12:16:13 -0700 (Wed, 26 Sep 2007)
Log Message:
-----------
* hoisted SimpleContract.Operator and .Operand to toplevel - those are just getting bigger
* extended the grammar for operator/operand pairs to include more choices (like "within" and the generic
"satisfies"), though most of them don't have their eval implemented yet
* extended the functor to have any number of 'Operand' arguments
* added a cache for Operand.VarRef so that we don't have to lookup and create objects for
each occurrence in an expression. Actually, we might even need indentity at some point, so it's not just
an optimization
* changed the precond evaluation to executeInstruction(), since we actually want to eval this
in the callers context (but need to check for performance)
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/test/Contract.java
trunk/src/gov/nasa/jpf/test/ContractSpec.g
trunk/src/gov/nasa/jpf/test/ContractSpecLexer.java
trunk/src/gov/nasa/jpf/test/ContractSpecParser.java
trunk/src/gov/nasa/jpf/test/SimpleContract.java
trunk/src/gov/nasa/jpf/tools/ContractVerifier.java
trunk/test/gov/nasa/jpf/test/TestContracts.java
trunk/test/gov/nasa/jpf/test/TestMethodTest.java
Added Paths:
-----------
trunk/src/gov/nasa/jpf/test/Operand.java
trunk/src/gov/nasa/jpf/test/Operator.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-09-28 17:39:37
|
Revision: 585
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=585&view=rev
Author: pcmehlitz
Date: 2007-09-28 10:39:35 -0700 (Fri, 28 Sep 2007)
Log Message:
-----------
* added some Verify.print() methods so that System.out clinits can be avoided if an
application really has to. Of course, you still have to use println(String...s) instead of
String concatenation, to avoid the StringBuilder
* added some Verify.get/setFieldAttribute() methods, but those are mostly for debugging
attribute propagation w/o writing listeners. Only supports int attributes, since what would
it be good for trying to access native JPF objects from your application?
still need to do the corresponding array element attrs
* wrote a reg test case that shows how to use it
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_Verify.java
trunk/src/gov/nasa/jpf/jvm/Verify.java
trunk/test/gov/nasa/jpf/jvm/TestAttrs.java
trunk/test/gov/nasa/jpf/jvm/TestAttrsJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-09-28 23:08:50
|
Revision: 586
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=586&view=rev
Author: pcmehlitz
Date: 2007-09-28 16:08:23 -0700 (Fri, 28 Sep 2007)
Log Message:
-----------
* added the array element attributes, which was mostly a little refactoring in
Fields/ArrayFields, plus the interface in ElementInfo
* added MJIEnv interfaces
* added all the stuff that potentially access elment attributes (System.arraycopy,
ArrayStore/LoadInstruction)
* fixed a bug with long GET/PUTFIELD ArrayLoad/StoreInstruction values, which of
course have to undergo the dreaded "attribute on first word" checks
* added test cases for it (using the Verify interface)
hopefully that is it
Modified Paths:
--------------
trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_lang_System.java
trunk/src/gov/nasa/jpf/jvm/ArrayFields.java
trunk/src/gov/nasa/jpf/jvm/ElementInfo.java
trunk/src/gov/nasa/jpf/jvm/Fields.java
trunk/src/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_Verify.java
trunk/src/gov/nasa/jpf/jvm/MJIEnv.java
trunk/src/gov/nasa/jpf/jvm/StackFrame.java
trunk/src/gov/nasa/jpf/jvm/bytecode/ArrayLoadInstruction.java
trunk/src/gov/nasa/jpf/jvm/bytecode/ArrayStoreInstruction.java
trunk/src/gov/nasa/jpf/jvm/bytecode/GETFIELD.java
trunk/src/gov/nasa/jpf/jvm/bytecode/PUTFIELD.java
trunk/test/gov/nasa/jpf/jvm/TestAttrs.java
trunk/test/gov/nasa/jpf/jvm/TestAttrsJPF.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <ubn...@us...> - 2007-10-12 22:36:07
|
Revision: 607
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=607&view=rev
Author: ubnepvpb
Date: 2007-10-12 15:36:05 -0700 (Fri, 12 Oct 2007)
Log Message:
-----------
Doubles & Symbolic Execution:
- Add most of the double byte codes
- Fix INVOKExxx to work with doubles
- Add some test cases
- Add some JPF VMListeners to help with debugging
Modified Paths:
--------------
trunk/.classpath
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/SymbolicInstructionFactory.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/FCMPL.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/INVOKESPECIAL.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/INVOKESTATIC.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/INVOKEVIRTUAL.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/PC3WayChoiceGenerator.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/PCChoiceGenerator.java
Added Paths:
-----------
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/DADD.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/DCMPL.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/DDIV.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/DMUL.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/DNEG.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/DREM.java
trunk/extensions/symbc/src/gov/nasa/jpf/symbc/bytecode/DSUB.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/Debug.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/JPF_gov_nasa_jpf_symbc_Debug.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/LineNumberListener.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/PathConditionListener.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/TestDouble1.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/TestDoubleSpecial1.java
trunk/extensions/symbc/test/gov/nasa/jpf/symbc/TestDoubleVirtual1.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-10-18 20:43:50
|
Revision: 634
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=634&view=rev
Author: pcmehlitz
Date: 2007-10-18 13:43:48 -0700 (Thu, 18 Oct 2007)
Log Message:
-----------
* added optional event receiver constraints. For scripts, this is specified as
[<receiver-pattern> {'|' <receiver-pattern> } ':'] <event-name> ['(' <args> ')']
where receiver pattern is using or StringSetMatcher notation, NOT general regexes, which means the only
meta char is the wildcard '*' (like a Unix wildcard char).
Explicitly sent events don't need receiver constraints, because they get them automatically. If we send an event to
an explicitly specified state, this implies it's only processed by itself or its children. Sounds sound, but the
implementation hurts (we pull it out of the PendingEvents queue of the receiver, just to encode the receiver again
in the SCEvent id). Nothing is perfect. At least, the receiver filter is consistent (all in NativeStateMachine and
SCEvent)
The SimStateMachine still needs to be updated accordingly
* added a little ReceiverConstraints example for this
* added a multiple-instances filter to NativeStateMachine.createCGFromPendingEvents(), since the hierarchical
lookup can lead to multiple inclusions of the same event, which just makes life harder for the model checker
Modified Paths:
--------------
trunk/examples/jpfESAS/launch/CEV-ascent-guards.launch
trunk/examples/jpfESAS/launch/CEV-safehold.launch
trunk/examples/jpfESAS/launch/CEV-scriptless-bt.launch
trunk/examples/jpfESAS/launch/CEV-scriptless-constraints.launch
trunk/examples/jpfESAS/launch/CEV-scriptless.launch
trunk/examples/jpfESAS/launch/CEV-tli.launch
trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEvent.java
trunk/src/gov/nasa/jpf/util/StringSetMatcher.java
Added Paths:
-----------
trunk/extensions/statechart/examples/ReceiverConstraints.es
trunk/extensions/statechart/examples/ReceiverConstraints.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-10-19 00:49:58
|
Revision: 638
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=638&view=rev
Author: pcmehlitz
Date: 2007-10-18 17:49:57 -0700 (Thu, 18 Oct 2007)
Log Message:
-----------
* the missing SimStateMachine receiver constraint support
note that the explicit send support is not yet correct: sendEvent(a,"foo") should match a.foo() or a.whatever.foo(),
but not abc.foo(). But it seems this belongs to StringSetMatcher and can be fixed later (the regex just gets
a bit more complicated)
Modified Paths:
--------------
trunk/examples/jpfESAS/launch/CEV-las-defect-sim.launch
trunk/examples/jpfESAS/launch/CEV-nominal-sim.launch
trunk/extensions/statechart/src/gov/nasa/jpf/jvm/choice/sc/SCEvent.java
trunk/extensions/statechart/src/gov/nasa/jpf/tools/sc/SimStateMachine.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-10-22 21:10:44
|
Revision: 642
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=642&view=rev
Author: pcmehlitz
Date: 2007-10-22 14:10:28 -0700 (Mon, 22 Oct 2007)
Log Message:
-----------
* fixed the annoying JPFException when specifying a non-existing application class (actually, it handles all
startup classes the same way now)
* added a Verify.set/getLocalAttr() debug method
* had to slightly change StackFrame.getLocalOffset() handling for this, which shouldn't throw an
exception anyways
* simplified the TestAttrsNew, which is going to be removed now anyways
* fixed the "lost attribute on backtrack" bug, which was nothing else than just a Fields.equals() that
wasn't aware of attributes. That's why it was spurious - sometimes, spuriousness tells a story.
* added attributes to the Fields hashing too. Not strictly required (hashCode isn't guaranteed to be unique
anyways), but seems like a good idea for sym exec (the other ones would get slowed down though)
Modified Paths:
--------------
trunk/examples/launch/basic-racer.launch
trunk/examples/launch/conc-1-RA.launch
trunk/src/gov/nasa/jpf/jvm/CollapsingRestorer.java
trunk/src/gov/nasa/jpf/jvm/Fields.java
trunk/src/gov/nasa/jpf/jvm/JPF_gov_nasa_jpf_jvm_Verify.java
trunk/src/gov/nasa/jpf/jvm/JVM.java
trunk/src/gov/nasa/jpf/jvm/StackFrame.java
trunk/src/gov/nasa/jpf/jvm/Verify.java
trunk/src/gov/nasa/jpf/util/HashData.java
trunk/test/gov/nasa/jpf/jvm/TestAttrs.java
trunk/test/gov/nasa/jpf/jvm/TestAttrsNew.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-10-29 20:32:07
|
Revision: 643
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=643&view=rev
Author: pcmehlitz
Date: 2007-10-29 13:31:58 -0700 (Mon, 29 Oct 2007)
Log Message:
-----------
* added return value reflection in ReturnInstruction
* added general local/parameter value reflection to Instruction (that doesn't
make the InvokeInstruction.getArgumentValues() irrelevant though, since it works
on the StackFrame the insn belongs to)
* with that, implemented a first version of PostConditions, including "old" values
I don't like the separation between old/current values, and the (lack of)
encapsulation, so I might still refactor this a bit
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/MethodInfo.java
trunk/src/gov/nasa/jpf/jvm/StackFrame.java
trunk/src/gov/nasa/jpf/jvm/StaticElementInfo.java
trunk/src/gov/nasa/jpf/jvm/bytecode/ARETURN.java
trunk/src/gov/nasa/jpf/jvm/bytecode/DRETURN.java
trunk/src/gov/nasa/jpf/jvm/bytecode/FRETURN.java
trunk/src/gov/nasa/jpf/jvm/bytecode/IRETURN.java
trunk/src/gov/nasa/jpf/jvm/bytecode/LRETURN.java
trunk/src/gov/nasa/jpf/jvm/bytecode/RETURN.java
trunk/src/gov/nasa/jpf/jvm/bytecode/ReturnInstruction.java
trunk/src/gov/nasa/jpf/test/Contract.java
trunk/src/gov/nasa/jpf/test/ContractAnd.java
trunk/src/gov/nasa/jpf/test/ContractOr.java
trunk/src/gov/nasa/jpf/test/EmptyContract.java
trunk/src/gov/nasa/jpf/test/Operand.java
trunk/src/gov/nasa/jpf/test/SimpleContract.java
trunk/src/gov/nasa/jpf/tools/ContractVerifier.java
trunk/test/gov/nasa/jpf/test/TestContracts.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-10-29 23:37:26
|
Revision: 644
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=644&view=rev
Author: pcmehlitz
Date: 2007-10-29 16:37:24 -0700 (Mon, 29 Oct 2007)
Log Message:
-----------
* forgot to commit @Ensures - Mea Culpa
* refactored and unified the value storage, which is now completely in ContractVerifier
(there was no need to have separate old and crrent value caches)
* refactored the error reporting, but I don't like it yet
* some fixes reg. handling of EmptyContract instances, esp. if the mdc contract
is empty. All the cotract hierarchy handling should be in class Contract itself
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/test/Contract.java
trunk/src/gov/nasa/jpf/test/ContractAnd.java
trunk/src/gov/nasa/jpf/test/ContractOr.java
trunk/src/gov/nasa/jpf/test/EmptyContract.java
trunk/src/gov/nasa/jpf/test/Operand.java
trunk/src/gov/nasa/jpf/test/SimpleContract.java
trunk/src/gov/nasa/jpf/tools/ContractVerifier.java
Added Paths:
-----------
trunk/app/gov/nasa/jpf/Ensures.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-11-01 02:07:41
|
Revision: 645
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=645&view=rev
Author: pcmehlitz
Date: 2007-10-31 19:07:39 -0700 (Wed, 31 Oct 2007)
Log Message:
-----------
* refactored the contract evaluation to turn the variable lookup policy into an object
(the old rule still holds: "if in doubt, turn it into an object"). The policy root class
VarLookup is now responsible for the caching (incl. old values)
this looks better, except of the error reporting, which is still hacked
* with this, implemented instance invariants. Currently, it's only evaluating at
ReturnInstructions of instance methods, and only if it's not a ctor.
This should be extended to method entry, static invariants and ctors. A question
that still remains is what to do with base class methods - shall we eval the
invariant above the level where it is introduced? At least base ctors need to
be filtered out, since they can hardly satisfy invariants for fields that aren't
initialized yet.
this still needs some thinking, but the infrastructure is in place
also need to add a @StaticInvariant, and maybe rename @Invariant accordingly,
so that it becomes obvious which one is evaluated in what context
Modified Paths:
--------------
trunk/src/gov/nasa/jpf/jvm/StackFrame.java
trunk/src/gov/nasa/jpf/test/Contract.java
trunk/src/gov/nasa/jpf/test/ContractAnd.java
trunk/src/gov/nasa/jpf/test/ContractOr.java
trunk/src/gov/nasa/jpf/test/EmptyContract.java
trunk/src/gov/nasa/jpf/test/Operand.java
trunk/src/gov/nasa/jpf/test/SimpleContract.java
trunk/src/gov/nasa/jpf/tools/ContractVerifier.java
trunk/test/gov/nasa/jpf/test/TestContracts.java
Added Paths:
-----------
trunk/app/gov/nasa/jpf/Invariant.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-11-01 18:05:10
|
Revision: 646
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=646&view=rev
Author: pcmehlitz
Date: 2007-11-01 11:05:08 -0700 (Thu, 01 Nov 2007)
Log Message:
-----------
* Duhh - forgot to commit the VarLookup (explicit commit selection in Eclipse is error-prone)
* added null operands
* added a hook for special variables (e.g. computed by the VM)
* changed the var lookup so that it can also handle null values
* added a Operand.CenterInterval, but the value conversion is kind of braindead - should
probably implement a full set of numeric operations for Operands, or it gets really messy
in terms of ad hoc type conversions
Modified Paths:
--------------
trunk/app/gov/nasa/jpf/Const.java
trunk/app/gov/nasa/jpf/Ensures.java
trunk/app/gov/nasa/jpf/Invariant.java
trunk/app/gov/nasa/jpf/Requires.java
trunk/src/gov/nasa/jpf/jvm/ElementInfo.java
trunk/src/gov/nasa/jpf/test/ContractSpec.g
trunk/src/gov/nasa/jpf/test/ContractSpecLexer.java
trunk/src/gov/nasa/jpf/test/ContractSpecParser.java
trunk/src/gov/nasa/jpf/test/Operand.java
trunk/test/gov/nasa/jpf/test/TestContracts.java
Added Paths:
-----------
trunk/app/gov/nasa/jpf/StaticInvariant.java
trunk/src/gov/nasa/jpf/test/VarLookup.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
|
From: <pcm...@us...> - 2007-11-02 05:06:41
|
Revision: 647
http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=647&view=rev
Author: pcmehlitz
Date: 2007-11-01 22:06:33 -0700 (Thu, 01 Nov 2007)
Log Message:
-----------
* added support for "String[] value" annotations, which are instantiated as conjunctions of contracts.
Not sure if that should be the same for pre- and post-conditions, but we sure need it for @Invariants,
and there a conjunction seems the only natural choice
Modified Paths:
--------------
trunk/.classpath
trunk/app/gov/nasa/jpf/Invariant.java
trunk/src/gov/nasa/jpf/JPF.java
trunk/src/gov/nasa/jpf/jvm/ClassInfo.java
trunk/src/gov/nasa/jpf/test/Contract.java
trunk/src/gov/nasa/jpf/tools/ContractVerifier.java
trunk/test/gov/nasa/jpf/test/TestContracts.java
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
×
Want the latest updates on software, tech news, and AI?
Get latest updates about software, tech news, and AI from SourceForge directly in your inbox once a month.
Thanks for helping keep SourceForge clean.
X