Это как протестировать API с отслеживанием состояния с символическим выполнением кли?

Question

В настоящее время я тестирую несколько подходов к тестированию и фаззингу C API. В процессе я нашел KLEE , который запускает код символически, то есть пытается охватить все ветки, которые зависят от какого-то символического ввода, и проверяет всевозможные ошибки. Мне удалось заставить его работать, и теперь я спрашиваю, хорош ли мой подход или есть ли у него какие-то серьезные недостатки или проблемы.

Предположим, у нас есть следующий простой, но глючный API:

      #include <assert.h>

static int g_state;

void setState(int state) {
    g_state = state;
}

void run(void) {
    if (g_state == 123) {
        assert(0);
    }
}

Если установлено состояние а потом вызывается помещенное утверждение терпит неудачу.

Для этого я написал следующий символический тест с KLEE:

      #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;
}

При работе с KLEE последовательность вызовов, необходимая для срабатывания утверждения, находится почти сразу. Затем я попытался расширить API несколькими другими функциями и спрятал утверждение за комбинацией состояний. KLEE снова нашел заложенную ошибку, но, естественно, это заняло немного больше времени.

Так я могу эффективно использовать KLEE для проверки API? Или есть документация о лучшем подходе?