diff --git a/tests/val_analysis/oracle/result.res.oracle b/tests/val_analysis/oracle/result.res.oracle index 3b23f6ed4e6a82458c2a697f5f940cc5022c3ae0..e4d64e807d194b5da2b6f5cc6dbaa1f4dc203fb5 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 275321a823661d21bbc9f5b9f4bd5b4b938cf2ef..2fb26faabab5c8c73076f4ef70374e4366a512b8 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;