Skip to content

allow multiple assigns clauses #6226

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
Jul 14, 2021
Merged

Conversation

kroening
Copy link
Member

This changes the parser to allow multiple assigns clauses in a contract.
The meaning of multiple clauses is the same as the meaning of one clause
that contains the concatenation of the target lists of the given clauses.

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

@kroening kroening added C Front End aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts labels Jul 14, 2021
@kroening kroening force-pushed the multiple_assigns_clauses branch from 90ef605 to 716eef1 Compare July 14, 2021 17:55
@feliperodri feliperodri force-pushed the multiple_assigns_clauses branch from 716eef1 to af22e6c Compare July 14, 2021 18:34
@feliperodri feliperodri marked this pull request as ready for review July 14, 2021 18:34
Copy link
Contributor

@SaswatPadhi SaswatPadhi left a comment

Choose a reason for hiding this comment

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

Thanks! LGTM

This changes the parser to allow multiple assigns clauses in a contract.
The meaning of multiple clauses is the same as the meaning of one clause
that contains the concatenation of the target lists of the given clauses.
@feliperodri feliperodri force-pushed the multiple_assigns_clauses branch from af22e6c to ef74099 Compare July 14, 2021 18:36
@codecov
Copy link

codecov bot commented Jul 14, 2021

Codecov Report

Merging #6226 (af22e6c) into develop (0002950) will increase coverage by 8.05%.
The diff coverage is n/a.

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

@@             Coverage Diff             @@
##           develop    #6226      +/-   ##
===========================================
+ Coverage    67.40%   75.46%   +8.05%     
===========================================
  Files         1157     1459     +302     
  Lines        95236   161447   +66211     
===========================================
+ Hits         64197   121841   +57644     
- Misses       31039    39606    +8567     
Flag Coverage Δ
cproversmt2 ?
regression ?
unit ?

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files Coverage Δ
src/util/string_container.cpp 52.94% <0.00%> (-47.06%) ⬇️
src/solvers/prop/prop.cpp 42.85% <0.00%> (-41.76%) ⬇️
src/solvers/flattening/boolbv_member.cpp 53.65% <0.00%> (-38.65%) ⬇️
src/cpp/cpp_storage_spec.cpp 65.00% <0.00%> (-35.00%) ⬇️
src/util/cmdline.h 66.66% <0.00%> (-33.34%) ⬇️
src/solvers/strings/array_pool.h 66.66% <0.00%> (-33.34%) ⬇️
src/solvers/strings/string_refinement.h 66.66% <0.00%> (-33.34%) ⬇️
...rs/strings/string_concatenation_builtin_function.h 0.00% <0.00%> (-33.34%) ⬇️
src/cbmc/c_test_input_generator.cpp 60.00% <0.00%> (-30.33%) ⬇️
src/analyses/local_cfg.h 75.00% <0.00%> (-25.00%) ⬇️
... and 1438 more

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 10ddca0...ef74099. Read the comment docs.

@feliperodri feliperodri merged commit c509854 into develop Jul 14, 2021
@feliperodri feliperodri deleted the multiple_assigns_clauses branch July 14, 2021 22:15
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 C Front End Code Contracts Function and loop contracts
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants