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.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000761 | Frama-C | Kernel > ACSL implementation | public | 2011-03-22 | 2014-02-12 |
| Reporter | patrick | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Carbon-20110201 | Target Version | - | Fixed in Version | Frama-C Nitrogen-20111001 |
Description :
\old(t)[0] is interpreted as \old((int*)t)[0] when t is a C variable declared as follow: int t[10];
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[10] and \let x = \old(t) ; x has type int* The issue is more significant on theses expressions \old(\let x = t ; x)[0] and (\let x = \old(t) ; x)[0].
So, is the problem with a typing rule or with the propagation rule.