Skip to content
Snippets Groups Projects
Select Git revision
  • 8f7615bcc7e058f3301a90dd89e125545320f2ec
  • master default protected
  • klee
3 results

profiling_db_parser.py

Blame
  • 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
    //