<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
