From d4bd82ff8a7facf67758047a55699a393709b6bf Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@cea.fr>
Date: Thu, 26 Sep 2024 18:44:55 +0200
Subject: [PATCH] [tests] update oracle after rebase
---
tests/misc/oracle/asm_initialized.res.oracle | 17 -----------------
1 file changed, 17 deletions(-)
diff --git a/tests/misc/oracle/asm_initialized.res.oracle b/tests/misc/oracle/asm_initialized.res.oracle
index 8a5b5eb3b7..86cf86de41 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...
--------------------------------------------------------------------------------
--
GitLab