[Javapathfinder-svn] SF.net SVN: javapathfinder:[1262] branches/mango/extensions/mango

[<fra...@us...>]

Revision: 1262
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1262&view=rev
Author:   frankrimlinger
Date:     2009-03-09 03:40:22 +0000 (Mon, 09 Mar 2009)

Log Message:
-----------
Fixed some E-Z bugs, and generated the sessions for the while_with_conjunct baseline test. This completes the "classical" set of loop tests written by Robert Krug at UT Austin.  At one time, the proof artifacts (e.g. rules) generated by these examples were actually admitted into the ACL2 logic and proven.  Much has changed since that time, but I hope to pick up this thread again some day.  Meanwhile, there are many more tests, and then all of the java.lang modelled by Mango has to be regenerated.  So far, so good.

Modified Paths:
--------------
    branches/mango/extensions/mango/Mango/src/mango/source/agent/msg/SourceViewCreateRequestMsg.java
    branches/mango/extensions/mango/Mango/src/mango/worker/workFlow/invariant/agent/InvariantHypoAgent.java
    branches/mango/extensions/mango/Mango/src/mango/workstation/Workstation.java
    branches/mango/extensions/mango/Mango/src/mango/workstation/action/MangoActionManager.java
    branches/mango/extensions/mango/local/franklocal/rules/rulebase.zip
    branches/mango/extensions/mango/local/franklocal/sessions/a.zip

Added Paths:
-----------
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/while_with_conjunct/
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/while_with_conjunct/<init>()V/
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/while_with_conjunct/<init>()V/case.zip
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/while_with_conjunct/conjunctive_while_loop(II)I/
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/while_with_conjunct/conjunctive_while_loop(II)I/'x in loop at #3:iload_x' is greater than or equal to 5.zip
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/while_with_conjunct/conjunctive_while_loop(II)I/'y in loop at #3:iload_x' is greater than or equal to 5.zip
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/while_with_conjunct/conjunctive_while_loop(II)I/loops/
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/while_with_conjunct/conjunctive_while_loop(II)I/loops/-baseline.while_with_conjunct.conjunctive_while_loop(II)I#3:iload_x_Code_01/
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/while_with_conjunct/conjunctive_while_loop(II)I/loops/-baseline.while_with_conjunct.conjunctive_while_loop(II)I#3:iload_x_Code_01/op0 is less than 5.zip
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/while_with_conjunct/disjunctive_while_loop(II)I/
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/while_with_conjunct/disjunctive_while_loop(II)I/case.zip
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/while_with_conjunct/disjunctive_while_loop(II)I/loops/
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/while_with_conjunct/disjunctive_while_loop(II)I/loops/-Alpha_baseline.while_with_conjunct.disjunctive_while_loop(II)I#3:iload_x_Code/
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/while_with_conjunct/disjunctive_while_loop(II)I/loops/-Alpha_baseline.while_with_conjunct.disjunctive_while_loop(II)I#3:iload_x_Code/op0 is greater than or equal to 5.zip
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/while_with_conjunct/disjunctive_while_loop(II)I/loops/-Alpha_baseline.while_with_conjunct.disjunctive_while_loop(II)I#3:iload_x_Code/op0 is less than 5.zip
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/while_with_conjunct/main(II)Z/
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/while_with_conjunct/main(II)Z/case.zip
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/while_with_conjunct/simple_loop(I)I/
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/while_with_conjunct/simple_loop(I)I/case.zip
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/while_with_conjunct/simple_loop(I)I/loops/
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/while_with_conjunct/simple_loop(I)I/loops/-baseline.while_with_conjunct.simple_loop(I)I#2:iload_x_Code_01/
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/while_with_conjunct/simple_loop(I)I/loops/-baseline.while_with_conjunct.simple_loop(I)I#2:iload_x_Code_01/op0 is less than 5.zip


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