From bc777dc35263b41c220599b2bef375ea86627b3d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 20 Feb 2024 09:53:53 +0000 Subject: [PATCH] Make tests pass when char is unsigned Not all platforms have signed `char` types. --- regression/cbmc-cpp/Pointer_Conversion2/main.cpp | 2 +- regression/cbmc/pragma_cprover_enable_all/test.desc | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/regression/cbmc-cpp/Pointer_Conversion2/main.cpp b/regression/cbmc-cpp/Pointer_Conversion2/main.cpp index ed2e29f5117..47b2882c788 100644 --- a/regression/cbmc-cpp/Pointer_Conversion2/main.cpp +++ b/regression/cbmc-cpp/Pointer_Conversion2/main.cpp @@ -1,5 +1,5 @@ #include -char a[100]; +signed char a[100]; void f(const signed char x[]) { diff --git a/regression/cbmc/pragma_cprover_enable_all/test.desc b/regression/cbmc/pragma_cprover_enable_all/test.desc index 2b59ea8ab11..36a44729a53 100644 --- a/regression/cbmc/pragma_cprover_enable_all/test.desc +++ b/regression/cbmc/pragma_cprover_enable_all/test.desc @@ -8,7 +8,7 @@ main.c ^\[main\.division-by-zero\.\d+\] line 84 division by zero in x / den: FAILURE ^\[main\.overflow\.\d+\] line 84 arithmetic overflow on floating-point division in x / den: FAILURE ^\[main\.enum-range-check\.\d+\] line 85 enum range check in \(ABC\)10: FAILURE -^\[main\.overflow\.\d+\] line 86 arithmetic overflow on signed type conversion in \(char\)\(\(signed int\)i \+ 1\): FAILURE +^\[main\.overflow\.\d+\] line 86 arithmetic overflow on signed (to unsigned )?type conversion in \(char\)\(\(signed int\)i \+ 1\): FAILURE ^\[main\.overflow\.\d+\] line 87 arithmetic overflow on signed \+ in j \+ 1: FAILURE ^VERIFICATION FAILED$ ^EXIT=10$