Skip to content

Commit 81fb2f2

Browse files
smowtontautschnig
authored andcommitted
Don't treat a dead instruction as a shared write
Doing so introduces an extra (nondet) generation of the symbol, which the test anonymous-java.lang.thread treats as an opportunity to fail its test by hypothesising that the main thread ends (and kills the temporary instance of A that the variable under test belongs to) before the worker thread starts. Arguably this is wrong -- the variable is stack-allocated, so either we should join all threads before returning from "main" or we shouldn't use stack allocation for Java objects at all -- but this simply restores symex's behaviour before field sensitivity was added, and thus is hopefully uncontroversial.
1 parent 3cd28cb commit 81fb2f2

File tree

1 file changed

+0
-12
lines changed

1 file changed

+0
-12
lines changed

src/goto-symex/symex_dead.cpp

Lines changed: 0 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -63,17 +63,5 @@ void goto_symext::symex_dead(statet &state)
6363
auto level2_it = state.level2.current_names.find(l1_identifier);
6464
if(level2_it != state.level2.current_names.end())
6565
symex_renaming_levelt::increase_counter(level2_it);
66-
67-
const bool record_events = state.record_events;
68-
state.record_events = false;
69-
state.rename(ssa_lhs, ns);
70-
state.record_events = record_events;
71-
72-
if(
73-
state.dirty(ssa_lhs.get_object_name()) && state.atomic_section_id == 0)
74-
{
75-
target.shared_write(
76-
state.guard.as_expr(), ssa_lhs, state.atomic_section_id, state.source);
77-
}
7866
}
7967
}

0 commit comments

Comments
 (0)