search

aws / aws-cryptographic-material-providers-library-java

AWS Cryptographic Material Providers Library for Java
Apache License 2.0
4 stars 6 forks source link

chore(deps): bump org.dafny:DafnyRuntime from 4.2.0 to 4.4.0 in /AwsCryptographicMaterialProviders/runtimes/java #211

Open dependabot[bot] opened 10 months ago

dependabot[bot] commented 10 months ago

Bumps org.dafny:DafnyRuntime from 4.2.0 to 4.4.0.

Release notes

Sourced from org.dafny:DafnyRuntime's releases.

Dafny 4.4.0

New features

  • Reads clauses on method declarations are now supported when the --reads-clauses-on-methods option is provided. The {:concurrent} attribute now verifies that the reads and modifies clauses are empty instead of generating an auditor warning. (dafny-lang/dafny#4440)

  • Added two new options, --warn-contradictory-assumptions and --warn-redundant-assumptions, to detect potential problems with specifications that indicate that successful verification may be misleading. These options are currently hidden because they may occasionally produce false positives in cases where proofs are so trivial that the solver never does work on them. (dafny-lang/dafny#4542)

  • Verification of the {:concurrent} attribute on methods now allows non-empty reads and modifies clauses with the {:assume_concurrent} attribute. (dafny-lang/dafny#4563)

  • Implemented support for workspace/symbol request to allow IDE navigation by symbol. (dafny-lang/dafny#4619)

  • The new --verification-coverage-report flag to dafny verify creates an HTML report highlighting which portions of the program were and were not necessary for verification. The format is the same as for dafny generate-tests --coverage-report and files from the two commands can be merged. (dafny-lang/dafny#4625)

  • Built-in types such as the nat subset type, tuples, arrows, and arrays are now pre-compiled into each backend's runtime library, instead of emitted on every call to dafny translate, to avoid potential duplicate definitions when translating components separately. (dafny-lang/dafny#4658)

  • The new --only-label option to merge-coverage-reports includes only one category of highlighting in the output. For example, merging coverage reports from test generation and verification using the option --only-label NotCovered will highlight only the regions not covered by either testing or verification. (dafny-lang/dafny#4673)

  • The Dafny distribution now includes standard libraries, available with the --standard-libraries option. See https://github.com/dafny-lang/dafny/blob/master/Source/DafnyStandardLibraries/README.md for details. (dafny-lang/dafny#4678)

  • Introduce replaceable modules, which can be used to help define Dafny applications that translate to multiple target languages. (dafny-lang/dafny#4681)

  • The new --coverage-report flag to dafny run and dafny test creates an HTML report highlighting which portions of the program were executed at runtime. (dafny-lang/dafny#4755)

  • Enable turning nonlinear arithmetic on or off on a per-module basis, using the attribute {:disable-nonlinear-arithmetic}, which optionally takes the value false to enable nonlinear arithmetic. (dafny-lang/dafny#4773)

  • Let the IDE provide code navigation in situations where the program parses but has resolution errors. Note that this only works for modules whose dependency tree does not have errors, or modules who contain errors themselves, but not for modules whose dependencies contain errors. (dafny-lang/dafny#4855)

Bug fixes

  • Ensures that computing the set of values or items of map can only be done if the type of the range supports equality. (dafny-lang/dafny#1373)

  • Subset type decl's witness correctly taken into account (dafny-lang/dafny#3792)

  • Added a comprehensive test for test generation and fixed a bug that prevented test generation to process function-by-method declarations (dafny-lang/dafny#4406)

  • Optimized memory consumption of test generation by reusing the Boogie AST of the target Dafny program. (dafny-lang/dafny#4530)

  • Fix a bug that prevented certain types of lemma to be verified in the IDE (dafny-lang/dafny#4607)

  • Dot completion now works on values the type of which is a type synonym. (dafny-lang/dafny#4635)

  • Fix a case where the document symbol API would return incorrect data when working on a file with parse errors (dafny-lang/dafny#4675)

... (truncated)

Changelog

Sourced from org.dafny:DafnyRuntime's changelog.

4.4.0

New features

  • Reads clauses on method declarations are now supported when the --reads-clauses-on-methods option is provided. The {:concurrent} attribute now verifies that the reads and modifies clauses are empty instead of generating an auditor warning. (dafny-lang/dafny#4440)

  • Added two new options, --warn-contradictory-assumptions and --warn-redundant-assumptions, to detect potential problems with specifications that indicate that successful verification may be misleading. These options are currently hidden because they may occasionally produce false positives in cases where proofs are so trivial that the solver never does work on them. (dafny-lang/dafny#4542)

  • Verification of the {:concurrent} attribute on methods now allows non-empty reads and modifies clauses with the {:assume_concurrent} attribute. (dafny-lang/dafny#4563)

  • Implemented support for workspace/symbol request to allow IDE navigation by symbol. (dafny-lang/dafny#4619)

  • The new --verification-coverage-report flag to dafny verify creates an HTML report highlighting which portions of the program were and were not necessary for verification. The format is the same as for dafny generate-tests --coverage-report and files from the two commands can be merged. (dafny-lang/dafny#4625)

  • Built-in types such as the nat subset type, tuples, arrows, and arrays are now pre-compiled into each backend's runtime library, instead of emitted on every call to dafny translate, to avoid potential duplicate definitions when translating components separately. (dafny-lang/dafny#4658)

  • The new --only-label option to merge-coverage-reports includes only one category of highlighting in the output. For example, merging coverage reports from test generation and verification using the option --only-label NotCovered will highlight only the regions not covered by either testing or verification. (dafny-lang/dafny#4673)

  • The Dafny distribution now includes standard libraries, available with the --standard-libraries option. See https://github.com/dafny-lang/dafny/blob/master/Source/DafnyStandardLibraries/README.md for details. (dafny-lang/dafny#4678)

  • Introduce replaceable modules, which can be used to help define Dafny applications that translate to multiple target languages. (dafny-lang/dafny#4681)

  • The new --coverage-report flag to dafny run and dafny test creates an HTML report highlighting which portions of the program were executed at runtime. (dafny-lang/dafny#4755)

  • Enable turning nonlinear arithmetic on or off on a per-module basis, using the attribute {:disable-nonlinear-arithmetic}, which optionally takes the value false to enable nonlinear arithmetic. (dafny-lang/dafny#4773)

  • Let the IDE provide code navigation in situations where the program parses but has resolution errors. Note that this only works for modules whose dependency tree does not have errors, or modules who contain errors themselves, but not for modules whose dependencies contain errors. (dafny-lang/dafny#4855)

Bug fixes

  • Ensures that computing the set of values or items of map can only be done if the type of the range supports equality. (dafny-lang/dafny#1373)

  • Subset type decl's witness correctly taken into account (dafny-lang/dafny#3792)

  • Added a comprehensive test for test generation and fixed a bug that prevented test generation to process function-by-method declarations (dafny-lang/dafny#4406)

  • Optimized memory consumption of test generation by reusing the Boogie AST of the target Dafny program. (dafny-lang/dafny#4530)

  • Fix a bug that prevented certain types of lemma to be verified in the IDE (dafny-lang/dafny#4607)

  • Dot completion now works on values the type of which is a type synonym. (dafny-lang/dafny#4635)

... (truncated)

Commits
  • 707b18a Release Dafny 4.4.0
  • 2cadde8 feat: Tighten specifications on Strings standard library (#4868)
  • f735fd9 feat: Add a few more Std.Collections.Seq functions (#4867)
  • 306f0c7 fix: Don’t add target-specific standard library doo files to root source URIs...
  • 5f30d1b fix: The Python compiler emits reserved names for datatypes (#4843)
  • 4faa561 chore: Prep for 4.4 release (#4859)
  • e6c8483 Use {:disable_nonlinear_arithmetic} to simplify standard library (#4841)
  • c7b2897 Bump Boogie to v3.0.9 (#4857)
  • 7e57091 Code navigation when resolution errors (#4855)
  • 97fc3a6 feat: Concurrent collections (#4815)
  • Additional commits viewable in compare view


Dependabot compatibility score

Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting @dependabot rebase.

Dependabot commands and options
You can trigger Dependabot actions by commenting on this PR: - `@dependabot rebase` will rebase this PR - `@dependabot recreate` will recreate this PR, overwriting any edits that have been made to it - `@dependabot merge` will merge this PR after your CI passes on it - `@dependabot squash and merge` will squash and merge this PR after your CI passes on it - `@dependabot cancel merge` will cancel a previously requested merge and block automerging - `@dependabot reopen` will reopen this PR if it is closed - `@dependabot close` will close this PR and stop Dependabot recreating it. You can achieve the same result by closing it manually - `@dependabot show ignore conditions` will show all of the ignore conditions of the specified dependency - `@dependabot ignore this major version` will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself) - `@dependabot ignore this minor version` will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself) - `@dependabot ignore this dependency` will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself)