Skip to content
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

Update to CBMC version 6.1.1 #2995

Merged
merged 62 commits into from
Jul 31, 2024
Merged

Update to CBMC version 6.1.1 #2995

merged 62 commits into from
Jul 31, 2024

Commits on Feb 6, 2024

  1. Update to CBMC version 6.0.0 

    Updates to match changes to the GOTO binary format.

Resolves: model-checking#2972
    @tautschnig
    tautschnig committed Feb 6, 2024
    Configuration menu
    Copy the full SHA
    da76cb3 View commit details
    Browse the repository at this point in the history

Commits on Jun 18, 2024

  1. Merge remote-tracking branch 'origin/main' into cbmc-6

    @tautschnig
    tautschnig committed Jun 18, 2024
    Configuration menu
    Copy the full SHA
    2f37c6f View commit details
    Browse the repository at this point in the history

Commits on Jun 19, 2024

  1. Force tests to pass

    @tautschnig
    tautschnig committed Jun 19, 2024
    Configuration menu
    Copy the full SHA
    d6e78a8 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/main' into cbmc-6

    @tautschnig
    tautschnig committed Jun 19, 2024
    Configuration menu
    Copy the full SHA
    1bc0129 View commit details
    Browse the repository at this point in the history

  3. Add overlay files to enable performance data output

    @tautschnig
    tautschnig committed Jun 19, 2024
    Configuration menu
    Copy the full SHA
    5d73a67 View commit details
    Browse the repository at this point in the history

  4. Enable verbosity 9 for performance numbers

    @tautschnig
    tautschnig committed Jun 19, 2024
    Configuration menu
    Copy the full SHA
    e95e689 View commit details
    Browse the repository at this point in the history

  5. Revert "Enable verbosity 9 for performance numbers" 

    This reverts commit e95e689.
    @tautschnig
    tautschnig committed Jun 19, 2024
    Configuration menu
    Copy the full SHA
    7feccd5 View commit details
    Browse the repository at this point in the history

  6. Revert "Add overlay files to enable performance data output" 

    This reverts commit 5d73a67.
    @tautschnig
    tautschnig committed Jun 19, 2024
    Configuration menu
    Copy the full SHA
    0125a23 View commit details
    Browse the repository at this point in the history

  7. Verbosity 9 for perf tests

    @tautschnig
    tautschnig committed Jun 19, 2024
    Configuration menu
    Copy the full SHA
    9a68859 View commit details
    Browse the repository at this point in the history

  8. Separate flags

    @tautschnig
    tautschnig committed Jun 19, 2024
    Configuration menu
    Copy the full SHA
    7dd43d8 View commit details
    Browse the repository at this point in the history

  9. benchcomp test with verbosity

    @tautschnig
    tautschnig committed Jun 19, 2024
    Configuration menu
    Copy the full SHA
    a55167a View commit details
    Browse the repository at this point in the history

Commits on Jun 20, 2024

  1. Merge remote-tracking branch 'origin/main' into cbmc-6

    @tautschnig
    tautschnig committed Jun 20, 2024
    Configuration menu
    Copy the full SHA
    952841d View commit details
    Browse the repository at this point in the history

  2. Revert "Force tests to pass" 

    This reverts commit d6e78a8.
    @tautschnig
    tautschnig committed Jun 20, 2024
    Configuration menu
    Copy the full SHA
    e32e3c6 View commit details
    Browse the repository at this point in the history

  3. Set higher verbosity for tests as needed

    @tautschnig
    tautschnig committed Jun 20, 2024
    Configuration menu
    Copy the full SHA
    383a6f4 View commit details
    Browse the repository at this point in the history

  4. Update interface to CBMC v6

    @tautschnig
    tautschnig committed Jun 20, 2024
    Configuration menu
    Copy the full SHA
    11b1dd1 View commit details
    Browse the repository at this point in the history

  5. Regression test workarounds

    @tautschnig
    tautschnig committed Jun 20, 2024
    Configuration menu
    Copy the full SHA
    d591c4d View commit details
    Browse the repository at this point in the history

  6. Revert "Regression test workarounds" 

    This reverts commit d591c4d.
    @tautschnig
    tautschnig committed Jun 20, 2024
    Configuration menu
    Copy the full SHA
    3abf589 View commit details
    Browse the repository at this point in the history

  7. Debugging storage markers

    @tautschnig
    tautschnig committed Jun 20, 2024
    Configuration menu
    Copy the full SHA
    d07841b View commit details
    Browse the repository at this point in the history

  8. WIP

    @tautschnig
    tautschnig committed Jun 20, 2024
    Configuration menu
    Copy the full SHA
    c179663 View commit details
    Browse the repository at this point in the history

  9. Codegen storage markers as assignments to __CPROVER_dead_object 

    This changes our handling of storage markers to be marking is-alive
