infflow-autopilot

Synopsis: infflow-autopilot;

Description:

This macro is tailored to information flow problems.
  1. Search exhaustively for applicable position, then
  2. Start auxiliary computation
  3. Finish symbolic execution
  4. Try to close as many goals as possible
  5. Apply macro recursively
  6. Finish auxiliary computation
  7. Use information flow contracts
  8. Try to close as many goals as possible

Arguments:

No arguments required