Possibility of symbolic argc + argv

[Lukáš Zaoral]

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