diff --git a/infer/tests/codetoanalyze/java/topl/iterators.topl b/infer/tests/codetoanalyze/java/topl/iterators.topl deleted file mode 100644 index 34d37da30..000000000 --- a/infer/tests/codetoanalyze/java/topl/iterators.topl +++ /dev/null @@ -1,36 +0,0 @@ -property HasNext - prefix "Iterator" - prefix "List" - nondet (start) - start -> start: * - start -> invalid: I = iterator(*) - invalid -> valid: = hasNext(i) // treat as shorthand for = hasNext if (b) - valid -> invalid: next(i) - invalid -> error: next(i) - -property UnsafeIterator - prefix "Collection" - prefix "Iterator" - nondet (start) - start -> start: * - start -> iterating: I = iterator(C) - iterating -> modified: remove(c, *) - iterating -> modified: add(c, *) - modified -> error: next(i) - -property UnsafeMapIterator - nondet (start) - start -> start: * - start -> gotView: View = keySet(M) - start -> gotView: View = values(M) - gotView -> iterating: I = iterator(view) - iterating -> updated: put(m, *) - updated -> error: next(i) - -property SkipIndexAfterRemove - prefix "ArrayList" - nondet (start) - start -> start: * - start -> removed: remove(Collection, Index) - removed -> ok: get(collection, index) - removed -> error: get(collection, J) if J != index diff --git a/infer/tests/codetoanalyze/java/topl/servlet/servlet.topl.inactive b/infer/tests/codetoanalyze/java/topl/servlet/servlet.topl.inactive deleted file mode 100644 index aec77e889..000000000 --- a/infer/tests/codetoanalyze/java/topl/servlet/servlet.topl.inactive +++ /dev/null @@ -1,19 +0,0 @@ -// A weaker version of InterleavedResponse -property InterleavedResponseWeak - // vertex names: w = got writer; W = used writer; similarly for s, S - message "Incompatible methods for putting data into a response were used." - prefix "javax.servlet.ServletResponse" - nondet (start) - start -> start: * - start -> w: W = getWriter(R) - start -> s: S = getOutputStream(R) - w -> sw: S = getOutputStream(r) - s -> sw: W = getWriter(r) - w -> W: *(w) - sw -> sW: *(w) - s -> S: *(s) - sw -> Sw: *(s) - W -> sW: S = getOutputStream(r) - S -> Sw: W = getWriter(r) - sW -> error: *(s) - Sw -> error: *(w)