Skip to content

Commit ea2d393

Browse files
committed
Make test work on windows
This is a hack, but "__asm__ __volatile__ ("mfence": : :"memory");" doesn't compile on windows and the way CBMC handles "__asm mfence" needs to be fixed. Currently "__asm mfence" is not recognised as a function by CBMC.
1 parent 6d0776f commit ea2d393

File tree

1 file changed

+10
-2
lines changed
  • regression/goto-instrument/assembly_call_graph_test

1 file changed

+10
-2
lines changed

regression/goto-instrument/assembly_call_graph_test/main.c

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,16 @@
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+
19
void* thr(void * arg) {
210
#ifdef __GNUC__
311
__asm__ __volatile__ ("mfence": : :"memory");
4-
#elif defined(_MSC_VER)
5-
__asm mfence;
12+
#else
13+
__asm_mfence();
614
#endif
715
}
816

0 commit comments

Comments
 (0)