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

SourceForge Headquarters 225 Broadway Suite 1600 San Diego, CA 92101 +1 (858) 422-6466

Revision: 1277
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=1277&view=rev
Author:   frankrimlinger
Date:     2009-03-12 04:05:18 +0000 (Thu, 12 Mar 2009)

Log Message:
-----------
Finished baseline loop testing, with sessions for two_loops_in_a_row, while_with_conjunct big_model_check_test, and AxiomInLoop.  The new quantified logic expressions performed nicely.   No bugs encountered, except that AxiomInLoop.main() could not complete  because of an invariant factorization failure.  This is precisely the problem that will be addressed with jpf backtracking, so AxiomInLoop will serve as a first test case.

Mango feels faster than the legacy tool, mostly because all the intertask latency is gone.  But the memory leaking is becoming increasingly annoying, since the tool bellies up after just a few sessions.  Hopefully testing and memory tune-up can be done by the end of this month, then finally finally jpf integration.

Modified Paths:
--------------
    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/AxiomInLoop/
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/AxiomInLoop/<init>()V/
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/AxiomInLoop/<init>()V/case.zip
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/AxiomInLoop/divide_arrays([I[II)V/
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/AxiomInLoop/divide_arrays([I[II)V/for all i such that i is less than 'n' AND i is greater than or equal to 0 implies 'y'[i] does not equal 0.zip
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/AxiomInLoop/divide_arrays([I[II)V/loops/
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/AxiomInLoop/divide_arrays([I[II)V/loops/-baseline.AxiomInLoop.divide_arrays([I[II)V#14:iload_i_Code_01/
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/AxiomInLoop/divide_arrays([I[II)V/loops/-baseline.AxiomInLoop.divide_arrays([I[II)V#14:iload_i_Code_01/'y'['i'] does not equal 0.zip
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/AxiomInLoop/init_arrays([I[II)V/
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/AxiomInLoop/init_arrays([I[II)V/length of the Array 'x' is greater than or equal to 'n', length of the Array 'y' is greater than or equal to 'n'.zip
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/AxiomInLoop/init_arrays([I[II)V/loops/
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/AxiomInLoop/init_arrays([I[II)V/loops/-baseline.AxiomInLoop.init_arrays([I[II)V#20:iload_i_Code_01/
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/AxiomInLoop/init_arrays([I[II)V/loops/-baseline.AxiomInLoop.init_arrays([I[II)V#20:iload_i_Code_01/op0 is less than 'n'.zip
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/AxiomInLoop/main([I[II)Z/
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/AxiomInLoop/main([I[II)Z/for all i such that i is less than 'n' AND i is greater than or equal to 0 implies 'y'[i] does not equal 0.zip
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/big_model_check_test/
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/big_model_check_test/<init>()V/
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/big_model_check_test/<init>()V/case.zip
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/big_model_check_test/main(I)I/
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/big_model_check_test/main(I)I/'x' equals 10.zip
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/big_model_check_test/main(I)I/'x' is less than 10.zip
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/big_model_check_test/main(I)I/10 is less than 'x'.zip
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/find_negative/<init>()V/
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/find_negative/<init>()V/case.zip
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/find_negative/find_negative_test([II)I/for all i such that i is less than 'n' AND 0 is greater than or equal to i implies 'a'[i] is greater than or equal to 0.zip
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/two_loops_in_a_row/<init>()V/case.zip
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/two_loops_in_a_row/loops(I)I/case.zip
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/two_loops_in_a_row/loops(I)I/loops/-baseline.two_loops_in_a_row.loops(I)I#15:iload_j_Code_01/op0 is less than 'x'.zip
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/two_loops_in_a_row/loops(I)I/loops/-baseline.two_loops_in_a_row.loops(I)I#7:iload_i_Code_01/op0 is less than 'x'.zip
    branches/mango/extensions/mango/local/franklocal/sessions/baseline/two_loops_in_a_row/main(I)Z/'x' is greater than or equal to 0.zip
    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/case.zip
    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/case.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 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/case.zip
    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/-baseline.while_with_conjunct.simple_loop(I)I#2:iload_x_Code_01/op0 is less than 5.zip

Removed Paths:
-------------
    branches/mango/extensions/mango/jars/.cvsignore
    branches/mango/extensions/mango/jars/.project

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