I'm currently playing around with frama-c and I'm looking to see how frama-c encodes the various proof obligations for giving to a prover (or proof assistant). In this instance, alt-ergo.
I was wondering if there's any specific way to "dump" the input given to alt-ergo (assuming alt-ergo is invoked from frama-c; i.e. not interop)?
I'd like to see how proof obligations of C programs' properties are encoded in alt-ergo's "native" input language. Any assistance would be much appreciated.
The option -wp-out <dir> allows you to select <dir> as the directory where generated files will be put. These files are sorted in subdirectories according to the memory model in use (typed by default). For Alt-Ergo, you should find files ending in .ergo containing only the proof obligation, and files ending in _Alt-Ergo.mlw containing the full context of the proof obligation (including axioms defining the arithmetic and memory models).
Note however that the upcoming Frama-C 20.0 Calcium is introducing the use of Why3's API for communicating with the provers, and that as a result the native Alt-Ergo (and Coq) outputs are slowly being deprecated.
