Original issue in Frama-C bts
Local ghosts should not shadow local non-ghost in non-ghost code, as in
void titi() {
int c = 0;
{
/*@ ghost int c = 1; */
c = 2; //c is still the non-ghost variable here.
}
/*@ assert c == 2; */
}
However, the ACSL manual does not say anything about that. A possibility would be to say that ghost code is implicitly enclosed into its own block. however, this would preclude something like that:
void f() {
/*@ ghost int c = 1; */
int x = 0;
/*@ ghost c = x; */
x++;
/*@ assert c == x - 1; */
}
and more generally would probably preclude the use of local ghost variables in assertions. It's probably better to have a ghost syntactic scope, which respects the same block boundaries than non-ghost one, but is only active for ghost statements.
Original issue in Frama-C bts Local ghosts should not shadow local non-ghost in non-ghost code, as in
However, the ACSL manual does not say anything about that. A possibility would be to say that ghost code is implicitly enclosed into its own block. however, this would preclude something like that:
and more generally would probably preclude the use of local ghost variables in assertions. It's probably better to have a ghost syntactic scope, which respects the same block boundaries than non-ghost one, but is only active for ghost statements.