Skip to content

ai_baset: output now requires function identifier [blocks: #3126] #3828

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

Jump to bottom
Merged
merged 4 commits into from
Jan 20, 2019
Merged

ai_baset: output now requires function identifier [blocks: #3126] #3828

merged 4 commits into from
Jan 20, 2019

Conversation

tautschnig
Copy link
Collaborator

We are working towards removing the "function" field from
goto_programt::instructionst::instructiont, and thus need to pass the identifier
of the function whenever it actually is required.

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@smowton
Copy link
Contributor

smowton commented Jan 18, 2019

Are the parameter order changes just for consistency?

smowton
smowton reviewed Jan 18, 2019
View reviewed changes
src/analyses/ai.h Outdated
@@ -124,6 +124,18 @@ class ai_baset
{
}

/// Output the abstract states for a single function
/// \param ns: The namespace
/// \param identifier: The identifier used to find a symbol to identify the
Copy link
Contributor

Choose a reason for hiding this comment

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

to identify the... (copy and paste error?)

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Not really, the next parameter goto_program, is what is being identified here. But that's a bit weird to read. Fixed.

@tautschnig
Copy link
Collaborator Author

Are the parameter order changes just for consistency?

Yes - I've now split this up in three commits.

allredj
allredj reviewed Jan 19, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

✔️
Passed Diffblue compatibility checks (cbmc commit: 500d485).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97924789

peterschrammel
peterschrammel approved these changes Jan 20, 2019
View reviewed changes
Copy link
Member

@peterschrammel peterschrammel left a comment

Choose a reason for hiding this comment

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

LGTM modulo naming

src/analyses/ai.cpp Outdated
@@ -187,12 +187,14 @@ void ai_baset::entry_state(const goto_programt &goto_program)
get_state(goto_program.instructions.begin()).make_entry();
}

void ai_baset::initialize(const goto_functionst::goto_functiont &goto_function)
void ai_baset::initialize(
const irep_idt &function,
Copy link
Member

@peterschrammel peterschrammel Jan 20, 2019 •
edited
Loading

Choose a reason for hiding this comment

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

While doing this could we agree on a consistent name, e.g. function_id, function_identifier, function, function_name or so?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Done (now using function_identifier).

@peterschrammel peterschrammel removed their assignment Jan 20, 2019
tautschnig and others added 4 commits January 20, 2019 18:57
@tautschnig
Make order of arguments in ai_baset::output* consistent
3de66f8 
Place the identifier (the name of the function) before the goto program.
@tautschnig
ai_baset::initialize now requires a function name
cc82d5c 
We are working towards removing the "function" field from
goto_programt::instructionst::instructiont, and thus need to pass the identifier
of the function whenever it actually is required.
@tautschnig
ai_baset: output now requires function identifier
63e00ba 
We are working towards removing the "function" field from
goto_programt::instructionst::instructiont, and thus need to pass the identifier
of the function whenever it actually is required.
@tautschnig
ai_baset: consistently use function_id instead of function_identifier
d7db14f 
It is as clear, but makes for shorter lines.
allredj
allredj reviewed Jan 20, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

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

✔️
Passed Diffblue compatibility checks (cbmc commit: d7db14f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97965595

@tautschnig tautschnig merged commit 4d2a024 into diffblue:develop Jan 20, 2019
@tautschnig tautschnig deleted the function-ai branch January 20, 2019 21:21
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@allredj allredj allredj left review comments

@smowton smowton smowton approved these changes

@peterschrammel peterschrammel peterschrammel approved these changes

@chrisr-diffblue chrisr-diffblue Awaiting requested review from chrisr-diffblue

@martin-cs martin-cs Awaiting requested review from martin-cs martin-cs is a code owner

@thk123 thk123 Awaiting requested review from thk123

Assignees

@martin-cs martin-cs

@chrisr-diffblue chrisr-diffblue

Labels
blocker
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@tautschnig @smowton @peterschrammel @allredj @martin-cs @chrisr-diffblue