Skip to content

Commit 309d207

Browse files
author
Daniel Kroening
committed
remove conversion for non-deterministic-goto
1 parent f3a3e79 commit 309d207

File tree

1 file changed

+1
-22
lines changed

1 file changed

+1
-22
lines changed

src/goto-programs/goto_convert.cpp

Lines changed: 1 addition & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -109,28 +109,7 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
109109
{
110110
goto_programt::instructiont &i=*(g_it.first);
111111

112-
if(i.code.get_statement()=="non-deterministic-goto")
113-
{
114-
const irept &destinations=i.code.find("destinations");
115-
116-
i.make_goto();
117-
118-
forall_irep(it, destinations.get_sub())
119-
{
120-
labelst::const_iterator l_it=
121-
targets.labels.find(it->id_string());
122-
123-
if(l_it==targets.labels.end())
124-
{
125-
error().source_location=i.code.find_source_location();
126-
error() << "goto label `" << it->id() << "' not found" << eom;
127-
throw 0;
128-
}
129-
130-
i.targets.push_back(l_it->second.first);
131-
}
132-
}
133-
else if(i.is_start_thread())
112+
if(i.is_start_thread())
134113
{
135114
const irep_idt &goto_label=i.code.get(ID_destination);
136115

0 commit comments

Comments
 (0)