replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
diffblue-cbmc/regression/cbmc-concurrency
History
Michael Tautschnig eaa7d93ac4 Skip phi assignment if one of the merged states has an uninitialised object 
With level-2 counters incremented on declaration and non-deterministic
initialisation upon allocation, the only remaining sources are pointer
dereferencing, where uninitialised objects necessarily refer to invalid objects.

This is a cleaner implementation of 369f077d2e. Removing only the code
introduced in 369f077d2e would yield a wrong result for
regression/cbmc/Local_out_of_scope3.

Fixes: #1630
 		2018-12-19 17:03:06 +00:00
..
assume1 regressions from Michael 2013-04-05 15:09:52 +00:00
assume2 regressions from Michael 2013-04-05 15:09:52 +00:00
atomic_section_sc1 fixes for concurrency regressions 2013-06-29 11:31:34 +00:00
atomic_section_sc2 fixes for concurrency regressions 2013-06-29 11:31:34 +00:00
atomic_section_sc3 Normalise newlines at ends of files 2016-11-29 09:59:31 +00:00
atomic_section_sc4 Normalise newlines at ends of files 2016-11-29 09:59:31 +00:00
atomic_section_sc5 Removed spurious linefeeds 2014-01-18 15:55:24 +00:00
atomic_section_sc6 fix expected output 2016-08-18 11:37:48 +01:00
conditional_spawn1 Normalise newlines at ends of files 2016-11-29 09:59:31 +00:00
conditional_spawn2 Normalise newlines at ends of files 2016-11-29 09:59:31 +00:00
constant_prop1 Modified tests to pass without using grep 2017-02-14 17:29:15 +00:00
deadlock1 Remove trailing whitespace from all lines 2016-11-29 09:58:36 +00:00
deadlock2 Remove trailing whitespace from all lines 2016-11-29 09:58:36 +00:00
dirty_local1 Treat local dirty variables as shared ones 2017-01-25 21:10:32 +00:00
dirty_local2 Treat local dirty variables as shared ones 2017-01-25 21:10:32 +00:00
generic_hw_sw_benchmark1 Concurrency-related tests compiled by Alex Horn 2014-08-08 12:47:50 +00:00
global_pointer1 Normalise newlines at ends of files 2016-11-29 09:59:31 +00:00
graphml_witness1 Fix graphml output of concurrency witnesses 2017-10-24 13:33:30 +01:00
if1 Normalise newlines at ends of files 2016-11-29 09:59:31 +00:00
invalid_object1 Normalise newlines at ends of files 2016-11-29 09:59:31 +00:00
loop_unwinding1 Normalise newlines at ends of files 2016-11-29 09:59:31 +00:00
malloc1 regressions from Michael 2013-04-05 15:09:52 +00:00
malloc2 symex_dynamic::dynamic_object_size* are constants 2018-04-25 21:36:47 +01:00
memory_barrier1 Normalise newlines at ends of files 2016-11-29 09:59:31 +00:00
memory_barrier2 Normalise newlines at ends of files 2016-11-29 09:59:31 +00:00
mutex1 more regressions 2013-04-05 15:35:48 +00:00
mutex2 more regressions 2013-04-05 15:35:48 +00:00
norace_array1 more line terminators 2016-09-17 11:15:22 +01:00
norace_array2 test from Lucas 2016-07-25 08:36:18 +01:00
norace_scalar1 more line terminators 2016-09-17 11:15:22 +01:00
norace_struct1 more line terminators 2016-09-17 11:15:22 +01:00
pthread_create_tso1 Remove trailing whitespace from all lines 2016-11-29 09:58:36 +00:00
pthread_join1 tests: drop number of iterations 2017-10-27 21:19:08 +02:00
pthread_join2 Remove trailing whitespace from all lines 2016-11-29 09:58:36 +00:00
recursion1 Normalise newlines at ends of files 2016-11-29 09:59:31 +00:00
sc1 basic concurrency regressions 2013-03-31 15:06:58 +00:00
sc2 Normalise newlines at ends of files 2016-11-29 09:59:31 +00:00
sc3 Remove trailing whitespace from all lines 2016-11-29 09:58:36 +00:00
sc4 Remove trailing whitespace from all lines 2016-11-29 09:58:36 +00:00
sc5 more 2013-04-05 14:40:27 +00:00
sc6 Normalise newlines at ends of files 2016-11-29 09:59:31 +00:00
sc7 regressions from Michael 2013-04-05 15:09:52 +00:00
sc8 Remove trailing whitespace from all lines 2016-11-29 09:58:36 +00:00
stack1 two new cbmc concurrency regression tests 2016-11-14 12:29:51 +00:00
struct_and_array1 Remove trailing whitespace from all lines 2016-11-29 09:58:36 +00:00
svcomp13_fib_bench_longer_safe fixes for concurrency regressions 2013-06-29 11:31:34 +00:00
svcomp13_fib_bench_longer_unsafe fixes for concurrency regressions 2013-06-29 11:31:34 +00:00
svcomp13_qrcu_safe Remove trailing whitespace from all lines 2016-11-29 09:58:36 +00:00
svcomp13_qrcu_unsafe Remove trailing whitespace from all lines 2016-11-29 09:58:36 +00:00
svcomp13_read_write_lock_safe Normalise newlines at ends of files 2016-11-29 09:59:31 +00:00
thread_chain_cbmc1 Concurrency-related tests compiled by Alex Horn 2014-08-08 12:47:50 +00:00
thread_chain_cbmc2 Concurrency-related tests compiled by Alex Horn 2014-08-08 12:47:50 +00:00
thread_chain_posix1 Remove trailing whitespace from all lines 2016-11-29 09:58:36 +00:00
thread_chain_posix2 Abort concurrency encoding in possibly unsound cases 2018-06-14 09:17:30 +00:00
thread_chain_posix3 Abort concurrency encoding in possibly unsound cases 2018-06-14 09:17:30 +00:00
thread_group_cbmc1 Concurrency-related tests compiled by Alex Horn 2014-08-08 12:47:50 +00:00
thread_group_cbmc2 Concurrency-related tests compiled by Alex Horn 2014-08-08 12:47:50 +00:00
thread_group_cbmc3 Concurrency-related tests compiled by Alex Horn 2014-08-08 12:47:50 +00:00
thread_group_cbmc4 Concurrency-related tests compiled by Alex Horn 2014-08-08 12:47:50 +00:00
thread_local1 Normalise newlines at ends of files 2016-11-29 09:59:31 +00:00
thread_local2 Skip phi assignment if one of the merged states has an uninitialised object 2018-12-19 17:03:06 +00:00
trace1 Fix concurrent traces generated via --trace 2017-03-30 14:00:01 +01:00
uf_with_threads1 Remove trailing whitespace from all lines 2016-11-29 09:58:36 +00:00
Makefile merge fixes 2017-04-03 16:57:59 +01:00