From b948c3e18235903af87422ae2f2c3d9f22c385db Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Mon, 27 Jan 2020 07:13:48 -0800 Subject: [PATCH] [topl] delete unused test file Summary: It's not used. Reviewed By: mityal Differential Revision: D19537449 fbshipit-source-id: 505e6b87b --- .../codetoanalyze/java/topl/iterators.topl | 36 ------------------- .../java/topl/servlet/servlet.topl.inactive | 19 ---------- 2 files changed, 55 deletions(-) delete mode 100644 infer/tests/codetoanalyze/java/topl/iterators.topl delete mode 100644 infer/tests/codetoanalyze/java/topl/servlet/servlet.topl.inactive 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)