Skip to content

Fix bugs in String.indexOf(c) TG-1846 #1668

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 4 commits into from
Dec 20, 2017
Merged

Fix bugs in String.indexOf(c) TG-1846 #1668

Changes from 1 commit
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
28a2ada
Access in empty array should be unconstrained
romainbrenguier Dec 13, 2017
682cd1a
Use a symbol generator to avoid name clashes
romainbrenguier Dec 14, 2017
9a7fa2d
Correct lower bound in String indexOf
romainbrenguier Dec 14, 2017
f3b4c9b
Test for verification of the indexOf method
romainbrenguier Dec 13, 2017
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
10 changes: 8 additions & 2 deletions src/solvers/refinement/string_refinement.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1076,6 +1076,8 @@ exprt fill_in_array_expr(const array_exprt &expr, std::size_t string_max_length)
/// expression will be: `index==0 ? 24 : index==2 ? 42 : 12`
/// * for an array access `(g1?arr1:arr2)[x]` where `arr1 := {12}` and
/// `arr2 := {34}`, the constructed expression will be: `g1 ? 12 : 34`
/// * for an access in an empty array `{ }[x]` returns a fresh symbol, this
/// corresponds to a non-deterministic result
/// \param expr: an expression containing array accesses
/// \return an expression containing no array access
static void substitute_array_access(exprt &expr)
Expand Down Expand Up @@ -1124,13 +1126,17 @@ static void substitute_array_access(exprt &expr)
"above"));
array_exprt &array_expr=to_array_expr(index_expr.array());

// Empty arrays do not need to be substituted.
const typet &char_type = index_expr.array().type().subtype();

// Access to an empty array is undefined (non deterministic result)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why? Where do you recognise that this should throw an exception in java?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@peterschrammel The exception is (intended) to be thrown at the model level. That's now the contract of the string methods in jbmc. I'm not sure whether this is sufficiently clearly stated, though.

if(array_expr.operands().empty())
{
expr = symbol_exprt("out_of_bound_access", char_type);
return;
}

size_t last_index=array_expr.operands().size()-1;

const typet &char_type=index_expr.array().type().subtype();
exprt ite=array_expr.operands().back();

if(ite.type()!=char_type)
Expand Down