2021-01-21 05:58 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002153Frama-CPlug-in > wppublic2015-09-03 11:55
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformSodium-20150201OSOS Versionxubuntu14.04
Product VersionFrama-C Sodium 
Target VersionFixed in Version 
Summary0002153: bound variable names in Coq file depend on unrelated function later in C source code
DescriptionRunning "frama-c -pp-annot -wp -wp-split -kernel-msg-key pp -wp-model Typed+ref -wp-driver ../BitTest.driver -cpp-command 'gcc -C -E' -wp-timeout 2 -wp-coq-timeout 5 -wp-prover cvc4 -wp-prover coq 0.c -wp-out 0.wp" on the attached file "0.c", and the corresponding command on "1.c", generate Coq proof obligation files "0.wp/typed_ref_BitTest/Bitstream_WriteThenRead_assert_left.coq" and "1.wp/typed_ref_BitTest/Bitstream_WriteThenRead_assert_left.coq" that differ in bound variable names.

However, "0.c" initially just includes "1.c" and the defines a function "Bitstream_ReadThenWrite" that is unrelated to the code in "1.c"; for this reason, it shouldn't influence the proof obligation of "Bitstream_WriteThenRead_assert_left". The influence apparently depends on the name of the trailing extra-function in "0.c": if it is named "Bitstream_XeadThenWrite", then the problem disappears. Frama-C handles functions in alphabetical order, as can be seen by its stdout messages.
TagsNo tags attached.
Attached Files
  • c file icon 0.c (103 bytes) 2015-08-31 17:30 -
    #include "1.c"
    
    //@ ensures s->bitpos==0;
    void Bitstream_VeadThenWrite(struct BStr* s) {
    	Read(s);
    }
    
    
    c file icon 0.c (103 bytes) 2015-08-31 17:30 +
  • c file icon 1.c (355 bytes) 2015-08-31 17:30 -
    //@ axiomatic b4fc_bit { predicate BTest(integer v); }
    
    //@ predicate Impl(int x,int y) = (BTest(x) ==> BTest(y));
    
    struct BStr {
    	int* addr;
    	int bitpos;
    };
    
    /*@
    	assigns s->bitpos;
    	ensures Impl(s->addr[0],s->addr[1]);
    */
    int Read(struct BStr* s);
    
    void Bitstream_WriteThenRead(struct BStr* s,int v) {
    	int r = Read(s);
    	//@ assert left: Impl(r,v);
    }
    
    
    c file icon 1.c (355 bytes) 2015-08-31 17:30 +
  • ? file icon BitTest.driver (175 bytes) 2015-08-31 17:32

-Relationships
related to 0002100closedcorrenson readability of coq(?) names 
+Relationships

-Notes

~0006012

Jochen (reporter)

(In file "0.c", the trailing extra-function is currently called "Bitstream_VeadThenWrite" rather than "Bitstream_ReadThenWrite". I had experimented with alphabetical order, and forgotten to restore the original name. I can't change the Description field or the uploaded file here, in order to correct my inconsistency.)

Not all of the command line options are really needed. However, using the full command line as given above, the naming difference is maximized, viz.:

29c29
< let m := t.[ (shiftfield_F_BStr_bitpos a) <- (i_1)%Z ] in
---
> let m := t.[ (shiftfield_F_BStr_bitpos a) <- (i)%Z ] in
34c34
< ((is_sint32 i%Z)) ->
---
> ((is_sint32 i_1%Z)) ->
40c40
< ((P_Impl i%Z i_2%Z)).
---
> ((P_Impl i_2%Z i_1%Z)).

~0006013

correnson (manager)

Yes, this is fundemental problem in current implementation of WP that we can not change easily.
As far as I understand, this makes a problem for replaying Coq scripts. Correct ?

~0006014

jens (reporter)

Yes, it breaks our coq proofs.

~0006018

Jochen (reporter)

I admit I have no clue about your implementation details; however, I don't understand why you can't just reset your name-generation mechanism for bound variables in proof-goals every time you start generating a new goal, or at least every time you start handling a new C function. I'd expect each of both measures to resolve the issue; or am I wrong?
+Notes

-Issue History
Date Modified Username Field Change
2015-08-31 17:30 Jochen New Issue
2015-08-31 17:30 Jochen Status new => assigned
2015-08-31 17:30 Jochen Assigned To => correnson
2015-08-31 17:30 Jochen File Added: 0.c
2015-08-31 17:30 Jochen File Added: 1.c
2015-08-31 17:32 Jochen File Added: BitTest.driver
2015-08-31 17:42 Jochen Note Added: 0006012
2015-09-01 12:01 correnson Note Added: 0006013
2015-09-01 12:01 correnson Status assigned => acknowledged
2015-09-01 12:03 correnson Relationship added related to 0002100
2015-09-01 12:26 jens Note Added: 0006014
2015-09-03 11:55 Jochen Note Added: 0006018
+Issue History