Slides for 4xxx.

[libguestfs-talks.git] / 2020-frama-c / 4870-range-init-spec.html

diff --git a/2020-frama-c/4870-range-init-spec.html b/2020-frama-c/4870-range-init-spec.html
new file mode 100644 (file)
index 0000000..a676f66
--- /dev/null
+++ b/2020-frama-c/4870-range-init-spec.html
@@ -0,0 +1,25 @@
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
+<link rel="stylesheet" href="style.css" type="text/css"/>
+<script src="code.js" type="text/javascript"></script>
+
+<h1>qemu range_init_nofail() spec</h1>
+
+<pre class="code">
+  /*@
+    requires \valid(range);
+    requires lob + (integer)size <= UINT64_MAX;
+    assigns *range;
+    behavior empty:
+      assumes lob > 0 && size == 0;
+      ensures empty_range(*range);
+    behavior non_empty:
+      assumes size > 0;
+      ensures range->lob == lob;
+      ensures size_of_bounds(lob, range->upb) == size;
+    behavior total:
+      assumes lob == 0 && size == 0;
+      ensures total_range(*range);
+    complete behaviors;
+    disjoint behaviors;
+   */
+</pre>