Evgeny Novikov

We can teach our C-backend to replace all calls to undefined functions, which base return types are simple, e.g. integers, with calls to SV-COMP well known functions. So this will...

I agree with you that it would be better to do this explicit both in SV-COMP rules and by providing some option to verification tools through BencExec wrappers. The same...

Another corner question is calls through unknown function pointers. Although this is just one special case of common interpretation of unknown pointers, it usually matters more than operations with other...

It won't be easy because of there is an unknown list of thousands of such functions when we are preparing verification tasks on the fly. So they should be processed...

My last reply was for Steve's last comment. It is hard for verifiers (people) to provide stubs for all unknown functions manually (and this has no much sense). This can...

Another option is to provide the list of assumptions globally, but this won't permit some tricky cases, e.g. when there are some particular context dependent reasonings about a call through...

> In a real world use case, the person who wrote the stub would be the same person who is running the verification tool. They don't need to be told...

Like #86 this is a very low priority issue, so, you can implement it much more later.