how to specify equality of references, rather than of values, in contract?
ID0001990: This issue was created automatically from Mantis Issue 1990. Further discussion may take place here.
|ID0001990||Frama-Clang||Plug-in > clang||public||2014-11-24||2015-02-16|
|Product Version||-||Target Version||-||Fixed in Version||-|
The contract of the function "fst" in line 4 of the attached program intends to specify that "fst(ppp)" returns a reference to "ppp.xxx".
However, it is interpreted by Frama-C as specifying that "fst(ppp)" and "ppp.xxx" have the same value. As a consequence, the assertion in line 10 cannot be proven; the generated obligation essentially amounts to "t_2[a_1] = t_2[a] -> 222 = t_2[a_1 <- 222][a]"; cf. the attached .mlw file. If the precondition would state reference equality (i.e. "a_1 = a") instead of value equality (i.e. "t_2[a_1] = t_2[a]"), the goal would follow trivially.
Frama-C's interpretation is not a bug, but is perfectly valid.
However, the question arises how the intended meaning (i.e. reference equality) could be formalized in the contract. Maybe another equality operator ( named e.g. "===") should be introduced into ACSL++ for this purpose.