0002340: Coq translation of predicate name changes when additional files are processed by Frama-C

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0002340

Frama-C

Plug-in > wp

public

2018-01-04 14:26

2018-02-02 18:37

Reporter

Jochen

Assigned To

correnson

Priority

normal

Severity

minor

Reproducibility

always

Status

acknowledged

Resolution

open

Platform

Sulfur-20171101

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

equal_range2_cpp.c [^] (401 bytes) 2018-01-04 14:26 [Show Content] [Hide Content]

/*@
  predicate
    LowerBound{L}(int* a, integer m, integer n, int v) =
      \forall integer i; m <= i < n  ==>  v <= a[i];

  predicate
    LowerBound{L}(int* a, integer n, int v) =
      LowerBound{L}(a, 0, n, v);
*/



/*@ 
  lemma
    LowerBoundShift{L}:
      \forall int *a, val, integer b, c, d;
        LowerBound{L}(a+b, c,   d,   val)  ==>
        LowerBound{L}(a,   c+b, d+b, val);

*/

lower_bound_cpp.c [^] (328 bytes) 2018-01-04 14:26 [Show Content] [Hide Content]

/*@
  predicate
    LowerBound{L}(int* a, integer m, integer n, int v) =
      \forall integer i; m <= i < n  ==>  v <= a[i];

  predicate
    LowerBound{L}(int* a, integer n, int v) =
      LowerBound{L}(a, 0, n, v);
*/



/*@
  assigns \nothing;
  ensures right:   LowerBound(a, n, n, n);
*/
void lwbnd(const int* a,int n);

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 0002153; 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 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.

(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 ...).

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