[Javapathfinder-devel] SF.net SVN: javapathfinder: [700] trunk/extensions/symbc

[<ubn...@us...>]

Revision: 700
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=700&view=rev
Author:   ubnepvpb
Date:     2007-12-13 15:52:47 -0800 (Thu, 13 Dec 2007)

Log Message:
-----------
A new symbolic execution example in the doc: path coverage.
Changes to symbolic execution: new methods for collecting all the variables in a PathCondition and their values.

Modified Paths:
--------------
    trunk/extensions/symbc/doc/index.html
    trunk/extensions/symbc/doc/index.pdf
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/BinaryLinearIntegerExpression.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/BinaryNonLinearIntegerExpression.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/BinaryRealExpression.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/Constraint.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/Expression.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/IntegerConstant.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/RealConstant.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/SymbolicInteger.java
    trunk/extensions/symbc/src/gov/nasa/jpf/symbc/numeric/SymbolicReal.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

Added Paths:
-----------
    trunk/extensions/symbc/examples/coverage/
    trunk/extensions/symbc/examples/coverage/CheckCoverage.java
    trunk/extensions/symbc/examples/coverage/JPF_coverage_CheckCoverage.java
    trunk/extensions/symbc/examples/coverage/MyClassOriginal.java
    trunk/extensions/symbc/examples/coverage/MyClassWithPathAnnotations.java
    trunk/extensions/symbc/examples/coverage/MyDriverForPathAnnotations.java


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