Skip to content

CONTRACTS: Drop function pointer contract support #7328

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

Conversation

remi-delmas-3000
Copy link
Collaborator

Dropping support for function pointer contract clauses in the old contract system (now only supported with DFCC).
This feature only makes sense when combined with the ability to use C functions to specify assignable sets, which only
exists in DFCC.

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

Dropping support for function pointer contract clauses
in the old contract system (now only supported with DFCC).
@remi-delmas-3000 remi-delmas-3000 self-assigned this Nov 11, 2022
@remi-delmas-3000 remi-delmas-3000 added aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts labels Nov 11, 2022
@codecov
Copy link

codecov bot commented Nov 11, 2022

Codecov Report

Base: 78.28% // Head: 78.28% // Decreases project coverage by -0.00% ⚠️

Coverage data is based on head (9fd95ed) compared to base (a295651).
Patch coverage: 82.45% of modified lines in pull request are covered.

Additional details and impacted files
@@             Coverage Diff             @@
##           develop    #7328      +/-   ##
===========================================
- Coverage    78.28%   78.28%   -0.01%     
===========================================
  Files         1642     1642              
  Lines       190004   189992      -12     
===========================================
- Hits        148744   148734      -10     
+ Misses       41260    41258       -2     
Impacted Files Coverage Δ
src/goto-instrument/contracts/contracts.h 100.00% <ø> (ø)
src/goto-programs/graphml_witness.cpp 52.94% <0.00%> (-0.15%) ⬇️
src/goto-programs/interpreter.cpp 52.38% <0.00%> (+0.17%) ⬆️
src/util/expr_initializer.cpp 85.10% <80.00%> (+1.77%) ⬆️
jbmc/src/java_bytecode/expr2java.cpp 86.25% <93.75%> (ø)
src/ansi-c/c_typecheck_initializer.cpp 76.57% <100.00%> (+0.04%) ⬆️
src/ansi-c/expr2c.cpp 67.33% <100.00%> (-0.02%) ⬇️
src/goto-instrument/contracts/contracts.cpp 94.47% <100.00%> (-0.56%) ⬇️
src/goto-instrument/dump_c.cpp 79.97% <100.00%> (-0.03%) ⬇️
src/memory-analyzer/analyze_symbol.cpp 74.09% <100.00%> (+0.06%) ⬆️
... and 4 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

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

@feliperodri feliperodri changed the title CONTRACTS: drop function pointer contract support CONTRACTS: Drop function pointer contract support Nov 12, 2022
@tautschnig tautschnig merged commit 7498a43 into diffblue:develop Nov 13, 2022
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 Code Contracts Function and loop contracts
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants