Skip to content

Commit

Permalink
Deploying to gh-pages from @ 6b5e688 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
AdarshRawat1 committed Oct 1, 2024
1 parent ac46fd3 commit d22d147
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 11 deletions.
11 changes: 0 additions & 11 deletions pr-preview/4919/ebpf_backend.html
Original file line number Diff line number Diff line change
Expand Up @@ -173,15 +173,6 @@
<li class="level4">
<a href="#translating-match-action-pipelines">Translating match-action pipelines</a>
</li>
</ul>
</li>
</ul>
</li>
<li class="level2">
<a href="#autotoc_md0">autotoc_md0</a>
<ul>
<li class="level3 empty">
<ul>
<li class="level4">
<a href="#generating-code-from-a-p4-file">Generating code from a .p4 file</a>
</li>
Expand Down Expand Up @@ -497,8 +488,6 @@ <h4><a class="anchor" id="translating-parsers"></a>
</table>
<h4><a class="anchor" id="translating-match-action-pipelines"></a>
Translating match-action pipelines</h4>
<h2><a class="anchor" id="autotoc_md0"></a>
autotoc_md0</h2>
<table class="markdownTable">
<tr class="markdownTableHead">
<th class="markdownTableHeadNone">P4 Construct </th><th class="markdownTableHeadNone">C Translation </th></tr>
Expand Down
2 changes: 2 additions & 0 deletions pr-preview/4919/p4testgen.html
Original file line number Diff line number Diff line change
Expand Up @@ -287,6 +287,7 @@ <h3><a class="anchor" id="generating-specific-tests"></a>
<h4><a class="anchor" id="restricted-tests"></a>
Restricted Tests</h4>
<p><code>testgen_assume(expr)</code> will add <code>expr</code> as a necessary path constraints to all subsequent execution. For example, for the following snippet </p><div class="fragment"><div class="line"> P4</div>
<div class="line"> </div>
<div class="line">state parse_ethernet {</div>
<div class="line"> packet.extract(headers.ethernet);</div>
<div class="line"> testgen_assume(headers.ethernet.ether_type == 0x800);</div>
Expand All @@ -300,6 +301,7 @@ <h4><a class="anchor" id="restricted-tests"></a>
<h4><a class="anchor" id="finding-assertion-violations"></a>
Finding Assertion Violations</h4>
<p>Conversely, <code>testgen_assert(expr)</code> can be used to find violations in a particular P4 program. By default, <code>testgen_assert</code> behaves like <code>testgen_assume</code>. If the flag <code>--assertion-mode</code> is enabled, P4Testgen will only generate tests that will cause <code>expr</code> to be false and, hence, violate the assertion. For example, for </p><div class="fragment"><div class="line"> P4</div>
<div class="line"> </div>
<div class="line">state parse_ethernet {</div>
<div class="line"> packet.extract(headers.ethernet);</div>
<div class="line"> transition select(headers.ethernet.ether_type) {</div>
Expand Down

0 comments on commit d22d147

Please sign in to comment.