Skip to content

Commit 7bfd36b

Browse files
authored
Merge pull request #2714 from diffblue/msvc-asm
add support for Visual Studio style inline assembler
2 parents 254b4d4 + af79cb9 commit 7bfd36b

File tree

2 files changed

+315
-161
lines changed

2 files changed

+315
-161
lines changed

regression/goto-instrument/assembly_call_graph_test/main.c

Lines changed: 4 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,10 @@
1-
// This is a hack to make the test pass on windows. The way CBMC on
2-
// windows handles assembly code needs to be fixed.
3-
// CBMC doesn't recognise __asm mfence as a function.
4-
5-
#ifndef __GNUC__
6-
void __asm_mfence();
7-
#endif
8-
91
void* thr(void * arg) {
102
#ifdef __GNUC__
11-
__asm__ __volatile__ ("mfence": : :"memory");
3+
// gcc/clang syntax
4+
__asm__ __volatile__("mfence" : : : "memory");
125
#else
13-
__asm_mfence();
6+
// this is Visual Studio syntax
7+
__asm mfence;
148
#endif
159
}
1610

0 commit comments

Comments
 (0)