about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorCristian Cadar <cristic@cs.stanford.edu>2009-05-28 04:44:50 +0000
committerCristian Cadar <cristic@cs.stanford.edu>2009-05-28 04:44:50 +0000
commitd5e3206198cb3c7489a2ba817dfdd4fe6587e143 (patch)
tree1a86bcf568e4a13b2fdf91bd70bcde48dc56f718
parent14f53fcc478fe46e76240ce3ee920adda74ddcd5 (diff)
downloadklee-d5e3206198cb3c7489a2ba817dfdd4fe6587e143.tar.gz
Changes to webpage to make both tutorials use the same template.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72515 91177308-0d34-0410-b5e6-96231b3b80d8
-rw-r--r--examples/islower/islower.c (renamed from www/code-examples/demo.c)6
-rw-r--r--www/GetStarted.html2
-rw-r--r--www/Tutorial-1.html (renamed from www/tutorial-1.html)4
-rw-r--r--www/Tutorials.html (renamed from www/tutorials.html)3
-rw-r--r--www/menu.html.incl2
-rw-r--r--www/resources/islower.c.html33
6 files changed, 45 insertions, 5 deletions
diff --git a/www/code-examples/demo.c b/examples/islower/islower.c
index 2bf1c00d..ab85d072 100644
--- a/www/code-examples/demo.c
+++ b/examples/islower/islower.c
@@ -1,3 +1,9 @@
+/*
+ * First KLEE tutorial: testing a small function
+ */
+
+#include <klee/klee.h>
+
 int my_islower(int x) {
   if (x >= 'a' && x <= 'z')
     return 1;
diff --git a/www/GetStarted.html b/www/GetStarted.html
index 890510ab..5c445059 100644
--- a/www/GetStarted.html
+++ b/www/GetStarted.html
@@ -86,7 +86,7 @@ necessary, but KLEE runs very slowly in Debug mode).
     </div>
   </li>
 
-  <li>You're ready to go!  Go to the <a href="tutorials.html">Tutorials</a> page
+  <li>You're ready to go!  Go to the <a href="Tutorials.html">Tutorials</a> page
   to try KLEE.</li>
 </ol>
 
diff --git a/www/tutorial-1.html b/www/Tutorial-1.html
index 3f9bfc4e..833541d7 100644
--- a/www/tutorial-1.html
+++ b/www/Tutorial-1.html
@@ -27,7 +27,9 @@
       else return 0;
   } </pre>
 
-  You can find the entire code for this example <a href="code-examples/demo.c">here</a>. 
+  You can find the entire code for this example in the source tree
+  under <tt>examples/islower</tt>.  A version of the source code can
+  also be accessed <a href="resources/islower.c.html">here</a>. 
 
   <h2>Marking input as symbolic</h2> 
 
diff --git a/www/tutorials.html b/www/Tutorials.html
index 795c629e..21ca3f29 100644
--- a/www/tutorials.html
+++ b/www/Tutorials.html
@@ -16,8 +16,7 @@
   <!--*********************************************************************-->
 
   <ol>
-    <li><a href="tutorial-1.html">Tutorial One</a>: Using KLEE on a toy
-      example.</li>
+    <li><a href="Tutorial-1.html">Tutorial One</a>: Testing a small function.</li>
 
     <li><a href="Tutorial-2.html">Tutorial Two</a>: Testing a simple regular
       expression library.</li>
diff --git a/www/menu.html.incl b/www/menu.html.incl
index 1c15ab44..22d6e578 100644
--- a/www/menu.html.incl
+++ b/www/menu.html.incl
@@ -8,7 +8,7 @@
     <a href="index.html">About</a>
     <a href="GetStarted.html">Getting Started</a>
     <a href="GetInvolved.html">Get Involved</a>
-    <a href="tutorials.html">Tutorials</a>
+    <a href="Tutorials.html">Tutorials</a>
   </div>
 
   <div class="submenu">
diff --git a/www/resources/islower.c.html b/www/resources/islower.c.html
new file mode 100644
index 00000000..524f2093
--- /dev/null
+++ b/www/resources/islower.c.html
@@ -0,0 +1,33 @@
+<!DOCTYPE html PUBLIC "-//IETF//DTD HTML 2.0//EN">
+<HTML>
+<HEAD>
+<TITLE>Enscript Output</TITLE>
+</HEAD>
+<BODY BGCOLOR="#FFFFFF" TEXT="#000000" LINK="#1F00FF" ALINK="#FF0000" VLINK="#9900DD">
+<A NAME="top">
+<A NAME="file1">
+<H1>islower.c</H1>
+
+<PRE>
+<I><FONT COLOR="#B22222">/*
+ * First KLEE tutorial: testing a small function
+ */</FONT></I>
+
+#<B><FONT COLOR="#5F9EA0">include</FONT></B> <B><FONT COLOR="#BC8F8F">&lt;klee/klee.h&gt;</FONT></B>
+
+<B><FONT COLOR="#228B22">int</FONT></B> <B><FONT COLOR="#0000FF">my_islower</FONT></B>(<B><FONT COLOR="#228B22">int</FONT></B> x) {
+  <B><FONT COLOR="#A020F0">if</FONT></B> (x &gt;= <B><FONT COLOR="#BC8F8F">'a'</FONT></B> &amp;&amp; x &lt;= <B><FONT COLOR="#BC8F8F">'z'</FONT></B>)
+    <B><FONT COLOR="#A020F0">return</FONT></B> 1;
+  <B><FONT COLOR="#A020F0">else</FONT></B> <B><FONT COLOR="#A020F0">return</FONT></B> 0;
+}
+
+<B><FONT COLOR="#228B22">int</FONT></B> <B><FONT COLOR="#0000FF">main</FONT></B>() {
+  <B><FONT COLOR="#228B22">char</FONT></B> c;
+  klee_make_symbolic(&amp;c, <B><FONT COLOR="#A020F0">sizeof</FONT></B>(c), <B><FONT COLOR="#BC8F8F">&quot;input&quot;</FONT></B>);
+  <B><FONT COLOR="#A020F0">return</FONT></B> my_islower(c);
+}
+</PRE>
+<HR>
+<ADDRESS>Generated by <A HREF="http://www.iki.fi/~mtr/genscript/">GNU enscript 1.6.4</A>.</ADDRESS>
+</BODY>
+</HTML>