From f3738af757f9b851ed11c202d12aae317da0beb0 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 27 Nov 2023 10:13:29 -0800 Subject: [PATCH 1/3] The emscripten compiler has alloca.h Emscripten is a compiler that targets WASM. To enable cross-compilation with emscripten, allocainc.h now uses alloca.h for this compiler. --- src/big-int/allocainc.h | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/big-int/allocainc.h b/src/big-int/allocainc.h index d0817d01484..30c491565ec 100644 --- a/src/big-int/allocainc.h +++ b/src/big-int/allocainc.h @@ -5,15 +5,17 @@ #ifndef CPROVER_BIG_INT_ALLOCAINC_H #define CPROVER_BIG_INT_ALLOCAINC_H - +// clang-format off #if defined linux || defined __linux__ \ || defined __sun \ || defined UWIN \ || defined osf1 \ || defined __MACH__ \ - || defined __CYGWIN__ + || defined __CYGWIN__ \ + || defined __EMSCRIPTEN__ +// clang-format on -#include +# include #elif defined _MSC_VER \ || defined __BORLANDC__ \ From e719c8b10b4bd697381f77363139adfe71418642 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 27 Nov 2023 13:47:14 -0800 Subject: [PATCH 2/3] add author section to satisfy cpplint --- src/big-int/allocainc.h | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/big-int/allocainc.h b/src/big-int/allocainc.h index 30c491565ec..2623b1da9c6 100644 --- a/src/big-int/allocainc.h +++ b/src/big-int/allocainc.h @@ -1,4 +1,10 @@ -// $Id: allocainc.h,v 1.7 2005-12-25 14:44:24 kroening Exp $ +/*******************************************************************\ + +Module: Big Integers + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ // Whatever is necessary to use alloca(). From 6a14010bdf01c96754b635dafcf484d5c09dd252 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 27 Nov 2023 13:48:35 -0800 Subject: [PATCH 3/3] tweak whitespace to satisfy cpplint --- src/big-int/allocainc.h | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/big-int/allocainc.h b/src/big-int/allocainc.h index 2623b1da9c6..31849174cbd 100644 --- a/src/big-int/allocainc.h +++ b/src/big-int/allocainc.h @@ -12,13 +12,13 @@ Author: Daniel Kroening, dkr@amazon.com #define CPROVER_BIG_INT_ALLOCAINC_H // clang-format off -#if defined linux || defined __linux__ \ - || defined __sun \ - || defined UWIN \ - || defined osf1 \ - || defined __MACH__ \ - || defined __CYGWIN__ \ - || defined __EMSCRIPTEN__ +#if defined linux || defined __linux__ \ + || defined __sun \ + || defined UWIN \ + || defined osf1 \ + || defined __MACH__ \ + || defined __CYGWIN__ \ + || defined __EMSCRIPTEN__ // clang-format on # include