diff --git a/tests/syntax/ghost_local_capture.i b/tests/syntax/ghost_local_capture.i index fc4ec789d44e7c0cc3a2cee5c86b8e4ecc7171a8..32c520c6903772d10c42df68b0d1d6003273b101 100644 --- a/tests/syntax/ghost_local_capture.i +++ b/tests/syntax/ghost_local_capture.i @@ -11,5 +11,18 @@ void titi() { /*@ assert c == 2; */ } +void toto() { + /*@ ghost int c = 1; */ { + L0: ; + int c = 0; + L1: ; + c = 2; + /*@ assert c == 2; */ + /*@ assert \at(c,L0) == 1; */ + /*@ assert \at(c,L1) == 0; */ + } + /*@ assert c == 1; */ +} + /*@ ghost int x; */ /*@ ghost void f() { x++; } */ diff --git a/tests/syntax/oracle/ghost_local_capture.res.oracle b/tests/syntax/oracle/ghost_local_capture.res.oracle index 6cb26bb591736597e7398bfe889099a4037ecbcd..648e40245cd0098fbd3a8d9b7dd52e785ef84979 100644 --- a/tests/syntax/oracle/ghost_local_capture.res.oracle +++ b/tests/syntax/oracle/ghost_local_capture.res.oracle @@ -16,6 +16,22 @@ void titi(void) return; } +void toto(void) +{ + /*@ ghost int c = 1; */ + { + L0: ; + int c_0 = 0; + L1: ; + c_0 = 2; + /*@ assert c_0 ≡ 2; */ ; + /*@ assert \at(c,L0) ≡ 1; */ ; + /*@ assert \at(c_0,L1) ≡ 0; */ ; + } + /*@ assert c ≡ 1; */ ; + return; +} + /*@ ghost int x; */ /*@ ghost void f(void) {