This file contains ambiguous Unicode characters that may be confused with others in your current locale. If your use case is intentional and legitimate, you can safely ignore this warning. Use the Escape button to highlight these characters.
<!DOCTYPE html>
<htmlxmlns="http://www.w3.org/1999/xhtml"><head><title>CTL (infer.ASTLanguage.CTL)</title><linkrel="stylesheet"href="../../../odoc.css"/><metacharset="utf-8"/><metaname="generator"content="odoc 1.5.2"/><metaname="viewport"content="width=device-width,initial-scale=1.0"/><scriptsrc="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><divclass="content"><header><nav><ahref="../index.html">Up</a>–<ahref="../../index.html">infer</a>»<ahref="../index.html">ASTLanguage</a>» CTL</nav><h1>Module <code>ASTLanguage.CTL</code></h1></header><aside><p>This module defines a language to define checkers. These checkers are interpreted over the AST of the program. A checker is defined by a CTL formula which expresses a condition saying when the checker should report a problem.</p></aside><dl><dtclass="spec type"id="type-clause"><ahref="#type-clause"class="anchor"></a><code><spanclass="keyword">type</span> clause</code><code> = </code><tableclass="variant"><trid="type-clause.CLet"class="anchored"><tdclass="def constructor"><ahref="#type-clause.CLet"class="anchor"></a><code>| </code><code><spanclass="constructor">CLet</span><spanclass="keyword">of</span><ahref="../ALVar/index.html#type-formula_id">ALVar.formula_id</a> * <span><ahref="../ALVar/index.html#type-t">ALVar.t</a> list</span> * <ahref="../CTLTypes/index.html#type-t">CTLTypes.t</a></code></td><tdclass="doc"><p>Let clause: let id = definifion;</p></td></tr><trid="type-clause.CSet"class="anchored"><tdclass="def constructor"><ahref="#type-clause.CSet"class="anchor"></a><code>| </code><code><spanclass="constructor">CSet</span><spanclass="keyword">of</span><ahref="../ALVar/index.html#type-keyword">ALVar.keyword</a> * <ahref="../CTLTypes/index.html#type-t">CTLTypes.t</a></code></td><tdclass="doc"><p>Set clause: set id = definition</p></td></tr><trid="type-clause.CDesc"class="anchored"><tdclass="def constructor"><ahref="#type-clause.CDesc"class="anchor"></a><code>| </code><code><spanclass="constructor">CDesc</span><spanclass="keyword">of</span><ahref="../ALVar/index.html#type-keyword">ALVar.keyword</a> * string</code></td><tdclass="doc"><p>Description clause eg: set message = "..."</p></td></tr><trid="type-clause.CPath"class="anchored"><tdclass="def constructor"><ahref="#type-clause.CPath"class="anchor"></a><code>| </code><code><spanclass="constructor">CPath</span><spanclass="keyword">of</span><span>[ `WhitelistPath <span>| `BlacklistPath</span> ]</span> * <span><ahref="../ALVar/index.html#type-t">ALVar.t</a> list</span></code></td></tr></table></dt><dd><p>"set" clauses are used for defining mandatory variables that will be used by when reporting issues: eg for defining the condition.</p><p>"desc" clauses are used for defining the error message, the suggestion, the severity.</p><p>"let" clauses are used to define temporary formulas which are then used to abbreviate the another formula. For example</p><pre> let f = a And B
set formula = f OR f
set message = "bla"</pre></dd></dl><dl><dtclass="spec type"id="type-ctl_checker"><ahref="#type-ctl_checker"class="anchor"></a><code><spanclass="keyword">type</span> ctl_checker</code><code> = </code><code>{</code><tableclass="record"><trid="type-ctl_checker.id"class="anchored"><tdclass="def field"><ahref="#type-ctl_checker.id"class="anchor"></a><code>id : string;</code></td><tdclass="doc"><p>Checker's id</p></td></tr><trid="type-ctl_checker.definitions"class="anchored"><tdclass="def field"><ahref="#type-ctl_checker.definitions"class="anchor"></a><code>definitions : <span><ahref="index.html#type-clause">clause</a> list</span>;</code></td><tdclass="doc"><p>A list of let/set definitions</p></td></tr></table><code>}</code></dt><dtclass="spec type"id="type-al_file"><ahref="#type-al_file"class="anchor"></a><code><spanclass="keyword">type</span> al_file</code><code> = </code><code>{</code><tableclass="record"><trid="type-al_file.import_files"class="anchored"><tdclass="def field"><ahref="#type-al_file.import_files"class="anchor"></a><code>import_files : <span>string list</span>;</code></td></tr><trid="type-al_file.global_macros"class="anchored"><tdclass="def field"><ahref="#type-al_file.global_macros"class="anchor"></a><code>global_macros : <span><ahref="index.html#type-clause">clause</a> list</span>;</code></td></tr><trid="type-al_file.global_paths"class="anchored"><tdclass="def field"><ahref="#type-al_file.global_paths"class="anchor"></a><code>global_paths : <span><span>(string * <span><ahref="../ALVar/index.html#type-alexp">ALVar.alexp</a> list</span>)</span> list</span>;</code></td></tr><trid="type-al_file.checkers"class="anchored"><tdclass="def field"><ahref="#type-al_file.checkers"class="anchor"></a><code>checkers : <span><ahref="index.html#type-ctl_checker">ctl_checker</a> list</span>;</code></td></tr></table><code>}</code></dt></dl><dl><dtclass="spec value"id="val-print_checker"><ahref="#val-print_checker"class="anchor"></a><code><spanclass="keyword">val</span> print_checker : <ahref="index.html#type-ctl_checker">ctl_checker</a><span>-></span> unit</code></dt><dtclass="spec value"id="val-eval_formula"><ahref="#val-eval_formula"class="anchor"></a><code><spanclass="keyword">val</span> eval_formula : <span>?⁠keep_witness:bool</span><span>-></span><ahref="../CTLTypes/index.html#type-t">CTLTypes.t</a><span>-></span><ahref="../Ctl_parser_types/index.html#type-ast_node">Ctl_parser_types.ast_node</a><span>-></span><ahref="../CLintersContext/index.html#type-context">CLintersContext.context</a><span>-></span><span><ahref="../Ctl_parser_types/index.html#type-ast_node">Ctl_parser_types.ast_node</a> option</span></code></dt><dd><p>return the evaluation of the formula and a witness</p></dd></dl><dl><dtclass="spec value"id="val-save_dotty_when_in_debug_mode"><ahref="#val-save_dotty_when_in_debug_mode"class="anchor"></a><code><spanclass="keyword">val</span> save_dotty_when_in_debug_mode : <ahref="../../IBase/SourceFile/index.html#type-t">IBase.SourceFile.t</a><span>-></span> unit</code></dt><dtclass="spec value"id="val-next_state_via_transition"><ahref="#val-next_state_via_transition"class="anchor"></a><code><spanclass="keyword">val</span> next_state_via_transition : <ahref="../Ctl_parser_types/index.html#type-ast_node">Ctl_parser_types.ast_node</a><span>-></span><ahref="../CTLTypes/index.html#type-transitions">CTLTypes.transitions</a><span>-></span><span><ahref="../Ctl_parser_types/index.html#type-ast_node">Ctl_parser_types.ast_node</a> list</span></code></dt><dtclass="spec value"id="val-create_ctl_evaluation_tracker"><ahref="#val-create_ctl_evaluation_tracker"class="anchor"></a><code><spanclass="keyword">val</span> create_ctl_evaluation_tracker : <ahref="../../IBase/SourceFile/index.html#type-t">IBase.SourceFile.t</a><span>-></span> unit</code></dt></dl></div></body></html>
