infer_clone

Commit Graph

Author	SHA1	Message	Date
Radu Grigore	91ebfe9c20	[topl] Support side conditions for transitions. 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	5 years ago
Radu Grigore	10d87eec4e	[topl] Simple error reporting. Reviewed By: jvillard Differential Revision: D15875271 fbshipit-source-id: 148206be9	6 years ago
Radu Grigore	8bf65086e3	[topl] Parser for temporal properties 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	6 years ago

Author

SHA1

Message

Date

Radu Grigore

91ebfe9c20

[topl] Support side conditions for transitions.

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

Radu Grigore

10d87eec4e

[topl] Simple error reporting.

Reviewed By: jvillard

Differential Revision: D15875271

fbshipit-source-id: 148206be9

Radu Grigore

8bf65086e3

[topl] Parser for temporal properties

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

3 Commits (5776d7cfab570c83061674b6ad698c3d8fab27e7)