Feature request: support for argc, argv

[db7]

How hard would it be to pass arguments to the tested program, letting main() do its job with argc and argv? I imagine that getting those values in the interpreter and passing to the function is simple because lli also supports it, but I wonder if there would be any implications to the verification?

[michaliskok]

Apart from making argument parsing a bit different, I don't see any major issues. I'll add it in my TODOs.

Michalis

[db7]

Perhaps it would be also possible to manually (and optionally) mark a point in the main() where the initialization has finished (with some __VERIFIER_...). So that updates before that point are considered part of the [INIT] state. That could help initializing memory with bzero() or other things while not causing mixed-size accesses. May be this would be too much sugar... :-D

[michaliskok]

I looked a bit into providing support for argc and argv, but it will make parsing more complicated if we are to maintain backward compatibility. If you do have cases where using CFLAGS is not adequate, I could provide a separate switch -argv which would then be used to pass runtime arguments. How does that sound?

[db7]

That sounds perfect.