ID0002340: **This issue was created automatically from Mantis Issue 2340. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002340 | Frama-C | Plug-in > wp | public | 2018-01-04 | 2019-10-17 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | won't fix | | **Priority** | normal | **Severity** | minor | **Reproducibility** | always | | **Platform** | Sulfur-20171101 | **OS** | Ubuntu | **OS Version** | Ubuntu 17.04 | | **Product Version** | - | **Target Version** | - | **Fixed in Version** | - | ### Description : 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". ## Attachments - [equal_range2_cpp.c](/uploads/a7f339a24fa1ad2c67458331246b61a8/equal_range2_cpp.c) - [lower_bound_cpp.c](/uploads/1b5c79b560a67c3ba096b9ce8462c3fc/lower_bound_cpp.c) - [wp0.script](/uploads/a549eb877d73af8f17c7be0a3cad6d0c/wp0.script)