We are looking for volunteers to integrate and update the Doxygen documentation for KLEE via GitHub actions:

• https://github.com/marketplace/actions/doxygen-action
• https://github.com/marketplace/actions/github-pages-action

We should keep the documentation, particularly the build instructions, for old KLEE versions.

KLEE documentation points to a buildbot (http://vm-klee.doc.ic.ac.uk:55555/) that is not up and running anymore. Should we replace the link to TravisCI?

llvm-gcc is part of LLVM 2.9. Recommend wllvm or clang instead.

I try to reproduce the OSDI experiments: http://klee.github.io/docs/coreutils-experiments/
Unfortunately the link to the sandbox is no longer available: http://www.doc.ic.ac.uk/~cristic/klee/klee-cu-sandbox.html

Is there an alternative source?

Thanks in advance.

I built KLEE this morning from scratch and when following the process found that one of the links is dead.

http://klee.github.io/build-llvm34/ — "Build instructions with LLVM 3.4".

05 (Optional) Build libgtest:
…
$ curl -OL https://googletest.googlecode.com/files/gtest-1.7.0.zip

This URL no longer works.
I believe the correct URL (and please note the new file name) is https://github.com/google/googletest/archive/release-1.7.0.zip

Different versions / releases including the latest 1.8.0 (with which I did not attempt to build KLEE) can be found here: https://github.com/google/googletest/releases

All the rest of the process worked perfectly.

Thanks!

I was taking a look what the slug page attribute was doing. It looks kind of broken.

The file _includes/nav/main.html gives hints at what the intention was, e.g.

<nav class="navdrawer-container promote-layer" role="navigation">
  <h4>Navigation</h3>
  <ul>
    <li{% if page.slug == "getting-started" %} class="active"{% endif %}>
      <a href="{{ site.baseurl }}/getting-started">Getting Started</a>
    </li>
    <li{% if page.slug == "documentation" %} class="active"{% endif %}>
      <a href="{{ site.baseurl }}/docs">Documentation</a>
    </li>
    <li{% if page.slug == "tutorials" %} class="active"{% endif %}>
      <a href="{{ site.baseurl }}/tutorials">Tutorials</a>
    </li>
    <li{% if page.slug == "publications" %} class="active"{% endif %}>
      <a href="{{ site.baseurl }}/publications">Publications</a>
    </li>
    <li{% if page.slug == "projects" %} class="active"{% endif %}>
      <a href="{{ site.baseurl }}/projects">Projects</a>
    </li>
    <li{% if page.slug == "getting-involved" %} class="active"{% endif %}>
      <a href="{{ site.baseurl }}/getting-involved">Getting Involved</a>
    </li>
  </ul>
</nav>

There seem to be two problems with this

• We have incorrect named slugs for several pages (e.g. docs/coreutils-experiments.md)
• The active class isn't used properly in the CSS. The file css/main.scss has

.navdrawer-container ul li a:active {
  background-color: rgba(255, 255, 255, 0.4);
}

but to work (at least for chromium 46.0.2490.80) the CSS needs to be

.navdrawer-container ul li a.active {
  background-color: rgba(255, 255, 255, 0.4);
}

@ccadar @petrhosek Thoughts?

docs/developers-guide.md still refers to Autoconf/Automake.

Affected page: http://klee.github.io/docs/files/

Dead links:

1. http://stp.github.io/cvc-input-language/
2. http://www.smtlib.org

@delcypher , you created branches fix_build_ruby2.3.1 and klee_cmake_instructions, which look outdated to me. Are they still needed? If not, let's delete them.

In the "Miscellaneous" section, "Writing messages to standard error" subsection, the guide suggests to look at lib/Core/Common.h file, which does not exist in the codebase. Also, in the same section, in "Adding a command line option to a tool" subsection, the guide suggests to look at lib/core/Executor.cpp, which should probably be lib/Core/Executor.cpp

When I attempt to test a build on Ubuntu 14.04, I get the error

"/Release+Asserts/bin/klee: error while loading shared libraries: libstp.so.2.1: cannot open shared object file: No such file or directory"

This occurs even after running "sudo make install".

By adding "export LD_LIBRARY_PATH=.../stp-2.1.0/build/lib", however, I can run "make check" without any problems. Am I doing something wrong, or should this be a part of the build?

In addition, the current build instructions use "--with-stp=.../stp/install". When using the newer version of stp, however, now this option isn't even necessary as long as "sudo make install" is run inside stp/build and the LD_LIBRARY_PATH is set.

I was trying to experiment with the recent support for C++ exceptions (klee/klee#966) and noticed that the instructions at https://klee.github.io/build-llvm9/ are now incomplete. In particular, they don't discuss how to install libcxxabi.
@futile, @jbuening perhaps you can add this info? Thanks!

There is detailed documentation for -sym-files and -sym-stdin. However, for -sym-stdout, it only says that it will make stdout symbolic. However, it's unclear to me of what the implication of making stdout symbolic is.

Thanks

Problem: It is difficult for readers who don't know what a "dynamic symbolic execution engine" is to figure out what KLEE can do, what it is useful for, and whether or not they would benefit from using it.

Explanation The current header on http://klee.github.io/ reads:

KLEE is a dynamic symbolic execution engine built on top of the LLVM compiler infrastructure, and available under the UIUC open source license. For more information on what KLEE is and what it can do, see the OSDI 2008 paper.

At this point a reader (probably) knows KLEE is a programmer's tool. If they doen't know what a "Dynamic Symbolic Execution Engine" they have been encouraged to read a block of unstyled text which has a few helpful snippets buried in it:

We present a new symbolic execution tool, KLEE, capable of automatically generating tests that achieve high coverage on a diverse set of complex and environmentally-intensive programs.

We also used KLEE as a bug finding tool, applying it to 452 applications (over 430K total lines of code), where it found 56 serious bugs

This tells the reader that KLEE is a programmer's tool that generates tests to find bugs in code. From here, they can click through to a 16-page academic paper, which explains how KLEE works and describes a few case studies where it was used to find bugs in C code. This document is obviously not written for non-academic programmers, and does not readily answer "What can KLEE do for me?"

Going back to http://klee.github.io/, there are several other prevalent and possibly-helpful-sounding links:

• Getting Started and Documentation describe how to install, run, and use KLEE, but assume the reader already know they want to do these things.
• Tutorials, the first of which says that KLEE will "exercise all paths through the code" in a simple C program, and that the program runs "as expected". Most of the tutorials are hosted on other websites and written by other people.
• Projects, a list of ongoing improvements to KLEE. This page does helpfully list some things KLEE doesn't currently work with.
• Getting Involved is for people who want to become KLEE developers, not KLEE users.
• Run small examples in your browser. All three examples are in C. The first example finds no bugs. The second example prints (at the bottom of 6578 warnings!) two memory error on line XXs with no further explanation about what kind of errors these are.

Proposed Solution Compose a description of what KLEE does and is useful for, and either include it on http://klee.github.io/, or on a page which is prominently linked there.

There is no link to https://klee.github.io/ on the main page of this repository.

We should update documentation accordingly according to @delcypher 's comment in klee/klee#336 (comment).

When looking at the Developer's Guide I came across an issue that seems to stem from some incorrect markdown:

As visible in the attachment:

• there's a stray </tt> in the text
• the final word is not rendered as a link because the bracketing is back to front

Please let me know if it's unclear what I'm referring to here.

Hello,

The step 7 of Building KLEE with LLVM 13 doc suggests to use -DKLEE_LIBCXX_INCLUDE_DIR=<LIBCXX_DIR>/libc++-install-130/include/c++/v1/

Wouldn't it better to suggest -DKLEE_LIBCXX_INCLUDE_DIR=<LIBCXX_DIR>/libc++-install-130/ ? So that KLEE_LIBCXX_PLATFORM_INCLUDE_PATH can be set properly as well as KLEE_LIBCXX_INCLUDE_PATH ?

Hi KLEE,

I was struggling a little with the introductory documentation (tutorials 1 and 2) because I was expecting clang to generate an .o object file. The tutorial asks to run clang and then to run klee.o

@andreamattavelli helped me to realize that the .bc files (a format with which I was confused) were really the ones to run klee on.

The tutorial mentions clang and then suggests:
klee get_sign.o

This might leave someone confused and looking for an object file.

Thanks!

Following the current build instructions on 64 bit linux results in a klee that terminates all states when memory use exceeds 2G. Since the default memory threshold is 2000 MB, that leaves a very narrow 48K window to avoid the error. The solution (as documented elsewhere here) is to use tcmalloc. Mentioning that in the build instructions would have saved me several days of troubleshooting :)

I looked at the "intro box" issue but couldn't come up with a sufficient solution. We should think about re-structuring the page. I'd suggest to merge tutorials and documentation and use different sections on a single page (development, installation, usage, ...).

Hi @251 would it be possible to create a banner advertising the upcoming workshop, similar to the one you did for KLEE 2018?

It's happened again! #29 should definitely have been closed years back, so this isn't exactly a duplicate.

The current doxygen link in the page footer (the same one as was recommended in #29 5 years ago) is now 404ing. Not sure who's managing it now, but I figured this might be the best place to start.

To build STP it is necessary to build Minisat, however the following command is not correct:

$ cmake -DSTATICCOMPILE=ON -DCMAKE_INSTALL_PREFIX=/usr/ ../

In fact, -DSTATICCOMPILE=ON is valid only in CryptoMinisat. We should think if we want to move to CryptoMinisat or remove the extra argument.

Building doesn't require dejagnu or subversion any more.

We now need cmake, git and python.

From the KLEE mailing list: Marko Dimjašević

https://klee.github.io/docs/developers-guide/
there's a link in the Building code documentation section leading to:
http://test.minormatter.com/~ddunbar/klee-doxygen/index.html
When I follow that link, I get a "Server not found" error.

The current documentation suggests to install STP 2.1.0 for compiling KLEE on LLVM 2.9. For LLVM 3.4, instead, the documentation suggests to use the STP version from the master branch on git (currently 2.1.2).
Is there any reason for this? That is, is there any known bug for KLEE on LLVM 2.9 and STP 2.1.2?
I'm asking this because I've observed that STP 2.1.2 has better performances.

We should think about how to re-structure the documentation. First, we should remove the build instructions for LLVM 2.9, and then decide how to include experimental support for newer LLVM versions in the build instructions.

Hi @petrhosek , I noticed you hard coded the numbers in /publications, which were automatically generated in HTML. What's the best way to replicate

...

Our documentation including tutorials, etc. assumes LLVM 2.9 is used. Since now LLVM 3.4 is the recommended version, we should update the documentation accordingly.

In build-llvm3.4md, http://llvm.org/apt/ is suggested as a source for LLVM 3.4.

http://llvm.org/apt/ does not contain any releases older than LLVM 3.8 for Xenial.

For new distributions (such as Ubuntu 16.04.1 LTS), which LLVM repository should we use?

dave@pc5:/mnt/bitcoder$ sudo apt-get update -o Dir::Etc::sourcelist="sources.list.d/llvm.list"
Hit:1 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.8 InRelease
Ign:2 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7 InRelease
Ign:3 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4 InRelease
Ign:4 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7 Release
Ign:5 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4 Release
Ign:6 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main Sources
Ign:7 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main amd64 Packages
Ign:8 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main all Packages
Ign:9 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main Translation-en_US
Ign:10 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main Translation-en
Ign:11 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main Sources
Hit:12 https://apt.dockerproject.org/repo ubuntu-xenial InRelease
Ign:13 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main amd64 Packages
Ign:14 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main all Packages
Ign:15 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main Translation-en_US
Ign:16 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main Translation-en
Ign:6 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main Sources
Ign:7 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main amd64 Packages
Ign:8 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main all Packages
Ign:9 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main Translation-en_US
Ign:10 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main Translation-en
Ign:11 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main Sources
Ign:13 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main amd64 Packages
Ign:14 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main all Packages
Ign:15 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main Translation-en_US
Ign:16 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main Translation-en
Ign:6 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main Sources
Ign:7 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main amd64 Packages
Ign:8 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main all Packages
Ign:9 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main Translation-en_US
Ign:10 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main Translation-en
Ign:11 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main Sources
Ign:13 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main amd64 Packages
Ign:14 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main all Packages
Ign:15 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main Translation-en_US
Ign:16 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main Translation-en
Ign:6 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main Sources
Ign:7 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main amd64 Packages
Ign:8 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main all Packages
Ign:9 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main Translation-en_US
Ign:10 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main Translation-en
Ign:11 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main Sources
Ign:13 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main amd64 Packages
Ign:14 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main all Packages
Ign:15 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main Translation-en_US
Ign:16 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main Translation-en
Ign:6 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main Sources
Ign:7 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main amd64 Packages
Ign:8 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main all Packages
Ign:9 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main Translation-en_US
Ign:10 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main Translation-en
Ign:11 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main Sources
Ign:13 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main amd64 Packages
Ign:14 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main all Packages
Ign:15 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main Translation-en_US
Ign:16 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main Translation-en
Err:6 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main Sources
  404  Not Found
Ign:7 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main amd64 Packages
Ign:8 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main all Packages
Ign:9 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main Translation-en_US
Ign:10 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7/main Translation-en
Err:11 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main Sources
  404  Not Found
Ign:13 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main amd64 Packages
Ign:14 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main all Packages
Ign:15 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main Translation-en_US
Ign:16 http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4/main Translation-en
Reading package lists... Done
W: The repository 'http://apt.llvm.org/xenial llvm-toolchain-xenial-3.7 Release' does not have a Release file.
N: Data from such a repository can't be authenticated and is therefore potentially dangerous to use.
N: See apt-secure(8) manpage for repository creation and user configuration details.
W: The repository 'http://apt.llvm.org/xenial llvm-toolchain-xenial-3.4 Release' does not have a Release file.
N: Data from such a repository can't be authenticated and is therefore potentially dangerous to use.
N: See apt-secure(8) manpage for repository creation and user configuration details.
E: Failed to fetch http://apt.llvm.org/xenial/dists/llvm-toolchain-xenial-3.7/main/source/Sources  404  Not Found
E: Failed to fetch http://apt.llvm.org/xenial/dists/llvm-toolchain-xenial-3.4/main/source/Sources  404  Not Found
E: Some index files failed to download. They have been ignored, or old ones used instead.

We should add instructions for these versions, perhaps by generalizing the existing ones if possible.