From ec2239cb52c23af99182c14555dfe0de7f9c1fe6 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 5 Jul 2024 18:39:50 +0000 Subject: [PATCH] Regression test: support big and little endian Extracting a value from a union via a field of different size is sensitive to endianness. --- regression/cbmc-incr-smt2/unions/padded.desc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/regression/cbmc-incr-smt2/unions/padded.desc b/regression/cbmc-incr-smt2/unions/padded.desc index d9c986bbe1b..b4223c923eb 100644 --- a/regression/cbmc-incr-smt2/unions/padded.desc +++ b/regression/cbmc-incr-smt2/unions/padded.desc @@ -3,7 +3,7 @@ padded.c --trace Passing problem to incremental SMT2 solving \[main\.assertion\.1\] line 13 assertion my_union\.a \=\= 5\: FAILURE -my_union\=\{ \.a\=\d+ \} \(\d{8} 00000101\) +my_union\=\{ \.a\=\d+ \} \((\d{8} 00000101|00000101 \d{8})\) ^EXIT=10$ ^SIGNAL=0$ --