View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0002340 | Frama-C | Plug-in > wp | public | 2018-01-04 14:26 | 2019-10-17 18:01 | ||||
Reporter | Jochen | ||||||||
Assigned To | correnson | ||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||
Status | closed | Resolution | won't fix | ||||||
Platform | Sulfur-20171101 | OS | Ubuntu | OS Version | Ubuntu 17.04 | ||||
Product Version | |||||||||
Target Version | Fixed in Version | ||||||||
Summary | 0002340: Coq translation of predicate name changes when additional files are processed by Frama-C | ||||||||
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". | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
Jochen (reporter) 2018-01-04 14:29 |
Another issues with name translations was 0002153; both issues might be related. |
correnson (manager) 2018-02-02 16:11 Last edited: 2018-02-02 16:12 |
Hi Jochen, The two issues are not related, although I've not completely investigated 0002153. The problem comes from the overloading of LowerBound ; each flavour of the predicate is assigned a different name, depending on its order of compilation during WP's tasks. We shall instead generate a name based on its signature to ensures more stability regarding coq scripts. |
correnson (manager) 2018-02-02 16:29 |
Cf. internal frama-c issue (465) |
jens (reporter) 2018-02-02 18:37 |
This sounds like the mangling of C++ names. I wonder how the proposed ACSL overload mangling has to be compatible with C++ name mangling (having Frama-Clang in mind ...). |
correnson (manager) 2019-10-17 17:15 |
Remark: the coq output will be deprecated in the next release and will be removed later on. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2018-01-04 14:26 | Jochen | New Issue | |
2018-01-04 14:26 | Jochen | Status | new => assigned |
2018-01-04 14:26 | Jochen | Assigned To | => correnson |
2018-01-04 14:26 | Jochen | File Added: equal_range2_cpp.c | |
2018-01-04 14:26 | Jochen | File Added: lower_bound_cpp.c | |
2018-01-04 14:26 | Jochen | File Added: wp0.script | |
2018-01-04 14:29 | Jochen | Note Added: 0006502 | |
2018-02-02 16:11 | correnson | Note Added: 0006517 | |
2018-02-02 16:11 | correnson | Note Edited: 0006517 | View Revisions |
2018-02-02 16:12 | correnson | Note Edited: 0006517 | View Revisions |
2018-02-02 16:29 | correnson | Note Added: 0006518 | |
2018-02-02 16:29 | correnson | Status | assigned => acknowledged |
2018-02-02 18:37 | jens | Note Added: 0006519 | |
2019-10-17 17:15 | correnson | Note Added: 0006905 | |
2019-10-17 17:16 | correnson | Status | acknowledged => resolved |
2019-10-17 17:16 | correnson | Resolution | open => won't fix |
2019-10-17 18:01 | signoles | Status | resolved => closed |