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

SV-COMP 2024 development #1257

Merged
merged 87 commits into from
Nov 24, 2023
Merged

SV-COMP 2024 development #1257

merged 87 commits into from
Nov 24, 2023

Commits on Oct 4, 2023

  1. Add ldv_kzalloc to svcomp malloc wrappers

    @sim642
    sim642 committed Oct 4, 2023
    Configuration menu
    Copy the full SHA
    80b3b72 View commit details
    Browse the repository at this point in the history

  2. Disable free races in svcomp 

    They should be considered MemSafety issues instead.
    @sim642
    sim642 committed Oct 4, 2023
    Configuration menu
    Copy the full SHA
    35f6d00 View commit details
    Browse the repository at this point in the history

  3. Make threadid path sensitive in svcomp 

    This is required for some ldv-races/ no-data-race tasks.
    @sim642
    sim642 committed Oct 4, 2023
    Configuration menu
    Copy the full SHA
    b6dfb14 View commit details
    Browse the repository at this point in the history

  4. Use exp.architecture for SV-COMP preprocessing 

    Avoids a large number or CIL warnings about mismatching types.
    @sim642
    sim642 committed Oct 4, 2023
    Configuration menu
    Copy the full SHA
    11164fd View commit details
    Browse the repository at this point in the history

Commits on Oct 5, 2023

  1. Add option ana.race.call

    @sim642
    sim642 committed Oct 5, 2023
    Configuration menu
    Copy the full SHA
    94307d0 View commit details
    Browse the repository at this point in the history

Commits on Nov 1, 2023

  1. Use threadflag path-sensitivity instead of threadid in svcomp conf 

    This is enough for ldv-races/race-2_1-container_of, etc, but cheaper.
    @sim642
    sim642 committed Nov 1, 2023
    Configuration menu
    Copy the full SHA
    35f9323 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into svcomp24-conf

    @sim642
    sim642 committed Nov 1, 2023
    Configuration menu
    Copy the full SHA
    ebc8cf8 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'sv-comp-yaml' into svcomp24-dev

    @sim642
    sim642 committed Nov 1, 2023
    Configuration menu
    Copy the full SHA
    b80ba98 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'sv-comp-multiproperty' into svcomp24-dev

    @sim642
    sim642 committed Nov 1, 2023
    Configuration menu
    Copy the full SHA
    4910a51 View commit details
    Browse the repository at this point in the history

  5. Copy svcomp conf to svcomp24

    @sim642
    sim642 committed Nov 1, 2023
    Configuration menu
    Copy the full SHA
    f4b3710 View commit details
    Browse the repository at this point in the history

  6. Add YAML witness generation to svcomp confs

    @sim642
    sim642 committed Nov 1, 2023
    Configuration menu
    Copy the full SHA
    529a415 View commit details
    Browse the repository at this point in the history

  7. Copy svcomp24 conf to svcomp24-validate

    @sim642
    sim642 committed Nov 1, 2023
    Configuration menu
    Copy the full SHA
    ab9eacc View commit details
    Browse the repository at this point in the history

  8. Add YAML witness validation to svcomp24-validate conf

    @sim642
    sim642 committed Nov 1, 2023
    Configuration menu
    Copy the full SHA
    95ee32e View commit details
    Browse the repository at this point in the history

  9. Update sv-comp/archive.sh for 2024

    @sim642
    sim642 committed Nov 1, 2023
    Configuration menu
    Copy the full SHA
    ce917e6 View commit details
    Browse the repository at this point in the history

  10. Fix Apron license for unpinned package for SV-COMP

    @sim642
    sim642 committed Nov 1, 2023
    Configuration menu
    Copy the full SHA
    6bad00c View commit details
    Browse the repository at this point in the history

Commits on Nov 7, 2023

  1. Warn whenever there's allocated heap memory that's unreachable from g… 

    …lobals at program exit
    @mrstanb
    mrstanb committed Nov 7, 2023
    Configuration menu
    Copy the full SHA
    421abcd View commit details
    Browse the repository at this point in the history

  2. Add test cases for unreachable heap memory from globals

    @mrstanb
    mrstanb committed Nov 7, 2023
    Configuration menu
    Copy the full SHA
    9f7224e View commit details
    Browse the repository at this point in the history

Commits on Nov 8, 2023

  1. Remove //TODO comment from 76/09

    @mrstanb
    mrstanb committed Nov 8, 2023
    Configuration menu
    Copy the full SHA
    c056b32 View commit details
    Browse the repository at this point in the history

  2. Don't set InvalidMemTrack flag a second time 

    Co-authored-by: Michael Schwarz <[email protected]>
    @mrstanb @michael-schwarz
    mrstanb and michael-schwarz authored Nov 8, 2023
    Configuration menu
    Copy the full SHA
    175b003 View commit details
    Browse the repository at this point in the history

  3. Don't set InvalidMemTrack flag a second time 

    Co-authored-by: Michael Schwarz <[email protected]>
    @mrstanb @michael-schwarz
    mrstanb and michael-schwarz authored Nov 8, 2023
    Configuration menu
    Copy the full SHA
    05e4892 View commit details
    Browse the repository at this point in the history

  4. Add 3 regr. tests for trying out global struct variables

    @mrstanb
    mrstanb committed Nov 8, 2023
    Configuration menu
    Copy the full SHA
    f343d74 View commit details
    Browse the repository at this point in the history

