Skip to content

goto_check_c: observe check pragmas annotated to individual expressions #6616

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
Open
wants to merge 2 commits into
base: develop
Choose a base branch
from
Open

goto_check_c: observe check pragmas annotated to individual expressions #6616

wants to merge 2 commits into from

Conversation

tautschnig
Copy link
Collaborator

@tautschnig tautschnig commented Jan 30, 2022 •
edited
Loading

This is required to make the conversion of __builtin_X_overflow not generate spurious conversion checks.

Please review commit-by-commit.

Fixes: #6452

  • 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.

@tautschnig tautschnig force-pushed the bugfix/overflow-conversion-check branch 2 times, most recently from a5af87c to 0b099d0 Compare January 30, 2022 21:49
@codecov
Copy link

codecov bot commented Jan 30, 2022 •
edited
Loading

Codecov Report

Merging #6616 (25d3a9c) into develop (afc53d8) will increase coverage by 0.00%.
The diff coverage is 100.00%.

Impacted file tree graph

@@           Coverage Diff            @@
##           develop    #6616   +/-   ##
========================================
  Coverage    76.73%   76.73%           
========================================
  Files         1579     1579           
  Lines       181999   182016   +17     
========================================
+ Hits        139652   139671   +19     
+ Misses       42347    42345    -2
Impacted Files Coverage Δ
src/analyses/goto_check_c.cpp 90.92% <100.00%> (+0.11%) ⬆️
src/ansi-c/ansi_c_parser.cpp 90.26% <100.00%> (+1.87%) ⬆️
src/goto-programs/goto_convert_side_effect.cpp 95.66% <100.00%> (+0.03%) ⬆️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 3f175c9...25d3a9c. Read the comment docs.

chris-ryder
chris-ryder approved these changes Feb 5, 2022
View reviewed changes
Copy link

@chris-ryder chris-ryder left a comment

Choose a reason for hiding this comment

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

Looks sensible to me.

@chris-ryder chris-ryder removed their assignment Feb 5, 2022
@tautschnig tautschnig force-pushed the bugfix/overflow-conversion-check branch from 0b099d0 to 577cfee Compare February 6, 2022 22:37
@tautschnig
C front-end: pragma conflict checking must handle empty stack
120f525 
We do not necessarily have any pragmas set, and therefore must be able
to handle an empty stack.

Surprisingly, this only seg faulted when building in exactly the way
check-ubuntu-20_04-make-gcc is doing this in CI, and only on one test
added in the next commit.
@tautschnig
goto_check_c: observe check pragmas annotated to individual expressions
25d3a9c 
This is required to make the conversion of __builtin_X_overflow not
generate spurious conversion checks.

Fixes: diffblue#6452
@tautschnig tautschnig force-pushed the bugfix/overflow-conversion-check branch from 577cfee to 25d3a9c Compare February 7, 2022 21:27
@tautschnig tautschnig mentioned this pull request Feb 10, 2022
Open
3 tasks
This was referenced Feb 24, 2022
Closed
Closed
@feliperodri feliperodri added the aws Bugs or features of importance to AWS CBMC users label Oct 6, 2022
@feliperodri feliperodri added the Kani Bugs or features of importance to Kani Rust Verifier label Nov 2, 2022
@jimgrundy
Copy link
Collaborator

Where are we on this one?
It seems like there is a fairly straightforward work-around to not having this, which is to have a statement assigning the sub-expression to a temporary variable and wrapping that statement in a pragma. Am I wrong about that?
Is this easy and non-disruptive to CBMC? If so, can we check it in? If not, is it worth doing if there is a simple work around?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@chris-ryder chris-ryder chris-ryder approved these changes

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

@kroening kroening Awaiting requested review from kroening kroening is a code owner

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

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

At least 1 approving review is required to merge this pull request.

Assignees

@tautschnig tautschnig

Labels
aws Bugs or features of importance to AWS CBMC users blocker bugfix Kani Bugs or features of importance to Kani Rust Verifier Property Instrumentation
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

pragma check disable does not work as expected
8 participants
@tautschnig @jimgrundy @chris-ryder @kroening @peterschrammel @feliperodri @martin-cs @chrisr-diffblue