X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=2020-frama-c%2F2820-range-init-spec.html;fp=2020-frama-c%2F2820-range-init-spec.html;h=a676f66a8ba13434106c043452c9400e6baa9dac;hb=6d2dcd916aa3e435d1f8ce691127bd891fc3c69a;hp=0000000000000000000000000000000000000000;hpb=a44fc27c4a4b02ed570dd5567ff8d309b885e904;p=libguestfs-talks.git

diff --git a/2020-frama-c/2820-range-init-spec.html b/2020-frama-c/2820-range-init-spec.html
new file mode 100644
index 0000000..a676f66
--- /dev/null
+++ b/2020-frama-c/2820-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>