Skip to content

Commit 85535be

Browse files
committed
Avoid need for preprocessor calls with -m64
This isn't portable to non-x86 architectures.
1 parent 34dc8dc commit 85535be

File tree

4 files changed

+14
-2
lines changed

4 files changed

+14
-2
lines changed

regression/cbmc-concurrency/memory_barrier2/msvc.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
CORE
2-
msvc.c
2+
msvc.i
33
--mm tso --winx64
44
^EXIT=0$
55
^SIGNAL=0$

regression/cbmc-concurrency/memory_barrier2/msvc.c renamed to regression/cbmc-concurrency/memory_barrier2/msvc.i

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,8 @@
1+
void __asm_mfence(void)
2+
{
3+
__CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
4+
}
5+
16
volatile int turn;
27
int x;
38
volatile int flag1 = 0, flag2 = 0;

regression/cbmc-library/__asm_fstcw-01/msvc.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
CORE
2-
msvc.c
2+
msvc.i
33
--pointer-check --bounds-check --winx64
44
^EXIT=0$
55
^SIGNAL=0$

regression/cbmc-library/__asm_fstcw-01/msvc.c renamed to regression/cbmc-library/__asm_fstcw-01/msvc.i

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,10 @@
1+
extern int __CPROVER_rounding_mode;
2+
3+
void __asm_fstcw(void *dest)
4+
{
5+
*(unsigned short *)dest = __CPROVER_rounding_mode << 10;
6+
}
7+
18
int main()
29
{
310
unsigned short cw;

0 commit comments

Comments
 (0)