3 Commits (34eb8ebafb717e50fc46ece82c59029bd2a7c201)

Author	SHA1	Message	Date
Radu Grigore	3478a8828f	[topl] Added limits, to avoid high runtimes in corner-cases. ... Summary: Added a topl-max-disjuncts, which is analogous to pulse-max-disjuncts. Note, however, that the maximum number of states tracked will be the product of the two limits. Added also topl-max-conjuncts, which drops Topl states that became too complex. Reviewed By: jvillard Differential Revision: D25240386 fbshipit-source-id: 588c90390	4 years ago
Radu Grigore	d3ff423bb1	[topl] Don't put trivial large steps in trace. ... Summary: A "large step" is a call, and it is "trivial" if it does not affect the automaton state; i.e., if it is irrelevant to the property being tracked. Reviewed By: jvillard Differential Revision: D25209670 fbshipit-source-id: bf3e594b3	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