Commits on Nov 9, 2023

  1. Merge branch 'master' into svcomp24-conf

    @sim642
    sim642 committed Nov 9, 2023
    Configuration menu
    Copy the full SHA
    afdf566 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into svcomp24-conf

    @sim642
    sim642 committed Nov 9, 2023
    Configuration menu
    Copy the full SHA
    6aed24f View commit details
    Browse the repository at this point in the history

  3. Merge branch 'svcomp24-conf' into svcomp24-dev

    @sim642
    sim642 committed Nov 9, 2023
    Configuration menu
    Copy the full SHA
    c88a1fa View commit details
    Browse the repository at this point in the history

  4. Merge branch 'yaml-witness-2.0' into svcomp24-dev

    @sim642
    sim642 committed Nov 9, 2023
    Configuration menu
    Copy the full SHA
    0698aad View commit details
    Browse the repository at this point in the history

  5. Fix relation read_globals_to_locals reading untracked variables

    @sim642
    sim642 committed Nov 9, 2023
    Configuration menu
    Copy the full SHA
    7fc8343 View commit details
    Browse the repository at this point in the history

  6. Remove default Apron polyhedra in svcomp24-validate conf

    @sim642
    sim642 committed Nov 9, 2023
    Configuration menu
    Copy the full SHA
    fbc66e3 View commit details
    Browse the repository at this point in the history

  7. Merge branch 'yaml-witness-2.0' into svcomp24-dev

    @sim642
    sim642 committed Nov 9, 2023
    Configuration menu
    Copy the full SHA
    39b9834 View commit details
    Browse the repository at this point in the history

Commits on Nov 15, 2023

  1. Merge branch 'master' into improve-valid-memtrack-for-single-threaded… 

    …-programs
    @michael-schwarz
    michael-schwarz authored Nov 15, 2023
    Configuration menu
    Copy the full SHA
    24fd4e8 View commit details
    Browse the repository at this point in the history

  2. Improve the detection of reachable memory through global struct vars

    @mrstanb
    mrstanb committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    6decbdd View commit details
    Browse the repository at this point in the history

  3. Add regr. tests for reachable memory through global struct vars

    @mrstanb
    mrstanb committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    c380426 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'improve-valid-memtrack-for-single-threaded-programs' of… 

    … github.com:mrstanb/analyzer into improve-valid-memtrack-for-single-threaded-programs
    @mrstanb
    mrstanb committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    0bec1ac View commit details
    Browse the repository at this point in the history

  5. Fix semgrep warning for using List.length for an emptiness check

    @mrstanb
    mrstanb committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    8459104 View commit details
    Browse the repository at this point in the history

Commits on Nov 16, 2023

  1. First attempt to improve precision for multi-threaded valid-memcleanup

    @mrstanb
    mrstanb committed Nov 16, 2023
    Configuration menu
    Copy the full SHA
    f209afd View commit details
    Browse the repository at this point in the history

  2. Add regr. test cases for multi-threaded valid-memcleanup

    @mrstanb
    mrstanb committed Nov 16, 2023
    Configuration menu
    Copy the full SHA
    c0fe89e View commit details
    Browse the repository at this point in the history

