Merge pull request #7844 from tautschnig/bugfixes/unsigned-char

Fix tests for unsigned-char architectures

Author: tautschnig

regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.desc

@@ -5,7 +5,7 @@ shift_right.c
 \[main\.assertion\.2\] line \d+ Right shifting a positive number has a lower bound of 0: SUCCESS
 \[main\.assertion\.3\] line \d+ Right shifting a negative number has a lower bound value of -1: SUCCESS
 second=128
-result_unsigned=64
+result_unsigned=(64|'@')
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/cbmc/integral-trace/test.desc

@@ -5,7 +5,7 @@ activate-multi-line-match
 ^EXIT=10$
 ^SIGNAL=0$
 VERIFICATION FAILED
-<full_lhs>u8</full_lhs>\s*<full_lhs_value binary="01100001">97</full_lhs_value>
+<full_lhs>u8</full_lhs>\s*<full_lhs_value binary="01100001">(97|'a')</full_lhs_value>
 <full_lhs>u16</full_lhs>\s*<full_lhs_value binary="0{12}1000">8</full_lhs_value>
 <full_lhs>u32</full_lhs>\s*<full_lhs_value binary="0{27}10000">16ul?</full_lhs_value>
 <full_lhs>u64</full_lhs>\s*<full_lhs_value binary="0{58}100000">32ull?</full_lhs_value>

regression/cbmc/pointer-offset-01/test.desc

@@ -1,14 +1,14 @@
 CORE
 main.c
 --trace
-^\s*ub.*=\(char \*\)&dynamic_object \+ \d+
+^\s*ub.*=(\(char \*\)&)?dynamic_object \+ \d+
 ^\s*offset_ubp1=\d+ul* \(00000000 1[0 ]+1\)$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
-^\s*ub.*=\(char \*\)&dynamic_object \+ -\d+
+^\s*ub.*=(\(char \*\)&)?dynamic_object \+ -\d+
 ^\s*offset_ubp1=\d+ul* \(11111111 1
 --
 Verifies that all offsets use unsigned arithmetic.

regression/goto-instrument-json/rol_signed/test-signed.desc

@@ -3,7 +3,7 @@ test-signed.json
 --dump-c
 ^EXIT=0$
 ^SIGNAL=0$
-signed char rol8=\(unsigned char\)'8' << 3 % 8 \| \(unsigned char\)'8' >> 8 - 3 % 8;
+signed char rol8=\(unsigned char\)('8'|56) << 3 % 8 \| \(unsigned char\)('8'|56) >> 8 - 3 % 8;
 --
 irep
 --

regression/goto-instrument-json/rol_unsigned/test.desc

@@ -3,7 +3,7 @@ test.json
 --dump-c
 ^EXIT=0$
 ^SIGNAL=0$
-unsigned char rol8=56 << 3 % 8 \| 56 >> 8 - 3 % 8;
+unsigned char rol8=(56|'8') << 3 % 8 \| (56|'8') >> 8 - 3 % 8;
 --
 irep
 --

regression/goto-instrument-json/ror_signed/test-signed.desc

@@ -3,7 +3,7 @@ test-signed.json
 --dump-c
 ^EXIT=0$
 ^SIGNAL=0$
-signed char ror8=\(unsigned char\)'8' >> 3 % 8 \| \(unsigned char\)'8' << 8 - 3 % 8;
+signed char ror8=\(unsigned char\)('8'|56) >> 3 % 8 \| \(unsigned char\)('8'|56) << 8 - 3 % 8;
 --
 irep
 --

regression/goto-instrument-json/ror_unsigned/test.desc

@@ -3,7 +3,7 @@ test.json
 --dump-c
 ^EXIT=0$
 ^SIGNAL=0$
-unsigned char ror8=56 >> 3 % 8 \| 56 << 8 - 3 % 8;
+unsigned char ror8=(56|'8') >> 3 % 8 \| (56|'8') << 8 - 3 % 8;
 --
 irep
 --