<!DOCTYPE html> <html xmlns="http://www.w3.org/1999/xhtml"><head><title>PulseOperations (infer.Pulselib.PulseOperations)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.1"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../index.html">infer</a> » <a href="../index.html">Pulselib</a> » PulseOperations</nav><h1>Module <code>Pulselib.PulseOperations</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../PulseAbductiveDomain/index.html#type-t">PulseDomainInterface.AbductiveDomain.t</a></code></dt><dt class="spec type" id="type-access_result"><a href="#type-access_result" class="anchor"></a><code><span class="keyword">type</span> <span>'a access_result</span></code><code> = <span><span>(<span class="type-var">'a</span>, <a href="../PulseDiagnostic/index.html#type-t">PulseBasicInterface.Diagnostic.t</a> * <a href="index.html#type-t">t</a>)</span> <a href="../../IStdlib/index.html#module-IStd">IStdlib.IStd</a>.result</span></code></dt></dl><dl><dt class="spec value" id="val-ok_continue"><a href="#val-ok_continue" class="anchor"></a><code><span class="keyword">val</span> ok_continue : <a href="index.html#type-t">t</a> <span>-></span> <span><span>(<span><a href="../PulseExecutionDomain/index.html#type-t">PulseDomainInterface.ExecutionDomain.t</a> list</span>, <span class="type-var">'a</span>)</span> <a href="../../IStdlib/index.html#module-IStd">IStdlib.IStd</a>.result</span></code></dt><dt class="spec value" id="val-check_addr_access"><a href="#val-check_addr_access" class="anchor"></a><code><span class="keyword">val</span> check_addr_access : <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>-></span> <span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <span><a href="index.html#type-t">t</a> <a href="index.html#type-access_result">access_result</a></span></code></dt><dd><p>Check that the <code>address</code> is not known to be invalid</p></dd></dl><div class="spec module" id="module-Closures"><a href="#module-Closures" class="anchor"></a><code><span class="keyword">module</span> <a href="Closures/index.html">Closures</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><dl><dt class="spec value" id="val-eval"><a href="#val-eval" class="anchor"></a><code><span class="keyword">val</span> eval : <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>-></span> <a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <span><span>(<a href="index.html#type-t">t</a> * <span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span>)</span> <a href="index.html#type-access_result">access_result</a></span></code></dt><dd><p>Use the stack and heap to evaluate the given expression down to an abstract address representing its value.</p><p>Return an error state if it traverses some known invalid address or if the end destination is known to be invalid.</p></dd></dl><dl><dt class="spec value" id="val-prune"><a href="#val-prune" class="anchor"></a><code><span class="keyword">val</span> prune : <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>-></span> <span>condition:<a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a></span> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <span><a href="index.html#type-t">t</a> <a href="index.html#type-access_result">access_result</a></span></code></dt><dt class="spec value" id="val-eval_deref"><a href="#val-eval_deref" class="anchor"></a><code><span class="keyword">val</span> eval_deref : <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>-></span> <a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <span><span>(<a href="index.html#type-t">t</a> * <span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span>)</span> <a href="index.html#type-access_result">access_result</a></span></code></dt><dd><p>Like <code>eval</code> but evaluates <code>*exp</code>.</p></dd></dl><dl><dt class="spec value" id="val-eval_access"><a href="#val-eval_access" class="anchor"></a><code><span class="keyword">val</span> eval_access : <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>-></span> <span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span> <span>-></span> <a href="../../Pulselib__PulseBaseMemory/index.html#module-Access">Pulselib.PulseDomainInterface.BaseMemory.Access</a>.t <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <span><span>(<a href="index.html#type-t">t</a> * <span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span>)</span> <a href="index.html#type-access_result">access_result</a></span></code></dt><dd><p>Like <code>eval</code> but starts from an address instead of an expression, checks that it is valid, and if so dereferences it according to the access.</p></dd></dl><dl><dt class="spec value" id="val-havoc_id"><a href="#val-havoc_id" class="anchor"></a><code><span class="keyword">val</span> havoc_id : <a href="../../IR/Ident/index.html#type-t">IR.Ident.t</a> <span>-></span> <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-havoc_field"><a href="#val-havoc_field" class="anchor"></a><code><span class="keyword">val</span> havoc_field : <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>-></span> <span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span> <span>-></span> <a href="../../IR/Fieldname/index.html#type-t">IR.Fieldname.t</a> <span>-></span> <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <span><a href="index.html#type-t">t</a> <a href="index.html#type-access_result">access_result</a></span></code></dt><dt class="spec value" id="val-realloc_pvar"><a href="#val-realloc_pvar" class="anchor"></a><code><span class="keyword">val</span> realloc_pvar : <a href="../../IR/Pvar/index.html#type-t">IR.Pvar.t</a> <span>-></span> <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-write_id"><a href="#val-write_id" class="anchor"></a><code><span class="keyword">val</span> write_id : <a href="../../IR/Ident/index.html#type-t">IR.Ident.t</a> <span>-></span> <span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-write_field"><a href="#val-write_field" class="anchor"></a><code><span class="keyword">val</span> write_field : <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>-></span> <span>ref:<span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span></span> <span>-></span> <a href="../../IR/Fieldname/index.html#type-t">IR.Fieldname.t</a> <span>-></span> <span>obj:<span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span></span> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <span><a href="index.html#type-t">t</a> <a href="index.html#type-access_result">access_result</a></span></code></dt><dd><p>write the edge <code>ref --.field--> obj</code></p></dd></dl><dl><dt class="spec value" id="val-write_arr_index"><a href="#val-write_arr_index" class="anchor"></a><code><span class="keyword">val</span> write_arr_index : <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>-></span> <span>ref:<span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span></span> <span>-></span> <span>index:<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a></span> <span>-></span> <span>obj:<span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span></span> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <span><a href="index.html#type-t">t</a> <a href="index.html#type-access_result">access_result</a></span></code></dt><dd><p>write the edge <code>ref[index]--> obj</code></p></dd></dl><dl><dt class="spec value" id="val-write_deref"><a href="#val-write_deref" class="anchor"></a><code><span class="keyword">val</span> write_deref : <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>-></span> <span>ref:<span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span></span> <span>-></span> <span>obj:<span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span></span> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <span><a href="index.html#type-t">t</a> <a href="index.html#type-access_result">access_result</a></span></code></dt><dd><p>write the edge <code>ref --*--> obj</code></p></dd></dl><dl><dt class="spec value" id="val-invalidate"><a href="#val-invalidate" class="anchor"></a><code><span class="keyword">val</span> invalidate : <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>-></span> <a href="../PulseInvalidation/index.html#type-t">PulseBasicInterface.Invalidation.t</a> <span>-></span> <span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <span><a href="index.html#type-t">t</a> <a href="index.html#type-access_result">access_result</a></span></code></dt><dd><p>record that the address is invalid</p></dd></dl><dl><dt class="spec value" id="val-allocate"><a href="#val-allocate" class="anchor"></a><code><span class="keyword">val</span> allocate : <a href="../../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>-></span> <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>-></span> <span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-add_dynamic_type"><a href="#val-add_dynamic_type" class="anchor"></a><code><span class="keyword">val</span> add_dynamic_type : <a href="../../IR/Typ/Name/index.html#type-t">IR.Typ.Name.t</a> <span>-></span> <a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-remove_allocation_attr"><a href="#val-remove_allocation_attr" class="anchor"></a><code><span class="keyword">val</span> remove_allocation_attr : <a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-invalidate_access"><a href="#val-invalidate_access" class="anchor"></a><code><span class="keyword">val</span> invalidate_access : <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>-></span> <a href="../PulseInvalidation/index.html#type-t">PulseBasicInterface.Invalidation.t</a> <span>-></span> <span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span> <span>-></span> <a href="../../Pulselib__PulseBaseMemory/index.html#module-Access">Pulselib.PulseDomainInterface.BaseMemory.Access</a>.t <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <span><a href="index.html#type-t">t</a> <a href="index.html#type-access_result">access_result</a></span></code></dt><dd><p>record that what the address points via the access to is invalid</p></dd></dl><dl><dt class="spec value" id="val-invalidate_array_elements"><a href="#val-invalidate_array_elements" class="anchor"></a><code><span class="keyword">val</span> invalidate_array_elements : <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>-></span> <a href="../PulseInvalidation/index.html#type-t">PulseBasicInterface.Invalidation.t</a> <span>-></span> <span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <span><a href="index.html#type-t">t</a> <a href="index.html#type-access_result">access_result</a></span></code></dt><dd><p>record that all the array elements that address points to is invalid</p></dd></dl><dl><dt class="spec value" id="val-shallow_copy"><a href="#val-shallow_copy" class="anchor"></a><code><span class="keyword">val</span> shallow_copy : <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>-></span> <span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <span><span>(<a href="index.html#type-t">t</a> * <span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span>)</span> <a href="index.html#type-access_result">access_result</a></span></code></dt><dd><p>returns the address of a new cell with the same edges as the original</p></dd></dl><dl><dt class="spec value" id="val-get_dynamic_type_unreachable_values"><a href="#val-get_dynamic_type_unreachable_values" class="anchor"></a><code><span class="keyword">val</span> get_dynamic_type_unreachable_values : <span><a href="../../IR/Var/index.html#type-t">IR.Var.t</a> list</span> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <span><span>(<a href="../../IR/Var/index.html#type-t">IR.Var.t</a> * <a href="../../IR/Typ/Name/index.html#type-t">IR.Typ.Name.t</a>)</span> list</span></code></dt><dd><p>Given a list of variables, computes the unreachable values if the variables were removed from the stack, then return the dynamic types of those values if they are available</p></dd></dl><dl><dt class="spec value" id="val-remove_vars"><a href="#val-remove_vars" class="anchor"></a><code><span class="keyword">val</span> remove_vars : <span><a href="../../IR/Var/index.html#type-t">IR.Var.t</a> list</span> <span>-></span> <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <span><a href="index.html#type-t">t</a> <a href="index.html#type-access_result">access_result</a></span></code></dt><dt class="spec value" id="val-check_address_escape"><a href="#val-check_address_escape" class="anchor"></a><code><span class="keyword">val</span> check_address_escape : <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>-></span> <a href="../../IR/Procdesc/index.html#type-t">IR.Procdesc.t</a> <span>-></span> <a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> <span>-></span> <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <span><a href="index.html#type-t">t</a> <a href="index.html#type-access_result">access_result</a></span></code></dt><dt class="spec value" id="val-call"><a href="#val-call" class="anchor"></a><code><span class="keyword">val</span> call : <span>caller_proc_desc:<a href="../../IR/Procdesc/index.html#type-t">IR.Procdesc.t</a></span> <span>-></span> <span>callee_data:<span><span>(<a href="../../IR/Procdesc/index.html#type-t">IR.Procdesc.t</a> * <a href="../PulseSummary/index.html#type-t">PulseSummary.t</a>)</span> option</span></span> <span>-></span> <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>-></span> <a href="../../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>-></span> <span>ret:<span>(<a href="../../IR/Ident/index.html#type-t">IR.Ident.t</a> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span></span> <span>-></span> <span>actuals:<span><span>(<span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span> list</span></span> <span>-></span> <span>formals_opt:<span><span><span>(<a href="../../IR/Pvar/index.html#type-t">IR.Pvar.t</a> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span> list</span> option</span></span> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <span><span><a href="../PulseExecutionDomain/index.html#type-t">PulseDomainInterface.ExecutionDomain.t</a> list</span> <a href="index.html#type-access_result">access_result</a></span></code></dt><dd><p>perform an interprocedural call: apply the summary for the call proc name passed as argument if it exists</p></dd></dl><dl><dt class="spec value" id="val-unknown_call"><a href="#val-unknown_call" class="anchor"></a><code><span class="keyword">val</span> unknown_call : <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>-></span> <a href="../PulseCallEvent/index.html#type-t">PulseBasicInterface.CallEvent.t</a> <span>-></span> <span>ret:<span>(<a href="../../IR/Ident/index.html#type-t">IR.Ident.t</a> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span></span> <span>-></span> <span>actuals:<span><span>(<span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span> list</span></span> <span>-></span> <span>formals_opt:<span><span><span>(<a href="../../IR/Pvar/index.html#type-t">IR.Pvar.t</a> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span> list</span> option</span></span> <span>-></span> <a href="index.html#type-t">t</a> <span>-></span> <a href="index.html#type-t">t</a></code></dt><dd><p>performs a call to a function with no summary by optimistically havoc'ing the by-ref actuals and the return value as appropriate</p></dd></dl></div></body></html>