Skip to content
Snippets Groups Projects
Select Git revision
  • f4c4df319bbfee584555f32ce2b697a3f2d8ee8d
  • master default protected
2 results

get_sign.c

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