Skip to content

Commit a1f1e64

Browse files
authored
Fix conflicting C function definitions (rust-lang#1812)
Declare the function signatures instead of importing system definitions. This avoids conflict between our pre-build libraries and the C files that are built on the user machine. Also remove the gen_c_lib.c file which seems to be dead code.
1 parent 85309be commit a1f1e64

File tree

2 files changed

+8
-66
lines changed

2 files changed

+8
-66
lines changed

library/kani/gen_c_lib.c

Lines changed: 0 additions & 61 deletions
This file was deleted.

library/kani/kani_lib.c

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,15 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
4-
#include <assert.h>
5-
#include <stdbool.h>
63
#include <stddef.h>
74
#include <stdint.h>
8-
#include <stdlib.h>
9-
#include <string.h>
5+
6+
// Declare functions instead of importing more headers in order to avoid conflicting definitions.
7+
// See https://github.com/model-checking/kani/issues/1774 for more details.
8+
void free(void *ptr);
9+
void *memcpy(void *dst, const void *src, size_t n);
10+
void *calloc(size_t nmemb, size_t size);
11+
12+
typedef __CPROVER_bool bool;
1013

1114
// `assert` then `assume`
1215
#define __KANI_assert(cond, msg) \

0 commit comments

Comments
 (0)