File tree Expand file tree Collapse file tree 2 files changed +2
-2
lines changed
cbmc/pragma_cprover_enable_all
cbmc-cpp/Pointer_Conversion2 Expand file tree Collapse file tree 2 files changed +2
-2
lines changed Original file line number Diff line number Diff line change 1
1
#include < cassert>
2
- char a[100 ];
2
+ signed char a[100 ];
3
3
4
4
void f (const signed char x[])
5
5
{
Original file line number Diff line number Diff line change 8
8
^\[main\.division-by-zero\.\d+\] line 84 division by zero in x / den: FAILURE
9
9
^\[main\.overflow\.\d+\] line 84 arithmetic overflow on floating-point division in x / den: FAILURE
10
10
^\[main\.enum-range-check\.\d+\] line 85 enum range check in \(ABC\)10: FAILURE
11
- ^\[main\.overflow\.\d+\] line 86 arithmetic overflow on signed type conversion in \(char\)\(\(signed int\)i \+ 1\): FAILURE
11
+ ^\[main\.overflow\.\d+\] line 86 arithmetic overflow on signed (to unsigned )? type conversion in \(char\)\(\(signed int\)i \+ 1\): FAILURE
12
12
^\[main\.overflow\.\d+\] line 87 arithmetic overflow on signed \+ in j \+ 1: FAILURE
13
13
^VERIFICATION FAILED$
14
14
^EXIT=10$
You can’t perform that action at this time.
0 commit comments