From 87bd5ac4bf59a6eb26fa834a4d1a1e9e424e2da5 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 20 Jan 2025 14:28:24 +0000
Subject: [PATCH] Avoid need for preprocessor calls with -m64

This isn't portable to non-x86 architectures.
---
 regression/cbmc-concurrency/memory_barrier2/msvc.desc      | 2 +-
 .../cbmc-concurrency/memory_barrier2/{msvc.c => msvc.i}    | 5 +++++
 regression/cbmc-library/__asm_fstcw-01/msvc.desc           | 2 +-
 regression/cbmc-library/__asm_fstcw-01/{msvc.c => msvc.i}  | 7 +++++++
 4 files changed, 14 insertions(+), 2 deletions(-)
 rename regression/cbmc-concurrency/memory_barrier2/{msvc.c => msvc.i} (83%)
 rename regression/cbmc-library/__asm_fstcw-01/{msvc.c => msvc.i} (66%)

diff --git a/regression/cbmc-concurrency/memory_barrier2/msvc.desc b/regression/cbmc-concurrency/memory_barrier2/msvc.desc
index 9327f8de9a5..91f366f8aeb 100644
--- a/regression/cbmc-concurrency/memory_barrier2/msvc.desc
+++ b/regression/cbmc-concurrency/memory_barrier2/msvc.desc
@@ -1,5 +1,5 @@
 CORE
-msvc.c
+msvc.i
 --mm tso --winx64
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/cbmc-concurrency/memory_barrier2/msvc.c b/regression/cbmc-concurrency/memory_barrier2/msvc.i
similarity index 83%
rename from regression/cbmc-concurrency/memory_barrier2/msvc.c
rename to regression/cbmc-concurrency/memory_barrier2/msvc.i
index b36e9a1be00..89ef92d50ed 100644
--- a/regression/cbmc-concurrency/memory_barrier2/msvc.c
+++ b/regression/cbmc-concurrency/memory_barrier2/msvc.i
@@ -1,3 +1,8 @@
+void __asm_mfence(void)
+{
+  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
+}
+
 volatile int turn;
 int x;
 volatile int flag1 = 0, flag2 = 0;
diff --git a/regression/cbmc-library/__asm_fstcw-01/msvc.desc b/regression/cbmc-library/__asm_fstcw-01/msvc.desc
index 0275139a2df..780e6502916 100644
--- a/regression/cbmc-library/__asm_fstcw-01/msvc.desc
+++ b/regression/cbmc-library/__asm_fstcw-01/msvc.desc
@@ -1,5 +1,5 @@
 CORE
-msvc.c
+msvc.i
 --pointer-check --bounds-check --winx64
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/cbmc-library/__asm_fstcw-01/msvc.c b/regression/cbmc-library/__asm_fstcw-01/msvc.i
similarity index 66%
rename from regression/cbmc-library/__asm_fstcw-01/msvc.c
rename to regression/cbmc-library/__asm_fstcw-01/msvc.i
index 11c1cf19932..e9de7276048 100644
--- a/regression/cbmc-library/__asm_fstcw-01/msvc.c
+++ b/regression/cbmc-library/__asm_fstcw-01/msvc.i
@@ -1,3 +1,10 @@
+extern int __CPROVER_rounding_mode;
+
+void __asm_fstcw(void *dest)
+{
+  *(unsigned short *)dest = __CPROVER_rounding_mode << 10;
+}
+
 int main()
 {
   unsigned short cw;