title: Is this how to test a stateful API with klee symbolic execution?
body: <p>I'm currently testing out a few approaches on how to test and fuzz a C API. In the process thereof I found <a href="https://klee.github.io/" rel="nofollow noreferrer">KLEE</a> which runs the code symbolically, meaning that it tries to cover all branches that depend on some symbolic input and checks for all sorts of errors. I managed to get it to work and am now asking if my approach is good or if it has some major drawbacks or problems.</p>
  <p>Let's suppose we have following simple but buggy API:</p>
  <pre class="lang-c prettyprint-override"><code>#include &lt;assert.h&gt;
  
  static int g_state;
  
  void setState(int state) {
      g_state = state;
  }
  
  void run(void) {
      if (g_state == 123) {
          assert(0);
      }
  }
  </code></pre>
  <p>If the state is set to <code>123</code> and then <code>run()</code> is invoked the placed assertion fails.</p>
  <p>For this I have written following symbolic test with KLEE:</p>
  <pre class="lang-c prettyprint-override"><code>#include &quot;klee/klee.h&quot;
  #include &quot;buggy_api.h&quot;
  
  int main(void) {
      for (int i = 0; i &lt; 2; ++i) { // sequentially call 2 APIs
          int f_select = klee_choose(2); // what API to call
          if (f_select == 0) {
              int state = 0;
              klee_make_symbolic(&amp;state, sizeof(state), &quot;state&quot;);
              setState(state);
          } else if (f_select == 1) {
              run();
          }
      }
      return 0;
  }
  </code></pre>
  <p>When running with KLEE, the sequence of calls necessary to trigger the assertion is found almost immediately. I then tried to extend the API with a few other functions and hid the assertion behind a combination of states. KLEE again found the planted bug but naturally took a bit longer.</p>
  <p>Is this how I can efficiently use KLEE for checking an API? Or is there documentation about a better approach?</p>