replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

fixes for concurrency regressions 

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@2690 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
This commit is contained in:
kroening 2013-06-29 11:31:34 +00:00
parent f165f4aee3
commit ee05f16ecc
4 changed files with 6 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
regression/cbmc-concurrency/atomic_section_sc1/main.c
View File

@ -4,9 +4,9 @@ int main()
{
__CPROVER_ASYNC_1: global=2;
__CPROVER_ATOMIC_BEGIN();
__CPROVER_atomic_begin();
global=1;
// no interleaving here
assert(global==1);
__CPROVER_ATOMIC_END();
__CPROVER_atomic_end();
}

4
regression/cbmc-concurrency/atomic_section_sc2/main.c
View File

@ -6,9 +6,9 @@ int main()
__CPROVER_ASYNC_1: assert(global==1);
__CPROVER_ATOMIC_BEGIN();
__CPROVER_atomic_begin();
global=2;
// no interleaving here
global=1;
__CPROVER_ATOMIC_END();
__CPROVER_atomic_end();
}

2
regression/cbmc-concurrency/svcomp13_fib_bench_longer_safe/test.desc
View File

@ -1,6 +1,6 @@
CORE
main.c
--error-label ERROR
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$

2
regression/cbmc-concurrency/svcomp13_fib_bench_longer_unsafe/test.desc
View File

@ -1,6 +1,6 @@
CORE
main.c
--error-label ERROR
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$