Skip to content

Conversation

NlightNFotis
Copy link
Contributor

During the work performed for case statement support in gnat2goto (#171) it was discovered that we do support case expressions already, but it's not a documented nor tested feature. This adds some basic tests for this, and fixes any problems discovered.

@NlightNFotis NlightNFotis self-assigned this Mar 28, 2019
@NlightNFotis NlightNFotis marked this pull request as ready for review March 28, 2019 15:14
@NlightNFotis
Copy link
Contributor Author

This is now ready for review. Works reliably, but has the same limitation as #171, in that the cases where there's a range in the condition don't work. This has been described better in #181 .

Copy link
Contributor

@xbauch xbauch left a comment

Choose a reason for hiding this comment

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

Looks good.

Copy link
Contributor

Choose a reason for hiding this comment

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

Please add the function indirection I mentioned before merging

@@ -0,0 +1 @@
ALL XFAIL CBMC crashes with first argument of if must be boolean, but got or
Copy link
Contributor

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue Mar 29, 2019

Choose a reason for hiding this comment

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

can you squash this together with the commit fixing this so you can remove it?

begin
Result := (case Random_Val is
when 1..10 => 1,
when 11..20 => 2,

Choose a reason for hiding this comment

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

I suspect handling a range expression should be fairly easy - a literal range should always be translatable like this x in a..b ===> a <= x and x <= b I'd think

@NlightNFotis NlightNFotis merged commit 707415a into diffblue:master Apr 1, 2019
@NlightNFotis NlightNFotis deleted the fix_case_statement_expressions branch April 1, 2019 09:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants