Skip to content

deprecate exprt::make_typecast(type) #3856

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 3 commits into from
Jan 23, 2019
Merged

deprecate exprt::make_typecast(type) #3856

merged 3 commits into from
Jan 23, 2019

Conversation

kroening
Copy link
Member

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a 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.

@kroening kroening force-pushed the make_typecast branch 2 times, most recently from 29a3eed to d1cdcea Compare January 19, 2019 21:19
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: d1cdcea).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97936959

tautschnig
tautschnig approved these changes Jan 21, 2019
View reviewed changes
Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

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

Some comments below with one additional nit-pick: the commit messages have typos (s/save/safe/).

src/pointer-analysis/goto_program_dereference.cpp Outdated

if(tmp.type()!=expr.type())
tmp.make_typecast(expr.type());
tmp = typecast_exprt::conditional_cast(tmp, expr.type());

expr.swap(tmp);
Copy link
Collaborator

Choose a reason for hiding this comment

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

I think that's expr = typecast_exprt::conditional_cast(expr.op0().op0(), expr.type());

Copy link
Member Author

Choose a reason for hiding this comment

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

sure

src/solvers/flattening/arrays.cpp Outdated
make_typecast(indices_equal.op0().type());
}
indices_equal.op1() = typecast_exprt::conditional_cast(
indices_equal.op1(), indices_equal.op0().type());
Copy link
Collaborator

Choose a reason for hiding this comment

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

I'd put this right in the constructor:
equal_exprt indices_equal(*i1, typecast_exprt::conditional_cast(*i2, i1->type()));

Copy link
Member Author

Choose a reason for hiding this comment

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

done

src/util/pointer_predicates.cpp Outdated
object_offset.make_typecast(access_size.type());
sum=plus_exprt(object_offset, access_size);
const auto object_offset_casted =
typecast_exprt::conditional_cast(object_offset, access_size.type());
Copy link
Collaborator

Choose a reason for hiding this comment

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

I'm not entirely happy with this happening here - on the one hand because it's already being done in 8f52d81, and on the other hand because it does only one part of the work (it doesn't remove ns from the parameter list).

@kroening kroening force-pushed the make_typecast branch 2 times, most recently from b99beb8 to f4b91a8 Compare January 22, 2019 08:28
@kroening kroening assigned peterschrammel and unassigned kroening Jan 22, 2019
allredj
allredj reviewed Jan 22, 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.

🚫
This PR failed Diffblue compatibility checks (cbmc commit: b99beb8).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98135668
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

  • the cbmc commit has disappeared in the mean time (e.g. in a force-push)
  • the author is not in the list of contributors (e.g. first-time contributors).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj
allredj reviewed Jan 22, 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: f4b91a8).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98138802

@kroening kroening mentioned this pull request Jan 22, 2019
Merged
4 tasks
Daniel Kroening added 2 commits January 23, 2019 18:49
@tautschnig
deprecate exprt::make_typecast()
c3ec380 
This is fundamentally not type-safe; the type of the expression will change.
The compiler is unable to assert memory safety.
@tautschnig
use typecast_exprt() instead of .make_typecast
624ff6c 
.make_typecast() isn't type safe; use the constructor for the
resulting expression instead.
@tautschnig
use typecast_exprt::conditional_cast
49b0670 
.make_typecast() isn't type safe; when used in the pattern
if(a.type()!=b.type()) ... then use typecast_exprt::conditional_cast
instead.
@tautschnig
Copy link
Collaborator

Rebased to resolve conflicts.

allredj
allredj reviewed Jan 23, 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: 49b0670).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98376149

@tautschnig tautschnig merged commit 65cfed1 into develop Jan 23, 2019
@tautschnig tautschnig deleted the make_typecast branch January 23, 2019 21:55
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

@thk123 thk123 thk123 approved these changes

@tautschnig tautschnig tautschnig 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

@pkesseli pkesseli Awaiting requested review from pkesseli

@smowton smowton Awaiting requested review from smowton

@cesaro cesaro Awaiting requested review from cesaro

@cristina-david cristina-david Awaiting requested review from cristina-david

@NathanJPhillips NathanJPhillips Awaiting requested review from NathanJPhillips

Assignees

@kroening kroening

Labels
cleanup
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@kroening @tautschnig @thk123 @peterschrammel @allredj