Coq translation of predicate name changes when additional files are processed by Frama-C
ID0002340: This issue was created automatically from Mantis Issue 2340. Further discussion may take place here.
|ID0002340||Frama-C||Plug-in > wp||public||2018-01-04||2019-10-17|
|Reporter||Jochen||Assigned To||correnson||Resolution||won't fix|
|Platform||Sulfur-20171101||OS||Ubuntu||OS Version||Ubuntu 17.04|
|Product Version||-||Target Version||-||Fixed in Version||-|
Running "frama-c -wp -wp-script wp0.script -wp-model Typed+ref -wp-prover coq -wp-prop LowerBoundShift equal_range2_cpp.c" succeeds in proving the lemma in line 16 of "equal_range2_cpp.c", using the Coq proof in file "wp0.script". However, when "lower_bound_cpp.c" is appended as another command line argument to the same call, the lemma is no longer proven. Using "wp-out" arguments and running a "diff -r" on the resulting directories reveals that the ACSL predicate name "LowerBound" is translated as "P_LowerBound_1_" for the first (succeeding) run, but as "P_LowerBound_2_" for the second (failing) run. Note that the definitions of the "LowerBound" predicates literally agree in both C files. The problem disappears when the overloaded 3-argument version of predicate "LowerBound" is omitted in both C files, or when the contract (i.e. the only use of "LowerBound" in that file) is omitted in file "lower_bound_cpp.c".