feature request: scope interactive verification, akin to /proc: on the command-line

[boogie-org]

feature request: scope interactive verification, akin to /proc: on the command-line

[cpitclaudel]

Hi there,

Thanks for the detailed request and explanations. It should be quite feasible, though I wonder what a good UI for this would be. One question that might help brainstorm it:

• Do you always want to verify either one or all functions? Or do you sometimes want two/three functions together? Presumably a single one, right?

Clément.

[0xabu]

Personally, I'd be happy with a dual of /proc where I can simply type in a pattern. Assuming you want to build something higher-level above that, then yes in my usage it is always a single function/method/lemma at a time, but it would still be nice to keep the raw power of the filter expression available. I guess the ideal goal would be to identify the name of the current function from the cursor location and then verify that, but I don't know if you have all the machinery to enable it (it seems non-trivial to me!).

Thanks for considering this!
Andrew

[cpitclaudel]

Maybe the filter is the simplest thing. Given my limited time, a prototype working with just a filter would probably be a good start.

I need to look at the server code and protocol definition to see if they can support this without an extension. IIRC the protocol already supports passing extra arguments.