Skip to content

[TG-9189] Value retriever: Allow @nondetLength field to be false. #5043

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
Aug 27, 2019
Merged

[TG-9189] Value retriever: Allow @nondetLength field to be false. #5043

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
11 changes: 8 additions & 3 deletions jbmc/src/java_bytecode/assignments_from_json.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -199,9 +199,14 @@ static bool has_nondet_length(const jsont &json)
/// (typed vs. untyped).
static jsont get_untyped(const jsont &json, const std::string &object_key)
{
if(get_type(json) || has_nondet_length(json))
return json[object_key];
return json;
if(!json.is_object())
Copy link
Contributor

Choose a reason for hiding this comment

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

Are you really expecting just any old thing here when it's not an object, or do you expect something specific, such as null for example? If so, check for your expectation.

Copy link
Contributor

Choose a reason for hiding this comment

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

@smowton It could be pretty much anything so I think this change makes sense.

return json;

const auto &json_object = to_json_object(json);
PRECONDITION(
get_type(json) || json_object.find("@nondetLength") != json_object.end());
Copy link
Contributor

@antlechner antlechner Aug 21, 2019 •
edited
Loading

Choose a reason for hiding this comment

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

⛏️ We could be more precise and assert the current precondition only if json is contains a json_arrayt, and assert only get_type(json) otherwise, as we wouldn't expect a @nondetLength key on e.g. a number or boolean. But then again in the current version we would just ignore such @nondetLength keys, which wouldn't cause any harm.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

precondition is split

Copy link
Contributor Author

Choose a reason for hiding this comment

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

This introduced problems, so I reverted to the initial solution.


return json[object_key];
}

/// \ref get_untyped for primitive types.
Expand Down