Commits on Nov 17, 2023

  1. Fix YAML witness invariants for unrolled loops (closes #1225)

    @sim642
    sim642 committed Nov 17, 2023
    Configuration menu
    Copy the full SHA
    6f54991 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'yaml-witness-2.0' into yaml-witness-location-hack

    @sim642
    sim642 committed Nov 17, 2023
    Configuration menu
    Copy the full SHA
    eabb461 View commit details
    Browse the repository at this point in the history

  3. Fix bisect_ppx build

    @sim642
    sim642 committed Nov 17, 2023
    Configuration menu
    Copy the full SHA
    952b90d View commit details
    Browse the repository at this point in the history

  4. Merge branch 'yaml-witness-location-hack' into svcomp24-dev

    @sim642
    sim642 committed Nov 17, 2023
    Configuration menu
    Copy the full SHA
    b699aa0 View commit details
    Browse the repository at this point in the history

  5. Fix missing unrolled iterations in YAML witness invariants 

    Unrolled loop heads are different nodes, which aren't actually loop heads.
For sound invariants, they must also be included if at a location if at least one is.
    @sim642
    sim642 committed Nov 17, 2023
    Configuration menu
    Copy the full SHA
    4ae3556 View commit details
    Browse the repository at this point in the history

  6. Refactor YAML witness fundec lookup

    @sim642
    sim642 committed Nov 17, 2023
    Configuration menu
    Copy the full SHA
    0fb479f View commit details
    Browse the repository at this point in the history

  7. Fix YamlWitness indentation

    @sim642
    sim642 committed Nov 17, 2023
    Configuration menu
    Copy the full SHA
    3c89ece View commit details
    Browse the repository at this point in the history

  8. Merge branch 'yaml-witness-location-hack' into svcomp24-dev

    @sim642
    sim642 committed Nov 17, 2023
    Configuration menu
    Copy the full SHA
    a69e5b6 View commit details
    Browse the repository at this point in the history

  9. Bump YAML entry size for large unrolled invariants

    @sim642
    sim642 committed Nov 17, 2023
    Configuration menu
    Copy the full SHA
    b57e80d View commit details
    Browse the repository at this point in the history

  10. Make YAML output buffer sizing exponential

    @sim642
    sim642 committed Nov 17, 2023
    Configuration menu
    Copy the full SHA
    f709482 View commit details
    Browse the repository at this point in the history

Commits on Nov 18, 2023

  1. Use solely local state for multi-threaded valid-memcleanup

    @mrstanb
    mrstanb committed Nov 18, 2023
    Configuration menu
    Copy the full SHA
    7289ec3 View commit details
    Browse the repository at this point in the history

  2. Use unrollType and GVarDecl for global vars 

    Also use `Queries.AD.fold` where applicable and prepend to accumulators
    @mrstanb
    mrstanb committed Nov 18, 2023
    Configuration menu
    Copy the full SHA
    6cc01b5 View commit details
    Browse the repository at this point in the history

  3. Check that addresses in struct fields are singletons and not top

    @mrstanb
    mrstanb committed Nov 18, 2023
    Configuration menu
    Copy the full SHA
    80492cc View commit details
    Browse the repository at this point in the history

Commits on Nov 19, 2023

  1. IsMallocCalled should be may

    @michael-schwarz
    michael-schwarz committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    720cfee View commit details
    Browse the repository at this point in the history

  2. Use unrollType for non-pointer global struct vars

    @mrstanb
    mrstanb committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    f2ca6d1 View commit details
    Browse the repository at this point in the history

  3. Don't forget to prepend to acc when collecting globally reachable mem

    @mrstanb
    mrstanb committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    0e09d09 View commit details
    Browse the repository at this point in the history

  4. Add unsound example

    @michael-schwarz
    michael-schwarz committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    af9ddc7 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'master' into improve-multi-threaded-valid-memcleanup

    @michael-schwarz
    michael-schwarz committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    0655fd6 View commit details
    Browse the repository at this point in the history

  6. Make sound by accounting for alloc in global invariant

    @michael-schwarz
    michael-schwarz committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    ada8491 View commit details
    Browse the repository at this point in the history

  7. Cleanup

    @michael-schwarz
    michael-schwarz committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    e7d6302 View commit details
    Browse the repository at this point in the history

  8. Fix memtrack for multi-threaded case

    @michael-schwarz
    michael-schwarz committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    e6cee27 View commit details
    Browse the repository at this point in the history

  9. Account for failing assertions in the multi-threaded case as well

    @mrstanb
    mrstanb committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    97eb715 View commit details
    Browse the repository at this point in the history

  10. Add a few more test cases

    @mrstanb
    mrstanb committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    987795e View commit details
    Browse the repository at this point in the history

  11. Add options to produce warnings only for memory leaks 

    due to `memcleanup` or `memtrack` violations
    @mrstanb
    mrstanb committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    8d55024 View commit details
    Browse the repository at this point in the history

Commits on Nov 20, 2023

  1. Make SV-COMP validation strict

    @sim642
    sim642 committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    ecd48aa View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into svcomp24-dev

    @sim642
    sim642 committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    71517e6 View commit details
    Browse the repository at this point in the history

  3. Add ana.autotune.activated schema

    @sim642
    sim642 committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    6797cbb View commit details
    Browse the repository at this point in the history

  4. Deactivate mhp and region for single-threaded programs

    @sim642
    sim642 committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    3af192d View commit details
    Browse the repository at this point in the history

  5. Update SV-COMP releasing guide for 2024

    @sim642
    sim642 committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    0ee71a0 View commit details
    Browse the repository at this point in the history

Commits on Nov 21, 2023

  1. Fix invariant_set elements schema in YAML witnesses

    @sim642
    sim642 committed Nov 21, 2023
    Configuration menu
    Copy the full SHA
    8b79948 View commit details
    Browse the repository at this point in the history

  2. Add example where better privatization helps

    @michael-schwarz
    michael-schwarz committed Nov 21, 2023
    Configuration menu
    Copy the full SHA
    ca61360 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into svcomp24-dev

    @sim642
    sim642 committed Nov 21, 2023
    Configuration menu
    Copy the full SHA
    f75a5ac View commit details
    Browse the repository at this point in the history

  4. Check at end of main thread that the program is certainly single-thre… 

    …aded.

If other threads are not joined, they may be killed by the main thread returning.
This will possibly leak memory.
    @jerhard
    jerhard committed Nov 21, 2023
    Configuration menu
    Copy the full SHA
    2cc915f View commit details
    Browse the repository at this point in the history

  5. Add test case for memory leaking from a thead that is not joined, add… 

    … thread_joins to other test cases.
    @jerhard
    jerhard committed Nov 21, 2023
    Configuration menu
    Copy the full SHA
    45ec8a6 View commit details
    Browse the repository at this point in the history

  6. Add test case with pthread_exit called in main, remove threadid analy… 

    …sis from params as it is not needed.
    @jerhard
    jerhard committed Nov 21, 2023
    Configuration menu
    Copy the full SHA
    56c4d62 View commit details
    Browse the repository at this point in the history

  7. Add testcases for thread return and pthread_exit in thread different … 

    …from main.
    @jerhard
    jerhard committed Nov 21, 2023
    Configuration menu
    Copy the full SHA
    2fef812 View commit details
    Browse the repository at this point in the history

  8. ThreadAnalysis: Handle pthread_exit like return from thread.

    @jerhard
    jerhard committed Nov 21, 2023
    Configuration menu
    Copy the full SHA
    645b03c View commit details
    Browse the repository at this point in the history

  9. Use AD.fold instead of List.fold_left

    @mrstanb
    mrstanb committed Nov 21, 2023
    Configuration menu
    Copy the full SHA
    9153eb3 View commit details
    Browse the repository at this point in the history

Commits on Nov 22, 2023

  1. Update tests/regression/76-memleak/16-no-mem-leak-thread-exit-main.c 

    Co-authored-by: Simmo Saan <[email protected]>
    @jerhard @sim642
    jerhard and sim642 authored Nov 22, 2023
    Configuration menu
    Copy the full SHA
    c6cb63e View commit details
    Browse the repository at this point in the history

  2. Remove call to free.

    @jerhard
    jerhard committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    f12a392 View commit details
    Browse the repository at this point in the history

  3. Add annotation of nowarn next to pthread_exit.

    @jerhard
    jerhard committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    be9171b View commit details
    Browse the repository at this point in the history

  4. Check in TheadAnalysis.return whether the return is actually a thread… 

    …return before side-effecting.
    @jerhard
    jerhard committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    585a65d View commit details
    Browse the repository at this point in the history

  5. Add test case that checking that analysis distinguishes between threa… 

    …d returns and normal returns of a thread.
    @jerhard
    jerhard committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    bc7694b View commit details
    Browse the repository at this point in the history

  6. MemLeak: Do not consider unions

    @michael-schwarz
    michael-schwarz committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    666795f View commit details
    Browse the repository at this point in the history

  7. Add initial CHANGELOG for SV-COMP 2024

    @sim642
    sim642 committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    dd45d19 View commit details
    Browse the repository at this point in the history

  8. Add initial CHANGELOG for v2.3.0

    @sim642
    sim642 committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    bf754c0 View commit details
    Browse the repository at this point in the history

  9. Add CHANGELOG for v2.3.0

    @sim642
    sim642 committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    9c65057 View commit details
    Browse the repository at this point in the history

  10. Merge branch 'master' into svcomp24-dev

    @sim642
    sim642 committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    af1ddef View commit details
    Browse the repository at this point in the history

  11. Merge remote-tracking branch 'mrstanb/improve-valid-memtrack-for-sing… 

    …le-threaded-programs' into svcomp24-dev
    @sim642
    sim642 committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    765a64e View commit details
    Browse the repository at this point in the history

  12. Merge remote-tracking branch 'mrstanb/improve-multi-threaded-valid-me… 

    …mcleanup' into svcomp24-dev
    @sim642
    sim642 committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    d629d14 View commit details
    Browse the repository at this point in the history

Commits on Nov 23, 2023

  1. Merge branch 'master' into svcomp24-dev

    @sim642
    sim642 committed Nov 23, 2023
    Configuration menu
    Copy the full SHA
    e0a0692 View commit details
    Browse the repository at this point in the history

Commits on Nov 24, 2023

  1. Merge branch 'master' into svcomp24-dev

    @sim642
    sim642 committed Nov 24, 2023
    Configuration menu
    Copy the full SHA
    c2e9465 View commit details
    Browse the repository at this point in the history