Skip to content
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

Jump to bottom

Update CBMC build instructions for Amazon Linux 2 #3431

Merged
merged 1 commit into from
Aug 9, 2024
Merged

Update CBMC build instructions for Amazon Linux 2 #3431

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
79 changes: 76 additions & 3 deletions scripts/setup/al2/install_cbmc.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,10 +21,83 @@ git clone \

pushd "${WORK_DIR}"

mkdir build
git submodule update --init
# apply workaround for https://github.com/diffblue/cbmc/issues/8357 until it is
# properly fixed in CBMC
cat > varargs.patch << "EOF"
--- a/src/ansi-c/library/stdio.c
+++ b/src/ansi-c/library/stdio.c
@@ -1135,7 +1135,7 @@ int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg)

cmake3 -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical"
(void)*format;
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) <
- __CPROVER_OBJECT_SIZE(arg))
+ __CPROVER_OBJECT_SIZE(*(void **)&arg))
{
void *a = va_arg(arg, void *);
__CPROVER_havoc_object(a);
@@ -1233,7 +1233,7 @@ int __stdio_common_vfscanf(

(void)*format;
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&args) <
- __CPROVER_OBJECT_SIZE(args))
+ __CPROVER_OBJECT_SIZE(*(void **)&args))
{
void *a = va_arg(args, void *);
__CPROVER_havoc_object(a);
@@ -1312,7 +1312,7 @@ __CPROVER_HIDE:;
(void)*s;
(void)*format;
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) <
- __CPROVER_OBJECT_SIZE(arg))
+ __CPROVER_OBJECT_SIZE(*(void **)&arg))
{
void *a = va_arg(arg, void *);
__CPROVER_havoc_object(a);
@@ -1388,7 +1388,7 @@ int __stdio_common_vsscanf(
(void)*s;
(void)*format;
while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&args) <
- __CPROVER_OBJECT_SIZE(args))
+ __CPROVER_OBJECT_SIZE(*(void **)&args))
{
void *a = va_arg(args, void *);
__CPROVER_havoc_object(a);
@@ -1774,12 +1774,12 @@ int vsnprintf(char *str, size_t size, const char *fmt, va_list ap)
(void)*fmt;

while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) <
- __CPROVER_OBJECT_SIZE(ap))
+ __CPROVER_OBJECT_SIZE(*(void **)&ap))

{
(void)va_arg(ap, int);
__CPROVER_precondition(
- __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap),
+ __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(*(void **)&ap),
"vsnprintf object overlap");
}

@@ -1822,12 +1822,12 @@ int __builtin___vsnprintf_chk(
(void)*fmt;

while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) <
- __CPROVER_OBJECT_SIZE(ap))
+ __CPROVER_OBJECT_SIZE(*(void **)&ap))

{
(void)va_arg(ap, int);
__CPROVER_precondition(
- __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap),
+ __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(*(void **)&ap),
"vsnprintf object overlap");
}

EOF

cmake3 -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical" \
-DCMAKE_C_COMPILER=gcc10-cc -DCMAKE_CXX_COMPILER=gcc10-c++ \
-DCMAKE_CXX_STANDARD_LIBRARIES=-lstdc++fs \
-DCMAKE_CXX_FLAGS=-Wno-error=register
cmake3 --build build -- -j$(nproc)
sudo make -C build install

Expand Down
1 change: 1 addition & 0 deletions scripts/setup/al2/install_deps.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ set -eu
DEPS=(
cmake
cmake3
gcc10-c++
git
openssl-devel
python3-pip
Expand Down
Loading