Improve the model for argc and argv

[arthaud]

On the following example:

#include <stdio.h>

int main(int argc, char** argv) {
    if (argc < 2) {
        return 0;
    }

    printf("Hello, %s", argv[1]);
    return 0;
}

IKOS generates the following warnings:

test.c: In function 'main':
test.c:8:5: warning: memory access might be invalid, could not infer information about pointer 'argv[1]'
    printf("Hello, %s", argv[1]);
    ^
test.c: In function 'main':
test.c:8:25: warning: possible buffer overflow, pointer '&argv[1]' accesses 8 bytes at offset 8 bytes of 'argv'
    printf("Hello, %s", argv[1]);
                        ^

We need to model argc/argv properly to get rid of these warnings. This seems complicated to achieve for non-relational numerical domains.