only rather than treating StorageLive as creating a new object. That is,
object instances are now tied to their Mir-provided declarations (which,
at present, only appear once per function). To still account for when
Rust scopes deem an object to be alive, we use StorageLive and
StorageDead to update `__CPROVER_dead_object`. This (global) variable is
used by CBMC's pointer checks to track when a pointer may not be safe to
dereference for it could be pointing to an object that no longer is in
scope.

Resolves: model-checking#3099
    @tautschnig
    tautschnig committed Jun 20, 2024
    Configuration menu
    Copy the full SHA
    2db2a0d View commit details
    Browse the repository at this point in the history

  10. Revert model-checking#3080 except for std enablement

    @tautschnig
    tautschnig committed Jun 20, 2024
    Configuration menu
    Copy the full SHA
    bb5dc8f View commit details
    Browse the repository at this point in the history

  11. Mark failure that is not yet understood as FIXME

    @tautschnig
    tautschnig committed Jun 20, 2024
    Configuration menu
    Copy the full SHA
    e29d024 View commit details
    Browse the repository at this point in the history

  12. Mark newly slow tests as such

    @tautschnig
    tautschnig committed Jun 20, 2024
    Configuration menu
    Copy the full SHA
    6480755 View commit details
    Browse the repository at this point in the history

  13. Update property configuration for CBMC v6

    @tautschnig
    tautschnig committed Jun 20, 2024
    Configuration menu
    Copy the full SHA
    445f363 View commit details
    Browse the repository at this point in the history

  14. fixup! Set higher verbosity for tests as needed

    @tautschnig
    tautschnig committed Jun 20, 2024
    Configuration menu
    Copy the full SHA
    bb373f2 View commit details
    Browse the repository at this point in the history

Commits on Jun 21, 2024

  1. Use CBMC version 6.0.1

    @tautschnig
    tautschnig committed Jun 21, 2024
    Configuration menu
    Copy the full SHA
    fda6424 View commit details
    Browse the repository at this point in the history

  2. Use PPA with GCC-9 to build CBMC v6+ on Ubuntu 18.04

    @tautschnig
    tautschnig committed Jun 21, 2024
    Configuration menu
    Copy the full SHA
    125473d View commit details
    Browse the repository at this point in the history

  3. Use older pip version to remain compatible with Python 3.7

    @tautschnig
    tautschnig committed Jun 21, 2024
    Configuration menu
    Copy the full SHA
    e7242f2 View commit details
    Browse the repository at this point in the history

  4. Factor out access to __CPROVER_dead_object

    @tautschnig
    tautschnig committed Jun 21, 2024
    Configuration menu
    Copy the full SHA
    7f996e7 View commit details
    Browse the repository at this point in the history

  5. Revert "Mark failure that is not yet understood as FIXME" 

    This reverts commit e29d024.
    @tautschnig
    tautschnig committed Jun 21, 2024
    Configuration menu
    Copy the full SHA
    93398cb View commit details
    Browse the repository at this point in the history

  6. fixup! Codegen storage markers as assignments to __CPROVER_dead_object

    @tautschnig
    tautschnig committed Jun 21, 2024
    Configuration menu
    Copy the full SHA
    dcc9d61 View commit details
    Browse the repository at this point in the history

  7. Remove TODO as CBMC will not necessarily pick this up

    @tautschnig
    tautschnig committed Jun 21, 2024
    Configuration menu
    Copy the full SHA
    2001ae8 View commit details
    Browse the repository at this point in the history

  8. Fix Docker as well

    @tautschnig
    tautschnig committed Jun 21, 2024
    Configuration menu
    Copy the full SHA
    59d2fba View commit details
    Browse the repository at this point in the history

  9. fixup! fixup! Codegen storage markers as assignments to __CPROVER_dea… 

    …d_object
    @tautschnig
    tautschnig committed Jun 21, 2024
    Configuration menu
    Copy the full SHA
    42ed007 View commit details
    Browse the repository at this point in the history

Commits on Jun 24, 2024

  1. Add comment

    @tautschnig
    tautschnig committed Jun 24, 2024
    Configuration menu
    Copy the full SHA
    268a0c0 View commit details
    Browse the repository at this point in the history

  2. Build static binaries on Linux 18.04

    @tautschnig
    tautschnig committed Jun 24, 2024
    Configuration menu
    Copy the full SHA
    ebe6cdb View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/main' into cbmc-6

    @tautschnig
    tautschnig committed Jun 24, 2024
    Configuration menu
    Copy the full SHA
    2545e0c View commit details
    Browse the repository at this point in the history

  4. Comment explaining StorageLive/StorageDead modelling

    @tautschnig
    tautschnig committed Jun 24, 2024
    Configuration menu
    Copy the full SHA
    62d9f85 View commit details
    Browse the repository at this point in the history

  5. Extend comment

    @tautschnig
    tautschnig committed Jun 24, 2024
    Configuration menu
    Copy the full SHA
    d273960 View commit details
    Browse the repository at this point in the history

