Skip to content

Use correct type for pointer checks in contracts #6164

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.

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

Merged
merged 1 commit into from
Jun 5, 2021

Conversation

SaswatPadhi
Copy link
Contributor

Resolves #6106.

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

@SaswatPadhi SaswatPadhi added bugfix aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts labels Jun 4, 2021
@SaswatPadhi SaswatPadhi requested a review from feliperodri June 4, 2021 22:23
@SaswatPadhi SaswatPadhi self-assigned this Jun 4, 2021
@SaswatPadhi SaswatPadhi requested a review from tautschnig as a code owner June 4, 2021 22:23
@SaswatPadhi SaswatPadhi force-pushed the assigns_w_ok_bug_fix branch from 09b87ec to b5873c9 Compare June 4, 2021 22:50
@SaswatPadhi SaswatPadhi force-pushed the assigns_w_ok_bug_fix branch from b5873c9 to 45cb253 Compare June 4, 2021 23:05
Copy link
Collaborator

@feliperodri feliperodri left a comment

Choose a reason for hiding this comment

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

Perfect! 👯

@codecov
Copy link

codecov bot commented Jun 4, 2021

Codecov Report

Merging #6164 (09b87ec) into develop (538070c) will increase coverage by 0.09%.
The diff coverage is 100.00%.

❗ Current head 09b87ec differs from pull request most recent head 45cb253. Consider uploading reports for the commit 45cb253 to get more accurate results
Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #6164      +/-   ##
===========================================
+ Coverage    74.95%   75.04%   +0.09%     
===========================================
  Files         1450     1450              
  Lines       158274   158274              
===========================================
+ Hits        118632   118782     +150     
+ Misses       39642    39492     -150     
Impacted Files Coverage Δ
src/goto-instrument/code_contracts.cpp 85.40% <100.00%> (ø)
src/util/expr.cpp 74.01% <0.00%> (-0.79%) ⬇️
src/util/simplify_expr.cpp 84.71% <0.00%> (-0.47%) ⬇️
src/ansi-c/expr2c.cpp 69.10% <0.00%> (-0.10%) ⬇️
src/util/json.cpp 87.38% <0.00%> (+1.80%) ⬆️
src/ansi-c/c_typecheck_type.cpp 76.38% <0.00%> (+12.84%) ⬆️
src/ansi-c/ansi_c_entry_point.cpp 87.44% <0.00%> (+21.39%) ⬆️

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 f5f965a...45cb253. Read the comment docs.

@SaswatPadhi SaswatPadhi merged commit 9539a51 into diffblue:develop Jun 5, 2021
@SaswatPadhi SaswatPadhi deleted the assigns_w_ok_bug_fix branch June 5, 2021 00:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
aws Bugs or features of importance to AWS CBMC users bugfix Code Contracts Function and loop contracts
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Suport for char variables in __CPROVER_w_ok()
2 participants