From 62e3144fe7a38cf1e18e61184c9b777b57313b84 Mon Sep 17 00:00:00 2001 From: Boris Yakobowski <boris.yakobowski@cea.fr> Date: Fri, 15 Jan 2016 15:01:27 +0100 Subject: [PATCH] Fix tests with branch feature/andre/empty-struct better handling of \valid on pointers to empty structs in Value --- src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle | 4 ++-- src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle index 36ad7b7e87f..983b2ddb8e8 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle @@ -11,12 +11,12 @@ __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] [value] using specification for function __store_block -tests/bts/bts1700.i:10:[value] Assertion got status unknown. +tests/bts/bts1700.i:10:[value] Assertion got status valid. [value] using specification for function __valid [value] using specification for function e_acsl_assert FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. [value] using specification for function __full_init -tests/bts/bts1700.i:13:[value] Assertion got status unknown. +tests/bts/bts1700.i:13:[value] Assertion got status valid. [value] using specification for function __initialized [value] using specification for function __delete_block [value] using specification for function __e_acsl_memory_clean diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle index 36ad7b7e87f..983b2ddb8e8 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle @@ -11,12 +11,12 @@ __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] [value] using specification for function __store_block -tests/bts/bts1700.i:10:[value] Assertion got status unknown. +tests/bts/bts1700.i:10:[value] Assertion got status valid. [value] using specification for function __valid [value] using specification for function e_acsl_assert FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. [value] using specification for function __full_init -tests/bts/bts1700.i:13:[value] Assertion got status unknown. +tests/bts/bts1700.i:13:[value] Assertion got status valid. [value] using specification for function __initialized [value] using specification for function __delete_block [value] using specification for function __e_acsl_memory_clean -- GitLab