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
Summary:
PulseTopl.large_step is now implemented
All active tests are migrated now to topl-in-pulse.
Reviewed By: jvillard
Differential Revision: D25179556
fbshipit-source-id: dc1136bab
Summary:
Report errors found by running Topl on top of Pulse, when using
--topl-pulse. Topl tests now run on top of Pulse.
Reviewed By: jvillard
Differential Revision: D23030771
fbshipit-source-id: 8770c2902
Summary:
This is the kind of property for which the previous syntax forced one to
use spurious registers.
Reviewed By: ngorogiannis
Differential Revision: D20118863
fbshipit-source-id: b49740d33
Summary:
1. One should use either a writer or a stream to send a response, but not both.
2. A response should be forwarded only if it was commited.
Both properties are extracted from API comments on classes in the servlet API.
Reviewed By: jvillard
Differential Revision: D19514568
fbshipit-source-id: 79f0257ed
Summary:
If data comes from an outer OutputStream, then this outer OutputStream
needs to be flushed before getting the byte array.
Reviewed By: jvillard
Differential Revision: D19514569
fbshipit-source-id: e3e025394
Summary: add subdirectories so that we can run each java file against its own topl properties
Reviewed By: rgrig
Differential Revision: D19347302
fbshipit-source-id: 562830774
Summary:
This havocs event data, so that biabduction doesn't try to
track what was the last event processed by the monitor
(which is redundant as long as the state of the monitor
is tracked).
Reviewed By: ngorogiannis
Differential Revision: D19035491
fbshipit-source-id: a1c75daae
Summary:
In addition to
state1 -> state2: pattern
one can now also write
state1 -> state2: pattern if condition
where "condition" is some conjunction of comparisons (==,<,>) that
involve variables bound by "pattern", registers of the automaton, and
constants.
Reviewed By: ngorogiannis
Differential Revision: D19035496
fbshipit-source-id: 6f6e6a9be
Summary:
Instrument SIL according to TOPL properties. Roughly, the
instrumentation is a set of calls into procedures that simulate a
nondeterministic automaton. For now, those procedures are NOP dummies.
Reviewed By: jvillard
Differential Revision: D15063942
fbshipit-source-id: d22c2f6fa
Summary:
TOPL properties are essentially automata, which specify a bad pattern.
This commit is just a parser for them.
Reviewed By: jvillard
Differential Revision: D14477671
fbshipit-source-id: c38a8ef37
Radu Grigore
Jules Villard
Josh Berdine