<p>The <code>requires</code> (here, something like <code>\valid(foo)</code> clause means exactly that: from the point of view of the callee, it is something it can assume, since it is up to the caller (or in the particular case of the main entry point, the outside world) to guarantee that the execution of the function will start in a state that respects the pre-condition.</p>
<p>However, in your particular case, there's a catch: for technical reasons, Eva does create an initial context first, and then reduce it according to the pre-condition. Hence, you'll get a warning that the <code>requires</code> is unknown.</p>
<p>Generally speaking, the usual way to let Eva start in a specific context is to write a small wrapper function, potentially using the built-ins mentioned in section 9.2.1 of the <a href="http://frama-c.com/download/eva-manual-21.1-Scandium.pdf" rel="nofollow noreferrer">Eva manual</a>. There are also a few options (described in section 6.3 of the manual) that control the way the initial state is computed. If you don't need too precise information about the initial state, they might be sufficient (e.g. too just ensure that <code>foo</code> and any other pointer is valid, use <code>-eva-context-valid-pointers</code>)</p>
<p>Finally, there have been experiments on generating a wrapper function from ACSL requires clause (see <a href="https://arxiv.org/abs/1709.04497" rel="nofollow noreferrer">this paper</a>), but as far as I know the corresponding plug-in is not freely available.</p>
How do you tell Frama-C and Eva that an entry point's parameters are assumed valid?
<p>Take the following C code example.</p>
<pre class="lang-c prettyprint-override"><code>struct foo_t {
    int bar;
};

int my_entry_point(const struct foo_t *foo) {
    return foo-&gt;bar;
}
</code></pre>
<p>In our case, <code>my_entry_point</code> will be called from assembly, and <code>*foo</code> here must be assumed to always be correct.</p>
<p>Running with the command line...</p>
<pre><code>frama-c -eva -report -report-classify -report-unclassified-warning ERROR -c11 -main my_entry_point /tmp/test.c
</code></pre>
<p>... results in ...</p>
<pre><code>[report] Monitoring events
[kernel] Parsing /tmp/override.c (with preprocessing)
[eva] Analyzing a complete application starting at my_entry_point
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization

[eva:alarm] /tmp/override.c:6: Warning:
  out of bounds read. assert \valid_read(&amp;foo-&gt;bar);
[eva] done for function my_entry_point
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function my_entry_point:
  __retres ∈ [--..--]
[eva:summary] ====== ANALYSIS SUMMARY ======
  ----------------------------------------------------------------------------
  1 function analyzed (out of 1): 100% coverage.
  In this function, 2 statements reached (out of 2): 100% coverage.
  ----------------------------------------------------------------------------
  No errors or warnings raised during the analysis.
  ----------------------------------------------------------------------------
  1 alarm generated by the analysis:
       1 invalid memory access
  ----------------------------------------------------------------------------
  No logical properties have been reached by the analysis.
  ----------------------------------------------------------------------------
[report] Classification
[ERROR:eva.unclassified.warning] Unclassified Warning (Plugin 'eva')
[REVIEW:unclassified.unknown] my_entry_point_assert_Eva_mem_access
[report] Reviews     :    1
[report] Errors      :    1
[report] Unclassified:    2
[report] User Error: Classified errors found
[kernel] Plug-in report aborted: invalid user input.
</code></pre>
<p>Of course, we can always add a base-case <code>NULL</code> check, which satisfies the checker (this is probably how we'll solve this for now, anyway).</p>
<pre class="lang-c prettyprint-override"><code>if (!foo) return 0;
</code></pre>
<p>But I'm more curious (for learning purposes) about how this might be done with e.g. ACSL annotations telling the checker &quot;hey, we understand this is pointer could, in theory, be invalid - however, please assume that, since it's the entry point, it is indeed valid&quot;.</p>
<p>Is this something that ACSL supports, or can the behavior be altered via command line arguments to <code>frama-c</code>? I can see why the standards committee might be hesitant on adding such a mechanism to ACSL since it could be abused, but seeing as how I'm just learning ACSL I was curious to know what the common approach might be here.</p>