diff options
| -rw-r--r-- | examples/islower/islower.c (renamed from www/code-examples/demo.c) | 6 | ||||
| -rw-r--r-- | www/GetStarted.html | 2 | ||||
| -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.incl | 2 | ||||
| -rw-r--r-- | www/resources/islower.c.html | 33 |
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"><klee/klee.h></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 >= <B><FONT COLOR="#BC8F8F">'a'</FONT></B> && x <= <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(&c, <B><FONT COLOR="#A020F0">sizeof</FONT></B>(c), <B><FONT COLOR="#BC8F8F">"input"</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> |