Skip to content

Commit fed5536

Browse files
committed
Fix --nondet-volatile bug where lhs was not considered in assignment
1 parent d58ebd8 commit fed5536

File tree

3 files changed

+21
-1
lines changed

3 files changed

+21
-1
lines changed
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
#include <assert.h>
2+
3+
void main()
4+
{
5+
int a[2] = {0};
6+
7+
volatile int i = 0;
8+
a[i] = 1;
9+
10+
assert(a[1] == 0); // should fail
11+
}
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
test.c
3+
--nondet-volatile
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
--
7+
--
8+
Check that volatile variables appearing in the lhs of an assignment are
9+
correctly treated as nondet

src/goto-instrument/nondet_volatile.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -88,7 +88,7 @@ void nondet_volatile(
8888
if(instruction.is_assign())
8989
{
9090
nondet_volatile_rhs(symbol_table, to_code_assign(instruction.code).rhs());
91-
nondet_volatile_lhs(symbol_table, to_code_assign(instruction.code).rhs());
91+
nondet_volatile_lhs(symbol_table, to_code_assign(instruction.code).lhs());
9292
}
9393
else if(instruction.is_function_call())
9494
{

0 commit comments

Comments
 (0)