3 Commits (fe1fd575935d9db380f7cf6f0317e7af8e7d5dcf)

Author	SHA1	Message	Date
Radu Grigore	3554101ece	[topl] Generate simpler monitor for deterministic states. ... Summary: This is an optimization. We ask the user to tell us which states are nondeterministic, and we generate code that handle nondeterminism only for those states. It is common for only one state per TOPL property to be nondeterministic. This speeds up the biabduction-analysis of the monitor by a factor of ~10. But, using the monitor is only a little faster. Facebook Reviewed By: jvillard Differential Revision: D19160286 fbshipit-source-id: 4dd39769a	5 years ago
Radu Grigore	d86e2f0d1c	[topl] Generate monitor. ... Summary: The synthetic methods from `topl.Property` are now nonempty: they simulate a nondeterministic automaton. Reviewed By: jvillard Differential Revision: D15668471 fbshipit-source-id: 050408283	6 years ago
Radu Grigore	047c64c528	[topl] Instrument SIL. ... 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	6 years ago