Skip to content

Replace requires with c_requires #7698

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 1 commit into from
May 12, 2023
Merged

Replace requires with c_requires #7698

merged 1 commit into from
May 12, 2023

Conversation

TGWDB
Copy link
Contributor

@TGWDB TGWDB commented May 3, 2023 •
edited
Loading

Fixes #7656

  • 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.
  • 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).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@feliperodri feliperodri added cleanup aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts labels May 3, 2023
@codecov
Copy link

codecov bot commented May 3, 2023 •
edited
Loading

Codecov Report

Patch coverage: 100.00% and no project coverage change.

Comparison is base (56bf6c1) 78.55% compared to head (3a6cef0) 78.55%.

Additional details and impacted files 
@@           Coverage Diff            @@
##           develop    #7698   +/-   ##
========================================
  Coverage    78.55%   78.55%           
========================================
  Files         1686     1686           
  Lines       192915   192917    +2     
========================================
+ Hits        151539   151541    +2     
  Misses       41376    41376
Impacted Files Coverage Δ
src/ansi-c/ansi_c_convert_type.h 100.00% <ø> (ø)
...contracts/dynamic-frames/dfcc_contract_functions.h 100.00% <ø> (ø)
src/ansi-c/ansi_c_convert_type.cpp 79.95% <100.00%> (ø)
src/ansi-c/c_typecheck_base.cpp 83.26% <100.00%> (ø)
src/cprover/instrument_contracts.cpp 90.51% <100.00%> (ø)
src/goto-instrument/contracts/contracts.cpp 94.81% <100.00%> (+0.01%) ⬆️
...ntracts/dynamic-frames/dfcc_contract_functions.cpp 100.00% <100.00%> (ø)
.../contracts/dynamic-frames/dfcc_wrapper_program.cpp 96.31% <100.00%> (ø)
src/linking/remove_internal_symbols.cpp 100.00% <100.00%> (ø)
src/util/c_types.h 100.00% <100.00%> (ø)

☔ View full report in Codecov by Sentry.
📢 Do you have feedback about the report comment? Let us know in this issue.

tautschnig
tautschnig requested changes May 4, 2023
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.

While this will make the change slightly larger than strictly necessary: can we please have consistent naming for all code contract components? If we use c_requires, then we should also have c_ensures.

@remi-delmas-3000
Copy link
Collaborator

there's also assigns->c_assigns, frees->c_frees

@TGWDB TGWDB requested a review from martin-cs as a code owner May 11, 2023 08:40
@TGWDB TGWDB force-pushed the 20230503-rename-requires branch 2 times, most recently from d0427d4 to 14baca8 Compare May 11, 2023 09:24
@feliperodri feliperodri requested a review from tautschnig May 11, 2023 17:48
tautschnig
tautschnig approved these changes May 12, 2023
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.

I would appreciate some squashing of commits.

@TGWDB
Prefix requires, assigns, frees, and ensures.
3a6cef0 
Fixes #7675

Adds the "c_" prefix to the requires, assigns, frees, and ensures
for consistency.
@TGWDB TGWDB force-pushed the 20230503-rename-requires branch from 14baca8 to 3a6cef0 Compare May 12, 2023 13:52
@feliperodri feliperodri enabled auto-merge May 12, 2023 17:43
@feliperodri
Copy link
Collaborator

@TGWDB there is a JBMC test failure (218 - jbmc-CORE (Failed)). Apart from it, it looks ready to merge.

@feliperodri feliperodri merged commit ba47c86 into develop May 12, 2023
@tautschnig tautschnig deleted the 20230503-rename-requires branch May 15, 2023 08:00
@jparsert jparsert mentioned this pull request Jun 4, 2023
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tautschnig tautschnig tautschnig approved these changes

@feliperodri feliperodri feliperodri approved these changes

@remi-delmas-3000 remi-delmas-3000 Awaiting requested review from remi-delmas-3000 remi-delmas-3000 is a code owner

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

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

@chris-ryder chris-ryder Awaiting requested review from chris-ryder

@martin-cs martin-cs Awaiting requested review from martin-cs

Assignees

@TGWDB TGWDB

Labels
aws Bugs or features of importance to AWS CBMC users cleanup Code Contracts Function and loop contracts
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Warning about requires keyword in C++20
4 participants
@TGWDB @remi-delmas-3000 @feliperodri @tautschnig