bound variable names in Coq file depend on unrelated function later in C source code
ID0002153: This issue was created automatically from Mantis Issue 2153. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002153 | Frama-C | Plug-in > wp | public | 2015-08-31 | 2015-09-03 |
| Reporter | Jochen | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | Sodium-20150201 | OS | - | OS Version | xubuntu14.04 |
| Product Version | Frama-C Sodium | Target Version | - | Fixed in Version | - |
Description :
Running "frama-c -pp-annot -wp -wp-split -kernel-msg-key pp -wp-model Typed+ref -wp-driver ../BitTest.driver -cpp-command 'gcc -C -E' -wp-timeout 2 -wp-coq-timeout 5 -wp-prover cvc4 -wp-prover coq 0.c -wp-out 0.wp" on the attached file "0.c", and the corresponding command on "1.c", generate Coq proof obligation files "0.wp/typed_ref_BitTest/Bitstream_WriteThenRead_assert_left.coq" and "1.wp/typed_ref_BitTest/Bitstream_WriteThenRead_assert_left.coq" that differ in bound variable names.
However, "0.c" initially just includes "1.c" and the defines a function "Bitstream_ReadThenWrite" that is unrelated to the code in "1.c"; for this reason, it shouldn't influence the proof obligation of "Bitstream_WriteThenRead_assert_left". The influence apparently depends on the name of the trailing extra-function in "0.c": if it is named "Bitstream_XeadThenWrite", then the problem disappears. Frama-C handles functions in alphabetical order, as can be seen by its stdout messages.