Skip to content

Conversation

@sim642
Copy link
Member

@sim642 sim642 commented Jun 23, 2022

This PR consists of a small set of fixes I made locally when I merged together #759, #762 and #742, and tried running the combination on pthread bench. Now that all three are merged, I can submit these.

  • The change of get_ikind is related to that now being used in Apron on mistyped alloc variables. Otherwise those void variables got the default IInt kind, which caused an incompatible ikinds crash in the meet of EvalInt query results.
  • The change of mkCast is similar but applies to the cast being added in base int invariants.

@sim642 sim642 added the bug label Jun 23, 2022
@sim642 sim642 requested a review from jerhard June 23, 2022 13:41
Comment on lines -325 to -327
| _ ->
Messages.warn "Something that we expected to be an integer type has a different type, assuming it is an IInt";
Cil.IInt
Copy link
Member Author

Choose a reason for hiding this comment

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

This default IInt ikind caused some mismatches in query result meets. Here I've replaced it with an exception and all our tests still pass. Although I don't know why the IInt default existed, as opposed to an exception. get_ikind (and get_ikind_exp) are somewhat extensively used, which made me worry about changing this.

Copy link
Member

Choose a reason for hiding this comment

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

It seems reasonable to throw an exception when get_ikind is applied to a type that is not a int, enum, or pointer. In case we will encounter some uncaught exceptions caused by this in the future, there probably needs to be some handling specific to the call-site of get_ikind, anyway.

Copy link
Member Author

Choose a reason for hiding this comment

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

Exactly! Having the exception immediately here makes it much easier to track down from the backtrace as opposed to the ikind flowing through bunch of other code before crashing at an unrelated place.

@sim642 sim642 merged commit 2860a13 into master Jun 24, 2022
@sim642 sim642 deleted the apron-ikind branch June 24, 2022 13:14
@sim642 sim642 added this to the v2.0.0 milestone Aug 12, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants