argv out-of-bound access is silently ignored

[lzaoral]

Might be related to #103.

Input:

#include <assert.h>

int main(int argc, char * argv[])
{
    assert(argc == 1);
    const char *ptr = argv[10]; /* error */
}

Output:

$ symbiotic --prp=memsafety argv-oob.c
8.0.0-pre-llvm-12.0.0-symbiotic:66916f64-dg:06c8ca8c-sbt-slicer:b0864a5b-sbt-instrumentation:ad1d134f-klee:10e5fae9
INFO: Looking for invalid dereferences, invalid free, memory leaks, etc.
INFO: Starting instrumentation
wrapper: `which slllvm` failed with error code 1

INFO: Instrumentation time: 0.05532646179199219
INFO: Optimizations time: 0.02613091468811035
INFO: Starting slicing
INFO: Total slicing time: 0.020180940628051758
INFO: Optimizations time: 0.026351213455200195
INFO: After-slicing optimizations and transformations time: 3.0517578125e-05
INFO: Starting verification
KLEE: WARNING: undefined reference to function: klee_make_nondet
No error found.
NOTE: In the future, the result is going to be reported in SV-COMP format only with --report=sv-comp switch
RESULT: true
INFO: Total time elapsed: 0.5680685043334961

[mchalupa]

Yep, solving this should probably solve also #103 .

We need to:

• enable symbolic argv in KLEE (and other verification backends). KLEE allows only a bounded argv, so we must pick a good bound (and make sure to catch the cases where the bound is not enough to avoid incorrect answers).
• check that slicer works in this scenario. I think that slicer should work well, but is imprecise with argv (Model argv[] mchalupa/dg#280.)