Opened 7 weeks ago

#117 new feature

Possibility of symbolic argc + argv

Reported by: Lukáš Zaoral Owned by: mornfall
Priority: major Milestone: 4.5
Component: other Keywords:
Cc: kdudka@…, lzaoral@…

Description

At the moment, Divine models the contents of argc and argv only by its own concrete arguments. It would be useful if it could handle these as symbolic variables as well so that the assertion in the following code snippet would be reachable even when executed as divine check test.c (maybe with some additional flag to toggle this behaviour).

#include <assert.h>

int main(int argc, char** argv)
{
    if (argc == 2)
        assert(0);
}

Change History (0)

Note: See TracTickets for help on using tickets.