Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002340Frama-CPlug-in > wppublic2018-01-04 14:262019-10-17 18:01
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionwon't fix 
PlatformSulfur-20171101OSUbuntuOS VersionUbuntu 17.04
Product Version 
Target VersionFixed in Version 
Summary0002340: Coq translation of predicate name changes when additional files are processed by Frama-C
DescriptionRunning "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".
TagsNo tags attached.
Attached Filesc file icon equal_range2_cpp.c [^] (401 bytes) 2018-01-04 14:26 [Show Content]
c file icon lower_bound_cpp.c [^] (328 bytes) 2018-01-04 14:26 [Show Content]
? file icon wp0.script [^] (466 bytes) 2018-01-04 14:26

- Relationships

-  Notes
(0006502)
Jochen (reporter)
2018-01-04 14:29

 Another issues with name translations was #2153; both issues might be related.
(0006517)
correnson (manager)
2018-02-02 16:11
edited on: 2018-02-02 16:12

 Hi Jochen, The two issues are not related, although I've not completely investigated #2153. 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.
(0006518)
correnson (manager)
2018-02-02 16:29

 Cf. internal frama-c issue (465)
(0006519)
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 ...).
(0006905)
correnson (manager)
2019-10-17 17:15

 Remark: the coq output will be deprecated in the next release and will be removed later on.

- Issue History
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

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker