Skip to content

[CONTRACTS] Allow loop contracts annotated to goto statement #8281

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Jun 17, 2024
Merged

[CONTRACTS] Allow loop contracts annotated to goto statement #8281

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 10 additions & 8 deletions src/ansi-c/goto-conversion/goto_convert.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1004,13 +1004,12 @@ void goto_convertt::convert_assume(

void goto_convertt::convert_loop_contracts(
const codet &code,
goto_programt::targett loop,
const irep_idt &mode)
goto_programt::targett loop)
{
auto assigns = static_cast<const unary_exprt &>(code.find(ID_C_spec_assigns));
if(assigns.is_not_nil())
{
PRECONDITION(loop->is_goto());
PRECONDITION(loop->is_goto() || loop->is_incomplete_goto());
loop->condition_nonconst().add(ID_C_spec_assigns).swap(assigns.op());
}

Expand All @@ -1024,7 +1023,7 @@ void goto_convertt::convert_loop_contracts(
"Loop invariant is not side-effect free.", code.find_source_location());
}

PRECONDITION(loop->is_goto());
PRECONDITION(loop->is_goto() || loop->is_incomplete_goto());
loop->condition_nonconst().add(ID_C_spec_loop_invariant).swap(invariant);
}

Expand All @@ -1039,7 +1038,7 @@ void goto_convertt::convert_loop_contracts(
code.find_source_location());
}

PRECONDITION(loop->is_goto());
PRECONDITION(loop->is_goto() || loop->is_incomplete_goto());
loop->condition_nonconst().add(ID_C_spec_decreases).swap(decreases_clause);
}
}
Expand Down Expand Up @@ -1123,7 +1122,7 @@ void goto_convertt::convert_for(
goto_programt::make_goto(u, true_exprt(), code.source_location()));

// assigns clause, loop invariant and decreases clause
convert_loop_contracts(code, y, mode);
convert_loop_contracts(code, y);

dest.destructive_append(sideeffects);
dest.destructive_append(tmp_v);
Expand Down Expand Up @@ -1181,7 +1180,7 @@ void goto_convertt::convert_while(
convert(code.body(), tmp_x, mode);

// assigns clause, loop invariant and decreases clause
convert_loop_contracts(code, y, mode);
convert_loop_contracts(code, y);

dest.destructive_append(tmp_branch);
dest.destructive_append(tmp_x);
Expand Down Expand Up @@ -1250,7 +1249,7 @@ void goto_convertt::convert_dowhile(
y->complete_goto(w);

// assigns_clause, loop invariant and decreases clause
convert_loop_contracts(code, y, mode);
convert_loop_contracts(code, y);

dest.destructive_append(tmp_w);
dest.destructive_append(sideeffects);
Expand Down Expand Up @@ -1512,6 +1511,9 @@ void goto_convertt::convert_goto(const code_gotot &code, goto_programt &dest)
goto_programt::targett t =
dest.add(goto_programt::make_incomplete_goto(code, code.source_location()));

// Loop contracts annotated in GOTO
convert_loop_contracts(code, t);

// remember it to do the target later
targets.gotos.emplace_back(t, targets.scope_stack.get_current_node());
}
Expand Down
5 changes: 1 addition & 4 deletions src/ansi-c/goto-conversion/goto_convert_class.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -241,10 +241,7 @@ class goto_convertt : public messaget
goto_programt &dest,
const irep_idt &mode);
void convert_cpp_delete(const codet &code, goto_programt &dest);
void convert_loop_contracts(
const codet &code,
goto_programt::targett loop,
const irep_idt &mode);
void convert_loop_contracts(const codet &code, goto_programt::targett loop);
void
convert_for(const code_fort &code, goto_programt &dest, const irep_idt &mode);
void convert_while(
Expand Down
Loading