...
 
Commits (5)
......@@ -3,13 +3,12 @@ macro autopilot;
# Invariant Initially Valid:
rule castAdd
formula="java.lang.Object::<inv>(heapAfter_iterator, result)"
formula="java.lang.Object::<inv>(heapAfter_listIterator, result)"
on="result";
auto;
# Body Preserves Invariant:
# Body Preserves Invariant
# Normal Execution
rule castAdd
formula="java.lang.Object::<inv>(heapAfter_addInputCol, result)"
on="result";
......@@ -21,16 +20,15 @@ rule applyEqReverse
formula="\exists int i; (  leq(Z(0(#)), i) & lt(i, seqLen(Seq::select(heapAfter_next, org.apache.commons.csv.CSVRecord::select(heap, self, de.polyas.core3.open.cred.CredTool::$record), org.apache.commons.csv.CSVRecord::$key_seq))) &   (java.lang.String)(any::seqGet(Seq::select(heapAfter_next, org.apache.commons.csv.CSVRecord::select(heap, self, de.polyas.core3.open.cred.CredTool::$record), org.apache.commons.csv.CSVRecord::$key_seq), i)) = (java.lang.String)result_2)"
on="result_2";
rule seqCastRemoveBeta
formula="\exists int i; (  leq(Z(0(#)), i) & lt(i, seqLen(Seq::select(heapAfter_next, org.apache.commons.csv.CSVRecord::select(heap, self, de.polyas.core3.open.cred.CredTool::$record), org.apache.commons.csv.CSVRecord::$key_seq))) &   (java.lang.String)(any::seqGet(Seq::select(heapAfter_next, org.apache.commons.csv.CSVRecord::select(heap, self, de.polyas.core3.open.cred.CredTool::$record), org.apache.commons.csv.CSVRecord::$key_seq), i)) = (java.lang.String)(java.lang.Object::seqGet(Seq::select(heap, java.util.ArrayList::select(heap, self, de.polyas.core3.open.cred.CredTool::$cols), java.util.Collection::$seq), int::select(anon_heap_LOOP<<anonHeapFunction>>, result, java.util.Iterator::$index))))"
on="(java.lang.String)(java.lang.Object::seqGet(Seq::select(heap, java.util.ArrayList::select(heap, self, de.polyas.core3.open.cred.CredTool::$cols), java.util.Collection::$seq), int::select(anon_heap_LOOP<<anonHeapFunction>>, result, java.util.Iterator::$index)))";
instantiate var="j" with="int::select(anon_heap_LOOP<<anonHeapFunction>>, result, java.util.Iterator::$index)" hide;
formula="\exists int i; (  leq(Z(0(#)), i) & lt(i, seqLen(Seq::select(heapAfter_next, org.apache.commons.csv.CSVRecord::select(heap, self, de.polyas.core3.open.cred.CredTool::$record), org.apache.commons.csv.CSVRecord::$key_seq))) &   (java.lang.String)(any::seqGet(Seq::select(heapAfter_next, org.apache.commons.csv.CSVRecord::select(heap, self, de.polyas.core3.open.cred.CredTool::$record), org.apache.commons.csv.CSVRecord::$key_seq), i)) = (java.lang.String)(java.lang.Object::seqGet(Seq::select(heap, java.util.ArrayList::select(heap, self, de.polyas.core3.open.cred.CredTool::$cols), java.util.Collection::$seq), int::select(anon_heap_LOOP<<anonHeapFunction>>, result, java.util.ListIterator::$index))))"
on="(java.lang.String)(java.lang.Object::seqGet(Seq::select(heap, java.util.ArrayList::select(heap, self, de.polyas.core3.open.cred.CredTool::$cols), java.util.Collection::$seq), int::select(anon_heap_LOOP<<anonHeapFunction>>, result, java.util.ListIterator::$index)))";
instantiate var="j" with="int::select(anon_heap_LOOP<<anonHeapFunction>>, result, java.util.ListIterator::$index)" hide;
rule impLeft;
tryclose;
# ClassCastException
rule applyEqReverse
formula="java.lang.String::instance(result_2) = TRUE"
on="result_2";
rule seqCastInstance
formula="java.lang.String::instance(java.lang.Object::seqGet(Seq::select(heap, java.util.ArrayList::select(heap, self, de.polyas.core3.open.cred.CredTool::$cols), java.util.Collection::$seq), int::select(anon_heap_LOOP<<anonHeapFunction>>, result, java.util.Iterator::$index))) = TRUE";
tryclose;
formula="!(java.lang.String)result_2 = null"
on="result_2";
rule seqCastRemoveBeta
formula="!  (java.lang.String)(java.lang.Object::seqGet(Seq::select(heap, java.util.ArrayList::select(heap, self, de.polyas.core3.open.cred.CredTool::$cols), java.util.Collection::$seq), int::select(anon_heap_LOOP<<anonHeapFunction>>, result, java.util.ListIterator::$index))) = null";
auto;
This diff is collapsed.
This diff is collapsed.
package java.io;
public class PrintStream extends java.io.FilterOutputStream {
public PrintStream(java.io.OutputStream out);
public PrintStream(java.io.OutputStream out, boolean autoFlush);
public void print(boolean b);
public void print(char c);
public void print(int i);
public void print(long l);
// public void print(float f);
// public void print(double d);
public void print(char[] s);
public void print(java.lang.String s);
public void print(java.lang.Object obj);
public void println();
public void println(boolean x);
public void println(char x);
public void println(int x);
public void println(long x);
// public void println(float x);
// public void println(double x);
public void println(char[] x);
public void println(java.lang.String x);
public void println(java.lang.Object x);
}
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Fri Mar 28 13:47:08 CET 2008
*/
package java.io;
public interface Serializable
{
}
......@@ -6,17 +6,77 @@ public final class System {
public static final java.io.PrintStream out;
public static final java.io.PrintStream err;
/*@ public behavior
@ requires true;
@ ensures true;
@ assignable \everything;
@*/
public static void arraycopy(java.lang.Object src, int srcPos, java.lang.Object dest, int destPos, int length);
/*@ public behavior
@ ensures false;
@ signals_only \nothing;
// Remarks: Currently the specifications assumes src and dest to be int[].
// This is incomplete, and should be amended when needed
// added by Mattias Ulbrich in Jan 19.
/*@ public exceptional_behavior
@ requires src == null || dest == null;
@ signals_only NullPointerException;
@ assignable \nothing;
@ also
@ public exceptional_behavior
@ requires src instanceof int[] && dest instanceof int[];
@ requires src != null && dest != null;
@ requires (srcPos < 0 || destPos < 0 || length < 0
@ || srcPos + length > ((int[])src).length
@ || destPos + length > ((int[])dest).length);
@ assignable \nothing;
@ signals_only ArrayIndexOutOfBoundsException;
@ also
@ public normal_behavior
@ requires src instanceof int[] && dest instanceof int[];
@ requires src != null && dest != null;
@ requires srcPos >= 0 && destPos >= 0;
@ requires length >= 0;
@ requires srcPos + length <= ((int[])src).length
@ && destPos + length <= ((int[])dest).length;
@ ensures (\forall int i; 0 <= i && i < length;
@ ((int[])dest)[destPos + i] == \old(((int[])src)[srcPos + i]));
@ assignable ((int[])dest)[destPos .. destPos + length - 1];
@*/
public static native void arraycopy(/*@nullable*/ java.lang.Object src, int srcPos,
/*@nullable*/ java.lang.Object dest, int destPos,
int length);
// This implementation has been used to verify the above contracts
// {
// if(src == null || dest == null) {
// throw new NullPointerException();
// }
// int[] isrc = (int[])src;
// int[] idest = (int[])dest;
// if(length < 0) {
// throw new ArrayIndexOutOfBoundsException();
// }
// int[] tmp = new int[length];
// if(srcPos < 0 || srcPos + length > isrc.length) {
// throw new ArrayIndexOutOfBoundsException();
// }
// /*@ loop_invariant 0 <= i && i <= length;
// @ loop_invariant (\forall int j; 0<=j && j < i; tmp[j] == isrc[srcPos + j]);
// @ loop_invariant \fresh(tmp);
// @ decreases length - i;
// @ assignable tmp[*];
// @*/
// for(int i = 0; i < length; i++) {
// tmp[i] = isrc[srcPos + i];
// }
// if(destPos < 0 || destPos + length > idest.length) {
// throw new ArrayIndexOutOfBoundsException();
// }
// /*@ loop_invariant 0 <= k && k <= length;
// @ loop_invariant (\forall int j; 0<=j && j < k; idest[destPos + j] == tmp[j]);
// @ decreases length - k;
// @ assignable idest[destPos .. destPos + length - 1];
// @*/
// for(int k = 0; k < length; k++) {
// idest[destPos + k] = tmp[k];
// }
// }
/*@ public behavior
@ ensures false;
@ signals_only \nothing;
@ diverges true;
@*/
public static void exit(int code);
public static void exit(int code);
}
......@@ -49,15 +49,6 @@ public interface Collection extends java.lang.Iterable
public boolean contains(String arg0);
public boolean containsAll(java.util.Collection arg0);
/*@ public normal_behavior
@ ensures \result.index == 0;
@ ensures \result.seq == seq;
@ ensures \fresh(\result) && \fresh(\result.*);
@ ensures \result instanceof java.util.CollectionIterator;
@ assignable \nothing;
@ determines \result.seq \by seq;
@ determines \result.index \by \nothing;
@*/
public java.util.Iterator iterator();
public java.lang.Object[] toArray();
......
package java.util;
public final class CollectionIterator implements Iterator { }
/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
* Date: Fri Mar 28 13:47:08 CET 2008
*/
package java.util;
public interface Iterator
{
//@ public instance ghost \seq seq;
//@ public instance ghost \bigint index;
//@ public instance invariant 0 <= index && index <= seq.length;
/*@ public normal_behavior
@ ensures \result == true <==> index < seq.length;
@ assignable \strictly_nothing;
@ determines \result \by seq.length, index;
@*/
public boolean hasNext();
/*@ public normal_behavior
@ ensures \old(index) < seq.length ==> \result == ((Object)seq[\old(index)]);
@ ensures \old(index) < seq.length ==> \result != null;
@ ensures \old(index) < seq.length ==> index == \old(index) + 1;
@ ensures \old(index) == seq.length ==> \result == null;
@ ensures \old(index) == seq.length ==> index == \old(index);
@ assignable index;
@ determines \result \by seq, index;
@ determines index \by seq.length, index;
@*/
public /*@nullable@*/ java.lang.Object next();
public /*@nullable@*/ Object next();
public void remove();
}
......@@ -27,6 +27,15 @@ public interface List extends java.util.Collection
public int indexOf(java.lang.Object arg0);
public int lastIndexOf(java.lang.Object arg0);
/*@ public normal_behavior
@ ensures \result.index == 0;
@ ensures \result.seq == seq;
@ ensures \fresh(\result) && \fresh(\result.*);
@ ensures \result instanceof ListIteratorImpl;
@ assignable \nothing;
@ determines \result.seq \by seq;
@ determines \result.index \by \nothing;
@*/
public java.util.ListIterator listIterator();
public java.util.ListIterator listIterator(int arg0);
public java.util.List subList(int arg0, int arg1);
......
......@@ -5,9 +5,29 @@ package java.util;
public interface ListIterator extends java.util.Iterator
{
//@ public instance ghost \seq seq;
//@ public instance ghost \bigint index;
//@ public instance invariant 0 <= index && index <= seq.length;
public boolean hasNext();
public java.lang.Object next();
/*@ public normal_behavior
@ ensures \result == true <==> index < seq.length;
@ assignable \strictly_nothing;
@ determines \result \by seq.length, index;
@*/
public boolean hasNext();
/*@ public behavior
@ requires index < seq.length;
@ ensures \result == ((Object)seq[\old(index)]);
@ ensures index == \old(index) + 1;
@ assignable index;
@ signals_only java.lang.RuntimeException;
@ determines \result \by seq, index;
@ determines index \by \itself;
@*/
public /*@nullable@*/ Object next();
public boolean hasPrevious();
public java.lang.Object previous();
public int nextIndex();
......
package java.util;
/*
* This final implementation of the Iterator interface is used for the iterators returned
* by Lists in the JavaRedux library.
*
* It thus models the various implementation-dependent Iterator classes used in a Java
* library. Since these are not visible to the library user, they are -- like this class --
* effectively final.
*/
public final class ListIteratorImpl implements ListIterator { }
......@@ -2,9 +2,5 @@ package org.bouncycastle.openpgp;
public class PGPPublicKeyRing extends org.bouncycastle.openpgp.PGPKeyRing implements org.bouncycastle.util.Iterable {
/*@ public normal_behavior
@ ensures \result.index == 0;
@ assignable \nothing;
@*/
public java.util.CollectionIterator getPublicKeys();
public java.util.Iterator getPublicKeys();
}
\ No newline at end of file
......@@ -7,9 +7,5 @@ public class PGPPublicKeyRingCollection extends java.lang.Object implements org.
@*/
public PGPPublicKeyRingCollection(java.io.InputStream param0, org.bouncycastle.openpgp.operator.KeyFingerPrintCalculator param1) throws java.io.IOException, org.bouncycastle.openpgp.PGPException;
/*@ public normal_behavior
@ ensures \result.index == 0;
@ assignable \nothing;
@*/
public java.util.CollectionIterator getKeyRings();
public java.util.Iterator getKeyRings();
}
\ No newline at end of file
......@@ -13,6 +13,7 @@ import java.util.Date;
import java.util.Iterator;
import java.util.LinkedHashMap;
import java.util.LinkedList;
import java.util.ListIterator;
import java.util.Map;
import org.apache.commons.csv.CSVFormat;
......@@ -394,25 +395,32 @@ public final class CredTool {
@ determines vals.seq \by vals.seq, cols.seq, record.key_seq, record.value_seq, (\seq_def int i; 0; cols.seq.length; \dl_strContent(((String)cols.seq[i])));
@*/
private /*@helper@*/ void addInputCols() {
Iterator it = cols.iterator();
/*@ loop_invariant (\forall \bigint j; 0 <= j && j < cols.seq.length;
@ (\exists \bigint i; 0 <= i && i < record.key_seq.length; ((String)record.key_seq[i]) == ((String)cols.seq[j])));
@ loop_invariant (\forall \bigint i; 0 <= i && i < cols.seq.length; ((String)cols.seq[i]) != null);
@ loop_invariant vals != cols;
@ loop_invariant \invariant_for(record);
@ loop_invariant \invariant_for(vals);
@ loop_invariant \invariant_for(cols);
@ loop_invariant \invariant_for(it);
@ loop_invariant it != null && record != null && vals != null && cols != null;
@ loop_invariant it instanceof java.util.CollectionIterator;
@ loop_invariant it.seq == cols.seq;
@ decreases it.seq.length - it.index;
@ assignable vals.seq, it.index;
@ determines vals.seq, it.seq, it.index, record.key_seq, record.value_seq, (\seq_def int i; 0; it.seq.length; \dl_strContent(((String)it.seq[i]))) \by \itself;
@*/
while (it.hasNext()) {
addInputCol(vals, (String) it.next(), record);
ListIterator it = cols.listIterator();
try {
/*@ loop_invariant (\forall \bigint j; 0 <= j && j < cols.seq.length;
@ (\exists \bigint i; 0 <= i && i < record.key_seq.length; ((String)record.key_seq[i]) == ((String)cols.seq[j])));
@ loop_invariant (\forall \bigint i; 0 <= i && i < cols.seq.length; ((String)cols.seq[i]) != null);
@ loop_invariant vals != cols;
@ loop_invariant \invariant_for(record);
@ loop_invariant \invariant_for(vals);
@ loop_invariant \invariant_for(cols);
@ loop_invariant \invariant_for(it);
@ loop_invariant it != null && record != null && vals != null && cols != null;
@ loop_invariant it.seq == cols.seq;
@ loop_invariant it instanceof java.util.ListIteratorImpl;
@ decreases it.seq.length - it.index;
@ assignable vals.seq, it.index;
@ determines vals.seq, it.seq, it.index, record.key_seq, record.value_seq, (\seq_def int i; 0; it.seq.length; \dl_strContent(((String)it.seq[i]))) \by \itself;
@*/
while (it.hasNext()) {
addInputCol(vals, (String) it.next(), record);
}
} catch (RuntimeException e) {
// Because `cols` is not modified in any way while it is being iterated over, no
// exception should occur here.
// However, this `catch` clause is still necessary to conform to the Iterator
// specification.
}
}
......@@ -501,20 +509,28 @@ public final class CredTool {
private static ArrayList extractInputColsForDist(final LinkedList cols, final String id) {
final ArrayList result = new ArrayList();
final Iterator it = cols.iterator();
final ListIterator it = cols.listIterator();
/*@ loop_invariant \invariant_for(it);
@ loop_invariant it.seq == cols.seq;
@ loop_invariant (\forall \bigint i; 0 <= i && i < result.seq.length; ((String)result.seq[i]) != null);
@ decreases cols.seq.length - it.index;
@ assignable result.seq, it.index;
@*/
while (it.hasNext()) {
String next = (String) it.next();
if (!id.equals(next)) {
result.add(next);
try {
/*@ loop_invariant \invariant_for(it);
@ loop_invariant it.seq == cols.seq;
@ loop_invariant (\forall \bigint i; 0 <= i && i < result.seq.length; ((String)result.seq[i]) != null);
@ loop_invariant it instanceof java.util.ListIteratorImpl;
@ decreases cols.seq.length - it.index;
@ assignable result.seq, it.index;
@*/
while (it.hasNext()) {
String next = (String) it.next();
if (!id.equals(next)) {
result.add(next);
}
}
} catch(RuntimeException e) {
// Because `cols` is not modified in any way while it is being iterated over, no
// exception should occur here.
// However, this `catch` clause is still necessary to conform to the Iterator
// specification.
}
return result;
......
open goals,0
Nodes,36,607
Branches,765
Nodes,65,665
Branches,1,424
Interactive steps,0
Symbolic execution steps,498
Automode time,114.3s
Automode time,114387ms
Avg. time per step,3.124ms
Symbolic execution steps,845
Automode time,166.3s
Automode time,166383ms
Avg. time per step,2.533ms
Rule applications
Quantifier instantiations,30
One-step Simplifier apps,6120
Quantifier instantiations,128
One-step Simplifier apps,10082
SMT solver apps,0
Dependency Contract apps,0
Operation Contract apps,8
Block/Loop Contract apps,0
Loop invariant apps,1
Merge Rule apps,0
Total rule apps,46,861
Total rule apps,78,712
open goals,0
Nodes,11,895
Branches,149
Nodes,12,552
Branches,176
Interactive steps,0
Symbolic execution steps,178
Automode time,24.9s
Automode time,24980ms
Avg. time per step,2.100ms
Symbolic execution steps,207
Automode time,27.8s
Automode time,27882ms
Avg. time per step,2.221ms
Rule applications
Quantifier instantiations,34
One-step Simplifier apps,1112
Quantifier instantiations,38
One-step Simplifier apps,1186
SMT solver apps,0
Dependency Contract apps,0
Operation Contract apps,6
Block/Loop Contract apps,0
Loop invariant apps,1
Merge Rule apps,0
Total rule apps,17,340
Total rule apps,18,029
open goals,0
Nodes,90,434
Branches,494
Nodes,89,252
Branches,586
Interactive steps,0
Symbolic execution steps,553
Automode time,8min
Automode time,503982ms
Avg. time per step,5.572ms
Symbolic execution steps,659
Automode time,11min
Automode time,714238ms
Avg. time per step,8.002ms
Rule applications
Quantifier instantiations,178
One-step Simplifier apps,8523
Quantifier instantiations,200
One-step Simplifier apps,7863
SMT solver apps,0
Dependency Contract apps,0
Operation Contract apps,55
Operation Contract apps,61
Block/Loop Contract apps,0
Loop invariant apps,2
Merge Rule apps,0
Total rule apps,127,857
Total rule apps,118,766