infflow-autopilot.html 772 Bytes
Newer Older
Sarah Grebing's avatar
Sarah Grebing committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
<!DOCTYPE html>
<html lang="en">
<head>
    <meta charset="UTF-8">
    <title>infflow-autopilot</title>
</head>
<body>
<h2 id="infflow-autopilot">infflow-autopilot</h2>
<blockquote>
    <p>Synopsis: <code>infflow-autopilot;</code></p>
</blockquote>
<p><strong></strong>Description:</strong></strong></p>
This macro is tailored to information flow problems.
<ol>
    <li>Search exhaustively for applicable position, then
    <li>Start auxiliary computation
    <li>Finish symbolic execution
    <li>Try to close as many goals as possible
    <li>Apply macro recursively
    <li>Finish auxiliary computation
    <li>Use information flow contracts
    <li>Try to close as many goals as possible
</ol>

<p><strong>Arguments:</strong></p>
No arguments required

</body>
</html>