From b405f4dc4866c8c12a57437a0a1ba3d23f9711fe Mon Sep 17 00:00:00 2001
From: Cristian Cadar <cristic@cs.stanford.edu>
Date: Tue, 7 May 2013 12:44:49 +0000
Subject: Patch by Dan Liew: "Added examples of using updates in KQuery
 documentation."

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@181310 91177308-0d34-0410-b5e6-96231b3b80d8
---
 www/KQuery.html | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/www/KQuery.html b/www/KQuery.html
index 15fbfdf7..a40f4435 100644
--- a/www/KQuery.html
+++ b/www/KQuery.html
@@ -186,7 +186,10 @@
 
   <p><b>Examples:</b></p>
   <div class="example">
-    (Add w32 N0:(Add w32 1 1) N0) <font color="Red"># Four</font>
+    (Add w32 N0:(Add w32 1 1) N0) <font color="Red"># Four</font><br><br>
+    array const_array[] : w32 -> w8 = [5,6]<br>
+    (Read w8 0 U0:[0=255] @ const_array) <font color="Red"># U0 now refers to an array [255,6]</font><br>
+    (Read w8 1 U0) <font color="Red"># Read from byte offset 1 of [255,6]</font><br>
   </div>
 
   <h2><a name="literals">Literals</a></h2>
@@ -329,6 +332,13 @@
     update-list = lhs-expression "=" rhs-expression [ "," update-list ]<br>
   </div>
 
+  <p><b>Examples:</b></p>
+  <div class="example">
+    array small_array[2] : w32 -> w8 = symbolic <font color="Red"># The array we will read from</font><br>
+    <br>
+    (Read w8 0 thing) <font color="Red"># No Updates to small_array</font><br>
+    (Read w8 1 [1=0xff] @ small_array) <font color="Red"># Read from small_array at byte offset 1 with update where byte 1 set to decimal 255</font><br>
+  </div>
   <p>A version can be specified either by an identifier, which can refer to an
   array or a <a href="#expr_labels">labelled version</a>, or by an explicit list
   of writes which are to be concatenated to another version (the most recent
-- 
cgit 1.4.1