Can symcc cover all the paths in one run?

[harperchen]

Hi developers, for the following C program,

#include <unistd.h>

static int32_t g_1 = 10;
static int32_t g_2 = -1;

static int32_t func_1(void)
{
    if (g_2 == 0) {
        return 0;
    }
    if (g_1 < 0) {
        return -1;
    }
    else {
        return 1;
    }
}

int main (int argc, char* argv[])
{
    read(STDIN_FILENO, &g_1, sizeof(g_1));
    read(STDIN_FILENO, &g_2, sizeof(g_2));
    func_1();
    return 0;
}

If I feed g_1=10 and g_2=-1 to the instrumented executable, will symcc find the inputs for all three paths in one run?

• g_2 == 0
• g_2 =/= 0 and g_1 < 0
• g_2 =/= 0 and g_1 >= 0

or do I need to recursively run the instrumented executable until no new input is generated?

[aurelf]

Hi harperchen, no currently there is no exploration of all possible states. Current SymCC follows a concolic approach (always follow the concrete path). However, this would be possible, with some important changes. This has been discussed in the past in issue #14, please use that issue to track this. Patches welcome of course !