[Feature Request] Add original src line number in WP proof obligation files.
Hello,
I am trying to understand why WP is having problems with a 'simple' calloc
of a complex (ie non-int) memory structure. (This is something done fairly often in ANSI-C code).
AND yes I realize that raw C pointers are dangerous and hence make WP's job nearly impossible... so I do expect that I need to 'teach' WP something about my use of pointers. Unfortunately, at the moment, I am at a loss as to what additional information I need to provide to WP.
(I have repeatedly (re)read the various "Memory Model" / "Dynamic Allocation" sections of the ACSL, EVA and WP manuals... )
While researching this problem, I noticed that Frama-C has an -wp-out <directory>
switch which can be used to keep all of WP's proof obligations for review by human inspection / interaction with the Why3 gui.
When I added this switch, I find a large number of individual files with Why3/Alt-Ergo statements in them.
Unfortunately I am not experienced enough with the system to map each file to the particular WP assertion in the original source code that WP is trying to prove.
Request: Could you add a simple one line comment (* ... *)
at the top of each of the proof obligation files which informs a human reader which original line of source code and/or rte/wp assertion (in ACSL) is being proven?
This would help a non-Frama-C developer by providing the conceptual context for the proof obligation being proven.
Regards, Stephen Gaito