[C/LLVM] Handle parameters of main (argc/argv)

[ThomasHaas]

This PR adds a very approximative handling of int argc and char *argv[] passed to main: we just upper bound argc with a constant m=10 and use it to allocate argv properly. The entries of argv will be valid pointers, but their content is also bounded c=10 and not initialized.

NOTE: The constants are arbitrarily chosen, but argc <= 10 is probably good enough for almost all benchmarks.

It should be enough to handle some more SVCOMP benchmarks.

[hernanponcedeleon]

The changes solve some of the issues, but it introduces new ones. We now give correct results for reorder_2, reorder_5 and twostage_3, but wrong results for reorder_2-2, reorder_5-2 and twostage_3-2.

I haven't checked if it introduces more regressions.

Also, I haven't yet checked the code, but at minimum we should add an option to set the upper bound rather than hardcode it.

[ThomasHaas]

We didn't handle any of the benchmarks correctly (and technically we still don't), but the invalid dereference that we reported for, e.g., reorder_2-2 just happened to match the expected result (although the witness would be totally wrong).
I guess we do validate our own witness here so it doesn't really matter that it is bullshit?

For example, the reorder_2... benchmarks use sscanf to parse the argv arguments into iSet and iCheck (which are otherwise set to value 2 as default).
In reorder_2, those values are checked against an upper limit (some high constant) and in reorder_2-2 they are not, causing the former to be safe and the latter to be unsafe.
Before this PR, we reported FAIL in both of them due to accesses to argv, which happened to be correct for reorder_2-2 (but for the wrong reason).
After this PR, we report PASS for both of them (which is again wrong for one of them), but only because our sscanf implementation does nothing so iSet=iCheck=2 (per default) which is valid.

Actually, I don't even understand why the verdicts for the benchmarks are as they are.
I don't understand why inreorder_2 a negative value of iSet/iCheck is supposedly no problem (I think this is UB!).
I also don't understand why the upper bound check for reorder_2-2 is needed: do allocations have an upper bound on their size? I think array[INT_MAX] would be a valid allocation.

In summary, I think we do not handle any of those benchmarks correctly, neither before this PR nor after this PR. This PR is semantically more correct than development but if it causes us to lose points in SVCOMP, it kinda sucks.
The most truthful solution would be to return UNKNOWN for these benchmarks.

[hernanponcedeleon]

For example, the reorder_2... benchmarks use sscanf to parse the argv arguments into iSet and iCheck

Do we even handle this correctly? If not, we should either fix our sscanf intrinsic or completely remove it from the supported ones (which would result in a "violation" by calling unknown intrinsic which in the context of SVCOMP we treat as UNKNOWN).

[ThomasHaas]

We do not handle sscanf and I think it is too hard to implement: we need to non-deterministically store to an address, but we do not know what type is expected (unless we parse the format string or maybe assume addresses to static allocations).

[hernanponcedeleon]

I removed from the supported intrinsic in the svcomp2026 branch here