Notes |
|
(0006012)
|
Jochen
|
2015-08-31 17:42
|
|
(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)). |
|
|
|
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
|
2015-09-01 12:26
|
|
Yes, it breaks our coq proofs. |
|
|
(0006018)
|
Jochen
|
2015-09-03 11:55
|
|
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? |
|