infer_clone

Commit Graph

Author	SHA1	Message	Date
Radu Grigore	6f83c45e47	[topl] Remove nondet marker Summary: The explicit marker for nondeterministic states was used to speed up the shallow implementations of Topl, which ar enow removed. Reviewed By: jvillard Differential Revision: D27297019 fbshipit-source-id: 0fce93817	4 years ago
Radu Grigore	59daa1f022	[topl] Added the ArrayWrite event type. Summary: Now one can use the pattern #ArrayWrite(A,I) to match on a write at index I in array A. This only works in the Pulse variant of Topl (not in the one based on SIL instrumentation). Reviewed By: jvillard Differential Revision: D25202768 fbshipit-source-id: 479f434e3	4 years ago

Author

SHA1

Message

Date

Radu Grigore

6f83c45e47

[topl] Remove nondet marker

Summary:
The explicit marker for nondeterministic states was used to speed up the
shallow implementations of Topl, which ar enow removed.

Reviewed By: jvillard

Differential Revision: D27297019

fbshipit-source-id: 0fce93817

Radu Grigore

59daa1f022

[topl] Added the ArrayWrite event type.

Summary:
Now one can use the pattern #ArrayWrite(A,I) to match on a write at
index I in array A. This only works in the Pulse variant of Topl (not in
the one based on SIL instrumentation).

Reviewed By: jvillard

Differential Revision: D25202768

fbshipit-source-id: 479f434e3

2 Commits (c82308e5860aa635e4d7e6fce9f62b05ca60011f)