Select Git revision
get_sign.c 3.64 KiB
/*
* First KLEE tutorial: testing a small function
* https://klee.github.io/tutorials/testing-function/
*/
#include <klee/klee.h>
int get_sign(int x)
{
if (x == 0)
return 0;
if (x < 0)
return -1;
else
return 1;
}
int main()
{
int a;
klee_make_symbolic(&a, sizeof(a), "a");
return get_sign(a);
}
// A) Compiling into LLVM bitcode
// > clang -emit-llvm -c get_sign.c
//
// Now you can run Klee on your generated bitcode.
//
// > klee get_sign.bc
//
// [your answer here]
//
// B) Inspecting the output
//
// > ls klee-last/
//
// [your answer here]
//
// C) Inspecting the generated test cases
//
// > ktest-tool klee-last/test000001.ktest
//
// What path in the code does this test represent?
//
// [your answer here]
//
// > ktest-tool klee-last/test000002.ktest
//
// What path in the code does this test represent?
//
// [your answer here]
// > ktest-tool klee-last/test000003.ktest
//
// What path in the code does this test represent?
//
// [your answer here]
//
// D) Replaying a test case
//
// Fist check that includes were installed:
// > ls /usr/local/include
// klee
//
// > ls /usr/local/lib
// klee libkleeRuntest.so libkleeRuntest.so.1.0
//
// If those are ok, then you can compile for replay:
//