typing rule of \old(tab) or tab[index] construct
ID0000761: This issue was created automatically from Mantis Issue 761. Further discussion may take place here.
|ID0000761||Frama-C||Kernel > ACSL implementation||public||2011-03-22||2014-02-12|
|Priority||normal||Severity||minor||Reproducibility||have not tried|
|Product Version||Frama-C Carbon-20110201||Target Version||-||Fixed in Version||Frama-C Nitrogen-20111001|
\old(t) is interpreted as \old((int*)t) when t is a C variable declared as follow: int t;
That raises a problem when using such constructs combined with \let constructs. It is mainly accepted that \old(\let x = t ; x) is equivalent to \let x = \old(t) ; x That propagation rule implies the type of t should be the same than the type of \old(t).
That isn't the case with the current ACSL implementation: \old(\let x = t ; x) has type int and \let x = \old(t) ; x has type int* The issue is more significant on theses expressions \old(\let x = t ; x) and (\let x = \old(t) ; x).
So, is the problem with a typing rule or with the propagation rule.