Skip to content

Commit 4d7039e

Browse files
committed
C library: typecast Boolean operand to int when using bitwise ops
Clang warns when bitwise operations are used with Boolean operands.
1 parent 4c3d949 commit 4d7039e

File tree

1 file changed

+6
-5
lines changed

1 file changed

+6
-5
lines changed

src/ansi-c/library/cprover_contracts.c

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -210,8 +210,8 @@ __CPROVER_HIDE:;
210210
CAR_SET_CONTAINS_LOOP:
211211
while(idx != 0)
212212
{
213-
incl |= candidate.is_writable & elem->is_writable &
214-
__CPROVER_same_object(elem->lb, candidate.lb) &
213+
incl |= (int)candidate.is_writable & (int)elem->is_writable &
214+
(int)__CPROVER_same_object(elem->lb, candidate.lb) &
215215
(__CPROVER_POINTER_OFFSET(elem->lb) <=
216216
__CPROVER_POINTER_OFFSET(candidate.lb)) &
217217
(__CPROVER_POINTER_OFFSET(candidate.ub) <=
@@ -798,7 +798,7 @@ __CPROVER_HIDE:;
798798
while(idx != 0)
799799
{
800800
incl |=
801-
elem->is_writable & __CPROVER_same_object(elem->lb, ptr) &
801+
(int)elem->is_writable & (int)__CPROVER_same_object(elem->lb, ptr) &
802802
(__CPROVER_POINTER_OFFSET(elem->lb) <= offset) &
803803
(__CPROVER_POINTER_OFFSET(ub) <= __CPROVER_POINTER_OFFSET(elem->ub));
804804
++elem;
@@ -1045,8 +1045,9 @@ __CPROVER_HIDE:;
10451045
// call free only iff the pointer is valid preconditions are met
10461046
// skip checks on r_ok, dynamic_object and pointer_offset
10471047
__CPROVER_bool preconditions =
1048-
(ptr == 0) | (__CPROVER_r_ok(ptr, 0) & __CPROVER_DYNAMIC_OBJECT(ptr) &
1049-
(__CPROVER_POINTER_OFFSET(ptr) == 0));
1048+
(ptr == 0) |
1049+
((int)__CPROVER_r_ok(ptr, 0) & (int)__CPROVER_DYNAMIC_OBJECT(ptr) &
1050+
(__CPROVER_POINTER_OFFSET(ptr) == 0));
10501051
// If there is aliasing between the pointers in the freeable set,
10511052
// and we attempt to free again one of the already freed pointers,
10521053
// the r_ok condition above will fail, preventing us to deallocate

0 commit comments

Comments
 (0)