From c6c5fb9c58ff51817502ba8884ef0c7eb769e2cc Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Tue, 25 Aug 2015 16:19:20 +0200 Subject: [PATCH] [mc] Add tests to show that DPOR is guilty of mutex mis-handling In fact SIMCALL_MUTEX_LOCK is handled but not in DPOR. --- tools/cmake/AddTests.cmake | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/tools/cmake/AddTests.cmake b/tools/cmake/AddTests.cmake index dca967f2be..ebdd393c13 100644 --- a/tools/cmake/AddTests.cmake +++ b/tools/cmake/AddTests.cmake @@ -101,8 +101,10 @@ IF(NOT enable_memcheck) ADD_TESH(tesh-mc-dwarf --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/dwarf --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/dwarf dwarf.tesh) ADD_TESH(tesh-mc-dwarf-expression --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/dwarf_expression --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/dwarf_expression dwarf_expression.tesh) - ADD_TESH(tesh-mc-mutex-handling --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc mutex_handling.tesh) - ADD_TESH(tesh-mc-no-mutex-handling --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc no_mutex_handling.tesh) + ADD_TESH(tesh-mc-mutex-handling --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc mutex_handling.tesh --cfg=model-check/reduction:none) + ADD_TESH(tesh-mc-mutex-handling-dpor --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc mutex_handling.tesh --cfg=model-check/reduction:dpor) + ADD_TESH(tesh-mc-no-mutex-handling --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc no_mutex_handling.tesh --cfg=model-check/reduction:none) + ADD_TESH(tesh-mc-no-mutex-handling-dpor --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc no_mutex_handling.tesh --cfg=model-check/reduction:dpor) ADD_TESH(mc-record-random-bug --setenv bindir=${CMAKE_BINARY_DIR}/teshsuite/mc/replay --setenv srcdir=${CMAKE_HOME_DIRECTORY}/teshsuite/mc/replay --cd ${CMAKE_HOME_DIRECTORY}/teshsuite/mc/replay random_bug.tesh) -- 2.20.1