Skip to content

C library: Fix type inconsistencies in contracts code #7371

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Nov 22, 2022
Merged

C library: Fix type inconsistencies in contracts code #7371

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 4 additions & 6 deletions src/ansi-c/library/cprover_contracts.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,12 +8,11 @@

// external dependencies
extern __CPROVER_size_t __CPROVER_max_malloc_size;
extern void *__CPROVER_alloca_object;
extern const void *__CPROVER_alloca_object;
extern const void *__CPROVER_deallocated;
extern const void *__CPROVER_new_object;
extern __CPROVER_bool __CPROVER_malloc_is_new_array;
int __builtin_clzll(unsigned long long);
char __VERIFIER_nondet_char();
__CPROVER_bool __VERIFIER_nondet_CPROVER_bool();

/// \brief A conditionally writable range of bytes.
Expand Down Expand Up @@ -245,8 +244,8 @@ __CPROVER_HIDE:;
// symex state from the number of object_bits/offset_bits
// the number of object bits is determined by counting the number of leading
// zeroes of the built-in constant __CPROVER_max_malloc_size;
__CPROVER_size_t object_bits = __builtin_clzll(__CPROVER_max_malloc_size);
__CPROVER_size_t nof_objects = 1UL << object_bits;
int object_bits = __builtin_clzll(__CPROVER_max_malloc_size);
__CPROVER_size_t nof_objects = 1ULL << object_bits;
*set = (__CPROVER_contracts_obj_set_t){
.max_elems = nof_objects,
.watermark = 0,
Expand Down Expand Up @@ -1143,7 +1142,6 @@ void *__CPROVER_contracts_malloc(
__CPROVER_size_t,
__CPROVER_contracts_write_set_ptr_t);

__CPROVER_bool __VERIFIER_nondet_bool();
/// \brief Implementation of the `is_fresh` front-end predicate.
///
/// The behaviour depends on the boolean flags carried by \p set
Expand All @@ -1170,7 +1168,7 @@ __CPROVER_bool __CPROVER_contracts_is_fresh(
__CPROVER_contracts_write_set_ptr_t write_set)
{
if(!write_set)
return __VERIFIER_nondet_bool();
return __VERIFIER_nondet_CPROVER_bool();
__CPROVER_HIDE:;
#ifdef DFCC_DEBUG
__CPROVER_assert(
Expand Down
2 changes: 1 addition & 1 deletion src/cpp/library/cprover.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ typedef __typeof__(sizeof(int)) __CPROVER_size_t;
void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);
extern const void *__CPROVER_deallocated;
extern const void *__CPROVER_new_object;
extern _Bool __CPROVER_malloc_is_new_array;
extern __CPROVER_bool __CPROVER_malloc_is_new_array;
extern const void *__CPROVER_memory_leak;

void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__));
Expand Down