Hi,
On Mon, 2 May 2022 09:50:23 +0200 Niklaus Leuenberger <niklaus.leu...@gmail.com> wrote: > For this I have written following KLEE harness: > --- > #include "klee/klee.h" > #include "buggy_api.h" > int main(void) { > for (int i = 0; i < 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(&state, sizeof(state), "state"); > setState(state); > } else if (f_select == 1) { > run(); > } > } > return 0; > } What I find a little odd here is that you drop the constraints of the global state every time you get f_select == 0. Is this supposed to be a reset and if so, would everything afterwards not be covered by a similar path starting from the initial state? > When running with KLEE, the sequence of calls necessary to trigger the > assertion is found almost immediately. But when extending it with more > functions, each doubles the runtime. So it scales rather poorly on > larger APIs. > Is this how I can use KLEE for checking an API? Or does someone have > pointers to a better approach? Hard to give recommendations without more knowledge about the problem. In general: KLEE tries to execute all paths - if your program has a lot of paths, than that's the issue. ;) You can also play with KLEE's flags, e.g. disable test generation (--write-no-tests) or use a less expensive search strategy (--search=[dfs,bfs,random-state]). You can also check KLEE's stats to see where it spends time or branches heavily, see: https://klee.github.io/tutorials/testing-coreutils/ (Step 6). Kind regards, Frank _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev