Skip to content

Refine symex pointer unsoundness #8780

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 3 commits into
base: develop
Choose a base branch
from
Open

Refine symex pointer unsoundness #8780

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
76b5d2b
Weak-memory examples: selectively use thread-local variables
tautschnig Nov 30, 2025
243a31b
goto-symex/concurrency: limit unsoundness-abort to dereferencing shar…
tautschnig Nov 30, 2025
d48dfd7
Do not use value-set supported simplification with multiple threads
tautschnig Nov 30, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
2 changes: 1 addition & 1 deletion regression/book-examples/account/C10.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
KNOWNBUG
CORE no-new-smt gcc-only
account.c

^EXIT=10$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-concurrency/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
if((NOT WIN32) AND (NOT APPLE) AND (NOT (CMAKE_SYSTEM_NAME STREQUAL "FreeBSD")))
if(NOT WIN32)
add_test_pl_tests(
"$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation"
)
Expand Down
3 changes: 1 addition & 2 deletions regression/cbmc-concurrency/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,8 @@ default: tests.log
include ../../src/config.inc
include ../../src/common

ifeq ($(filter-out OSX MSVC FreeBSD,$(BUILD_ENV_)),)
ifeq ($(filter-out MSVC,$(BUILD_ENV_)),)
# no POSIX threads on Windows
# for OSX and FreeBSD we'd need sound handling of pointers in multi-threaded programs
no_pthread = -X pthread
endif

Expand Down
4 changes: 2 additions & 2 deletions regression/cbmc-concurrency/dirty_local1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
CORE
main.c
--no-standard-checks
^EXIT=10$
pointer handling for concurrency is unsound
^EXIT=6$
^SIGNAL=0$
^VERIFICATION FAILED$
--
^warning: ignoring
8 changes: 8 additions & 0 deletions regression/cbmc-concurrency/global_pointer1/detect_unsoundness.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE pthread
main.c

pointer handling for concurrency is unsound
^EXIT=6$
^SIGNAL=0$
--
^warning: ignoring
4 changes: 4 additions & 0 deletions regression/cbmc-concurrency/global_pointer1/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,9 @@ void *thread1(void * arg)
void *thread2(void *arg)
{
assert(v == &g);
#ifndef NO_DEREF
*v = 1;
#endif
}

int main()
Expand All @@ -26,7 +28,9 @@ int main()
pthread_join(t2, 0);

assert(v == &g);
#ifndef NO_DEREF
assert(*v == 1);
#endif

return 0;
}
8 changes: 8 additions & 0 deletions regression/cbmc-concurrency/global_pointer1/no_deref.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE pthread
main.c
-DNO_DEREF
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
2 changes: 1 addition & 1 deletion regression/cbmc-concurrency/global_pointer1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
KNOWNBUG
KNOWNBUG pthread
main.c

^EXIT=0$
Expand Down
4 changes: 2 additions & 2 deletions regression/cbmc-concurrency/malloc1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
CORE
main.c
--no-malloc-may-fail
^EXIT=0$
pointer handling for concurrency is unsound
^EXIT=6$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
4 changes: 2 additions & 2 deletions regression/cbmc-concurrency/malloc2/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
CORE
main.c
--no-malloc-may-fail
^EXIT=0$
pointer handling for concurrency is unsound
^EXIT=6$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
2 changes: 1 addition & 1 deletion regression/cbmc-concurrency/thread_chain_posix2/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
KNOWNBUG pthread
CORE pthread
main.c
-D_ENABLE_CHAIN_ --unwind 2
^EXIT=0$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-concurrency/thread_chain_posix3/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
KNOWNBUG pthread
CORE pthread
main.c
-D_ENABLE_CHAIN_ -D_SANITY_CHECK_ --unwind 2
^EXIT=10$
Expand Down
10 changes: 3 additions & 7 deletions regression/cbmc-library/realloc-03/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,12 +1,8 @@
CORE
main.c

^EXIT=6$
--no-malloc-may-fail
^VERIFICATION SUCCESSFUL$
^EXIT=0$
^SIGNAL=0$
pointer handling for concurrency is unsound
--
^warning: ignoring
--
The test uses "__CPROVER_ASYNC_1:" and the async-called function foo does
pointer operations over allocated memory - which is not handled in a sound way
in CBMC.
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_aclwsrr000_PSO_ALL/aclwsrr000.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ int __unbuffered_p0_r3 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p2_r1 = 0;
int __unbuffered_p2_r3 = 0;
int __unbuffered_p2_r4 = 0;
__CPROVER_thread_local int __unbuffered_p2_r4 = 0;
int __unbuffered_p2_r5 = 0;
int x = 0;
int y = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_aclwsrr000_PSO_OPC/aclwsrr000.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ int __unbuffered_p0_r3 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p2_r1 = 0;
int __unbuffered_p2_r3 = 0;
int __unbuffered_p2_r4 = 0;
__CPROVER_thread_local int __unbuffered_p2_r4 = 0;
int __unbuffered_p2_r5 = 0;
int x = 0;
int y = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_aclwsrr000_RMO_ALL/aclwsrr000.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ int __unbuffered_p0_r3 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p2_r1 = 0;
int __unbuffered_p2_r3 = 0;
int __unbuffered_p2_r4 = 0;
__CPROVER_thread_local int __unbuffered_p2_r4 = 0;
int __unbuffered_p2_r5 = 0;
int x = 0;
int y = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_aclwsrr000_RMO_OPC/aclwsrr000.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ int __unbuffered_p0_r3 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p2_r1 = 0;
int __unbuffered_p2_r3 = 0;
int __unbuffered_p2_r4 = 0;
__CPROVER_thread_local int __unbuffered_p2_r4 = 0;
int __unbuffered_p2_r5 = 0;
int x = 0;
int y = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_aclwsrr000_TSO_ALL/aclwsrr000.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ int __unbuffered_p0_r3 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p2_r1 = 0;
int __unbuffered_p2_r3 = 0;
int __unbuffered_p2_r4 = 0;
__CPROVER_thread_local int __unbuffered_p2_r4 = 0;
int __unbuffered_p2_r5 = 0;
int x = 0;
int y = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_aclwsrr000_TSO_OPC/aclwsrr000.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ int __unbuffered_p0_r3 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p2_r1 = 0;
int __unbuffered_p2_r3 = 0;
int __unbuffered_p2_r4 = 0;
__CPROVER_thread_local int __unbuffered_p2_r4 = 0;
int __unbuffered_p2_r5 = 0;
int x = 0;
int y = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_aclwsrr002_POWER_ALL/aclwsrr002.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ int __unbuffered_p0_r1 = 0;
int __unbuffered_p0_r3 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p1_r3 = 0;
int __unbuffered_p1_r4 = 0;
__CPROVER_thread_local int __unbuffered_p1_r4 = 0;
int __unbuffered_p1_r5 = 0;
int x = 0;
int y = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_aclwsrr002_POWER_OPC/aclwsrr002.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ int __unbuffered_p0_r1 = 0;
int __unbuffered_p0_r3 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p1_r3 = 0;
int __unbuffered_p1_r4 = 0;
__CPROVER_thread_local int __unbuffered_p1_r4 = 0;
int __unbuffered_p1_r5 = 0;
int x = 0;
int y = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_aclwsrr002_PSO_ALL/aclwsrr002.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ int __unbuffered_p0_r1 = 0;
int __unbuffered_p0_r3 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p1_r3 = 0;
int __unbuffered_p1_r4 = 0;
__CPROVER_thread_local int __unbuffered_p1_r4 = 0;
int __unbuffered_p1_r5 = 0;
int x = 0;
int y = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_aclwsrr002_PSO_OPC/aclwsrr002.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ int __unbuffered_p0_r1 = 0;
int __unbuffered_p0_r3 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p1_r3 = 0;
int __unbuffered_p1_r4 = 0;
__CPROVER_thread_local int __unbuffered_p1_r4 = 0;
int __unbuffered_p1_r5 = 0;
int x = 0;
int y = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_aclwsrr002_RMO_ALL/aclwsrr002.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ int __unbuffered_p0_r1 = 0;
int __unbuffered_p0_r3 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p1_r3 = 0;
int __unbuffered_p1_r4 = 0;
__CPROVER_thread_local int __unbuffered_p1_r4 = 0;
int __unbuffered_p1_r5 = 0;
int x = 0;
int y = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_aclwsrr002_RMO_OPC/aclwsrr002.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ int __unbuffered_p0_r1 = 0;
int __unbuffered_p0_r3 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p1_r3 = 0;
int __unbuffered_p1_r4 = 0;
__CPROVER_thread_local int __unbuffered_p1_r4 = 0;
int __unbuffered_p1_r5 = 0;
int x = 0;
int y = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_aclwsrr002_TSO_ALL/aclwsrr002.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ int __unbuffered_p0_r1 = 0;
int __unbuffered_p0_r3 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p1_r3 = 0;
int __unbuffered_p1_r4 = 0;
__CPROVER_thread_local int __unbuffered_p1_r4 = 0;
int __unbuffered_p1_r5 = 0;
int x = 0;
int y = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_aclwsrr002_TSO_OPC/aclwsrr002.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ int __unbuffered_p0_r1 = 0;
int __unbuffered_p0_r3 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p1_r3 = 0;
int __unbuffered_p1_r4 = 0;
__CPROVER_thread_local int __unbuffered_p1_r4 = 0;
int __unbuffered_p1_r5 = 0;
int x = 0;
int y = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_bclwdww000_PSO_ALL/bclwdww000.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ void isync()

int __unbuffered_cnt = 0;
int __unbuffered_p0_r1 = 0;
int __unbuffered_p0_r3 = 0;
__CPROVER_thread_local int __unbuffered_p0_r3 = 0;
int __unbuffered_p0_r4 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p1_r3 = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_bclwdww000_PSO_OPC/bclwdww000.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ void isync()

int __unbuffered_cnt = 0;
int __unbuffered_p0_r1 = 0;
int __unbuffered_p0_r3 = 0;
__CPROVER_thread_local int __unbuffered_p0_r3 = 0;
int __unbuffered_p0_r4 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p1_r3 = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_bclwdww000_RMO_ALL/bclwdww000.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ void isync()

int __unbuffered_cnt = 0;
int __unbuffered_p0_r1 = 0;
int __unbuffered_p0_r3 = 0;
__CPROVER_thread_local int __unbuffered_p0_r3 = 0;
int __unbuffered_p0_r4 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p1_r3 = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_bclwdww000_RMO_OPC/bclwdww000.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ void isync()

int __unbuffered_cnt = 0;
int __unbuffered_p0_r1 = 0;
int __unbuffered_p0_r3 = 0;
__CPROVER_thread_local int __unbuffered_p0_r3 = 0;
int __unbuffered_p0_r4 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p1_r3 = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_bclwdww000_TSO_ALL/bclwdww000.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ void isync()

int __unbuffered_cnt = 0;
int __unbuffered_p0_r1 = 0;
int __unbuffered_p0_r3 = 0;
__CPROVER_thread_local int __unbuffered_p0_r3 = 0;
int __unbuffered_p0_r4 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p1_r3 = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_bclwdww000_TSO_OPC/bclwdww000.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ void isync()

int __unbuffered_cnt = 0;
int __unbuffered_p0_r1 = 0;
int __unbuffered_p0_r3 = 0;
__CPROVER_thread_local int __unbuffered_p0_r3 = 0;
int __unbuffered_p0_r4 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p1_r3 = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_bclwdww001_PSO_ALL/bclwdww001.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ void isync()

int __unbuffered_cnt = 0;
int __unbuffered_p0_r1 = 0;
int __unbuffered_p0_r3 = 0;
__CPROVER_thread_local int __unbuffered_p0_r3 = 0;
int __unbuffered_p0_r4 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p1_r3 = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_bclwdww001_PSO_OPC/bclwdww001.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ void isync()

int __unbuffered_cnt = 0;
int __unbuffered_p0_r1 = 0;
int __unbuffered_p0_r3 = 0;
__CPROVER_thread_local int __unbuffered_p0_r3 = 0;
int __unbuffered_p0_r4 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p1_r3 = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_bclwdww001_TSO_ALL/bclwdww001.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ void isync()

int __unbuffered_cnt = 0;
int __unbuffered_p0_r1 = 0;
int __unbuffered_p0_r3 = 0;
__CPROVER_thread_local int __unbuffered_p0_r3 = 0;
int __unbuffered_p0_r4 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p1_r3 = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_bclwdww001_TSO_OPC/bclwdww001.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ void isync()

int __unbuffered_cnt = 0;
int __unbuffered_p0_r1 = 0;
int __unbuffered_p0_r3 = 0;
__CPROVER_thread_local int __unbuffered_p0_r3 = 0;
int __unbuffered_p0_r4 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p1_r3 = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_bclwdww003_PSO_ALL/bclwdww003.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ void isync()

int __unbuffered_cnt = 0;
int __unbuffered_p0_r1 = 0;
int __unbuffered_p0_r3 = 0;
__CPROVER_thread_local int __unbuffered_p0_r3 = 0;
int __unbuffered_p0_r4 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p1_r3 = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_bclwdww003_PSO_OPC/bclwdww003.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ void isync()

int __unbuffered_cnt = 0;
int __unbuffered_p0_r1 = 0;
int __unbuffered_p0_r3 = 0;
__CPROVER_thread_local int __unbuffered_p0_r3 = 0;
int __unbuffered_p0_r4 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p1_r3 = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_bclwdww003_RMO_ALL/bclwdww003.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ void isync()

int __unbuffered_cnt = 0;
int __unbuffered_p0_r1 = 0;
int __unbuffered_p0_r3 = 0;
__CPROVER_thread_local int __unbuffered_p0_r3 = 0;
int __unbuffered_p0_r4 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p1_r3 = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_bclwdww003_RMO_OPC/bclwdww003.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ void isync()

int __unbuffered_cnt = 0;
int __unbuffered_p0_r1 = 0;
int __unbuffered_p0_r3 = 0;
__CPROVER_thread_local int __unbuffered_p0_r3 = 0;
int __unbuffered_p0_r4 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p1_r3 = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_bclwdww003_TSO_ALL/bclwdww003.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ void isync()

int __unbuffered_cnt = 0;
int __unbuffered_p0_r1 = 0;
int __unbuffered_p0_r3 = 0;
__CPROVER_thread_local int __unbuffered_p0_r3 = 0;
int __unbuffered_p0_r4 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p1_r3 = 0;
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-instrument-wmm-core/ppc_bclwdww003_TSO_OPC/bclwdww003.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ void isync()

int __unbuffered_cnt = 0;
int __unbuffered_p0_r1 = 0;
int __unbuffered_p0_r3 = 0;
__CPROVER_thread_local int __unbuffered_p0_r3 = 0;
int __unbuffered_p0_r4 = 0;
int __unbuffered_p1_r1 = 0;
int __unbuffered_p1_r3 = 0;
Expand Down
Loading
Loading