From 4adb38eea19e9e1a09968f6dd374c67973eb9c38 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 7 Feb 2022 17:42:29 +0100
Subject: [PATCH] [tests] remove incorrect spec from
 tests/val_analysis/result.cc

In presence of constructor elision, the contract of f didn't make sense
---
 tests/val_analysis/oracle/result.res.oracle | 12 +++++++++---
 tests/val_analysis/result.cc                |  1 -
 2 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/tests/val_analysis/oracle/result.res.oracle b/tests/val_analysis/oracle/result.res.oracle
index 3b23f6ed..e4d64e80 100644
--- a/tests/val_analysis/oracle/result.res.oracle
+++ b/tests/val_analysis/oracle/result.res.oracle
@@ -7,16 +7,22 @@ Now output intermediate result
   _frama_c_rtti_name_info.name ∈ {{ "A" }}
                          {.base_classes; .number_of_base_classes; .pvmt} ∈
                          {0}
-[eva:alarm] tests/val_analysis/result.cc:7: Warning: 
-  function f, behavior default: postcondition got status invalid.
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function g:
+  __retres ∈ {3}
 [eva:final-states] Values at end of function A::Ctor:
   a ∈ {0}
+[eva:final-states] Values at end of function A::Ctor:
+  __fc_tmp_1.x ∈ {3}
 [eva:final-states] Values at end of function A::Dtor:
   
 [eva:final-states] Values at end of function f:
   a.x ∈ {2}
   z ∈ {2}
 [eva:final-states] Values at end of function main:
-  NON TERMINATING FUNCTION
+  b.x ∈ {2}
+  __fc_tmp_0.x ∈ {2}
+  z ∈ {3}
+  __fc_tmp_1.x ∈ {3}
+  __retres ∈ {0}
diff --git a/tests/val_analysis/result.cc b/tests/val_analysis/result.cc
index 275321a8..2fb26faa 100644
--- a/tests/val_analysis/result.cc
+++ b/tests/val_analysis/result.cc
@@ -4,7 +4,6 @@ struct A {
   A(const A& a) { x = a.x + 1; }
 };
 
-/*@ behavior default: ensures \result.x == y; */
 A f(int y) {
   A a;
   int z = y -1;
-- 
GitLab