From 31970458116edc0b45fda69fef5e9ef643370a22 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 4 Oct 2017 11:04:54 +0100
Subject: [PATCH 1/2] library_check: rename _mm_*fence functions

These functions are built-ins as of LLVM>=9. Treat them the same way as is done
for __builtin_* functions.

Fixes: #1415
---
 src/ansi-c/library_check.sh | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/ansi-c/library_check.sh b/src/ansi-c/library_check.sh
index c65dcd8919e..847ba8f8729 100755
--- a/src/ansi-c/library_check.sh
+++ b/src/ansi-c/library_check.sh
@@ -4,6 +4,7 @@ for f in "$@"; do
     echo "Checking ${f}"
     cp "${f}" __libcheck.c
     perl -p -i -e 's/(__builtin_[^v])/s$1/' __libcheck.c
+    perl -p -i -e 's/(_mm_.fence)/s$1/' __libcheck.c
     perl -p -i -e 's/(__sync_)/s$1/' __libcheck.c
     perl -p -i -e 's/(__noop)/s$1/' __libcheck.c
     cc -std=gnu99 -E -include library/cprover.h -D__CPROVER_bool=_Bool -D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c

From 14eecf663a48bf87a953b91803d8099d08d599eb Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 4 Oct 2017 11:07:05 +0100
Subject: [PATCH 2/2] library_check: use the build-system configured C compiler

---
 src/ansi-c/CMakeLists.txt   | 2 +-
 src/ansi-c/Makefile         | 2 +-
 src/ansi-c/library_check.sh | 7 +++++--
 3 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/src/ansi-c/CMakeLists.txt b/src/ansi-c/CMakeLists.txt
index 8627bfaef4c..ae387958df9 100644
--- a/src/ansi-c/CMakeLists.txt
+++ b/src/ansi-c/CMakeLists.txt
@@ -40,7 +40,7 @@ list(REMOVE_ITEM library_check_sources ${platform_unavail})
 
 add_custom_command(
     DEPENDS ${library_check_sources}
-    COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/library_check.sh ${library_check_sources}
+    COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/library_check.sh ${CMAKE_C_COMPILER} ${library_check_sources}
     COMMAND ${CMAKE_COMMAND} -E touch ${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp
     OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp
     WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
diff --git a/src/ansi-c/Makefile b/src/ansi-c/Makefile
index 1cfc9b01385..53e8104aac1 100644
--- a/src/ansi-c/Makefile
+++ b/src/ansi-c/Makefile
@@ -92,7 +92,7 @@ else
   platform_unavail = library/java.io.c library/threads.c
 endif
 library_check: library/*.c
-	./library_check.sh $(filter-out $(platform_unavail), $^)
+	./library_check.sh $(CC) $(filter-out $(platform_unavail), $^)
 	touch $@
 
 cprover_library.inc: library/converter$(EXEEXT) library/*.c
diff --git a/src/ansi-c/library_check.sh b/src/ansi-c/library_check.sh
index 847ba8f8729..9da4ee6f633 100755
--- a/src/ansi-c/library_check.sh
+++ b/src/ansi-c/library_check.sh
@@ -1,5 +1,8 @@
 #!/usr/bin/env bash
 
+CC=$1
+shift
+
 for f in "$@"; do
     echo "Checking ${f}"
     cp "${f}" __libcheck.c
@@ -7,8 +10,8 @@ for f in "$@"; do
     perl -p -i -e 's/(_mm_.fence)/s$1/' __libcheck.c
     perl -p -i -e 's/(__sync_)/s$1/' __libcheck.c
     perl -p -i -e 's/(__noop)/s$1/' __libcheck.c
-    cc -std=gnu99 -E -include library/cprover.h -D__CPROVER_bool=_Bool -D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c
-    cc -S -Wall -Werror -pedantic -Wextra -std=gnu99 __libcheck.i -o __libcheck.s -Wno-unused-label
+    $CC -std=gnu99 -E -include library/cprover.h -D__CPROVER_bool=_Bool -D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c
+    $CC -S -Wall -Werror -pedantic -Wextra -std=gnu99 __libcheck.i -o __libcheck.s -Wno-unused-label
     ec="${?}"
     rm __libcheck.s __libcheck.i __libcheck.c
     [ "${ec}" -eq 0 ] || exit "${ec}"