diff --git a/tests/misc/oracle/asm_initialized.res.oracle b/tests/misc/oracle/asm_initialized.res.oracle index 8a5b5eb3b7df56ab2017ba24da1880114d60ee6a..86cf86de41f0c8e0e9518e089ad3507b61d1cd61 100644 --- a/tests/misc/oracle/asm_initialized.res.oracle +++ b/tests/misc/oracle/asm_initialized.res.oracle @@ -29,23 +29,6 @@ NULL[268435456..4294967298] [inout] Inputs for function main: \nothing -/* Generated by Frama-C */ -int main(void) -{ - int *sp; - int x; - /*@ ensures \initialized(&sp); - assigns sp; - assigns sp \from \nothing; */ - __asm__ volatile ("mov %%rsp, %0;" : "=r" (sp)); - /*@ assert inline_stmt_contract: \initialized(&sp); */ ; - /*@ assert Eva: mem_access: \valid(sp - 2); */ - *(sp - 2) = 3; - /*@ assert Eva: initialization: \initialized(&x); */ - return x; -} - - [report] Computing properties status... --------------------------------------------------------------------------------