Commits on Jun 25, 2024

  1. Merge branch 'main' into cbmc-6

    @tautschnig
    tautschnig committed Jun 25, 2024
    Configuration menu
    Copy the full SHA
    728c1f7 View commit details
    Browse the repository at this point in the history

Commits on Jul 23, 2024

  1. Merge remote-tracking branch 'origin/main' into cbmc-6

    @tautschnig
    tautschnig committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    df95895 View commit details
    Browse the repository at this point in the history

  2. Use CBMC 6.1.0

    @tautschnig
    tautschnig committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    9d2e3e5 View commit details
    Browse the repository at this point in the history

  3. Test performance with CBMC using CaDiCaL 2.0.0

    @tautschnig
    tautschnig committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    b7b3b15 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'main' into cbmc-6

    @tautschnig
    tautschnig committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    fd78563 View commit details
    Browse the repository at this point in the history

Commits on Jul 24, 2024

  1. Merge branch 'main' into cbmc-6

    @tautschnig
    tautschnig committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    bdb80ea View commit details
    Browse the repository at this point in the history

  2. Work around CaDiCaL performance regression

    @tautschnig
    tautschnig committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    033b27d View commit details
    Browse the repository at this point in the history

  3. Revert "Work around CaDiCaL performance regression" 

    This reverts commit 033b27d.
    @tautschnig
    tautschnig committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    8cd357a View commit details
    Browse the repository at this point in the history

  4. Bump s2n-quic submodule

    @tautschnig
    tautschnig committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    277bdad View commit details
    Browse the repository at this point in the history

  5. Merge remote-tracking branch 'origin/main' into cbmc-6

    @tautschnig
    tautschnig committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    f938676 View commit details
    Browse the repository at this point in the history

  6. Benchcomp perf regression: move setup into run

    @tautschnig
    tautschnig committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    c1bc1ee View commit details
    Browse the repository at this point in the history

  7. Revert "Benchcomp perf regression: move setup into run" 

    This reverts commit c1bc1ee.
    @tautschnig
    tautschnig committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    f60db0e View commit details
    Browse the repository at this point in the history

  8. Install variant-specific dependencies

    @tautschnig
    tautschnig committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    85092ed View commit details
    Browse the repository at this point in the history

Commits on Jul 25, 2024

  1. Merge remote-tracking branch 'origin/main' into cbmc-6

    @tautschnig
    tautschnig committed Jul 25, 2024
    Configuration menu
    Copy the full SHA
    d94175c View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/main' into cbmc-6

    @tautschnig
    tautschnig committed Jul 25, 2024
    Configuration menu
    Copy the full SHA
    8127e5c View commit details
    Browse the repository at this point in the history

Commits on Jul 26, 2024

  1. Merge remote-tracking branch 'origin/main' into cbmc-6

    @tautschnig
    tautschnig committed Jul 26, 2024
    Configuration menu
    Copy the full SHA
    8bb15ce View commit details
    Browse the repository at this point in the history

  2. Use Local

    @tautschnig
    tautschnig committed Jul 26, 2024
    Configuration menu
    Copy the full SHA
    7ab6f60 View commit details
    Browse the repository at this point in the history

  3. Use constant

    @tautschnig
    tautschnig committed Jul 26, 2024
    Configuration menu
    Copy the full SHA
    e902354 View commit details
    Browse the repository at this point in the history

Commits on Jul 30, 2024

  1. Merge branch 'main' into cbmc-6

    @tautschnig
    tautschnig committed Jul 30, 2024
    Configuration menu
    Copy the full SHA
    007b1e9 View commit details
    Browse the repository at this point in the history

Commits on Jul 31, 2024

  1. Merge remote-tracking branch 'origin/main' into cbmc-6

    @tautschnig
    tautschnig committed Jul 31, 2024
    Configuration menu
    Copy the full SHA
    2a3fd06 View commit details
    Browse the repository at this point in the history

  2. Use CBMC 6.1.1

    @tautschnig
    tautschnig committed Jul 31, 2024
    Configuration menu
    Copy the full SHA
    c968d65 View commit details
    Browse the repository at this point in the history

  3. Revert "Test performance with CBMC using CaDiCaL 2.0.0" 

    This reverts commit b7b3b15.
    @tautschnig
    tautschnig committed Jul 31, 2024
    Configuration menu
    Copy the full SHA
    2de6464 View commit details
    Browse the repository at this point in the history

  4. Use verbosity 9 by default

    @tautschnig
    tautschnig committed Jul 31, 2024
    Configuration menu
    Copy the full SHA
    f878fd9 View commit details
    Browse the repository at this point in the history