Select Git revision
profiling_db_parser.py
get_sign.c 4.52 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]
// KLEE: done: total instructions = 31
// KLEE: done: completed paths = 3
// KLEE: done: generated tests = 3
//
// B) Inspecting the output
//
// > ls klee-last/
//
// [your answer here]
// assembly.ll info messages.txt run.istats run.stats test000001.ktest test000002.ktest test000003.ktest warnings.txt
//
// C) Inspecting the generated test cases
//
// > ktest-tool klee-last/test000001.ktest
//
// What path in the code does this test represent?
//
// [The first: return 0]
//
// > ktest-tool klee-last/test000002.ktest
//
// What path in the code does this test represent?
//
// [The third: return 1]
//
// > ktest-tool klee-last/test000003.ktest
//
// What path in the code does this test represent?
//
// [The second: return -1]
//
// D) Replaying a test case
//
// Fist check that includes were installed:
// > ls /usr/local/include
// klee
//