Code

SV-COMP 2024 development#1257

Code

Merged

sim642 merged 87 commits intomastergoblint/analyzer:masterfrom svcomp24-devgoblint/analyzer:svcomp24-devCopy head branch name to clipboardNov 24, 2023

+1,212-89

Commits

Commits on Oct 4, 2023

• Add ldv_kzalloc to svcomp malloc wrappers

  sim642

  committed
  80b3b72

• Disable free races in svcomp

  Show description for 35f6d00
  sim642

  committed
  35f6d00

• Make threadid path sensitive in svcomp

  Show description for b6dfb14
  sim642

  committed
  b6dfb14

• Use exp.architecture for SV-COMP preprocessing

  Show description for 11164fd
  sim642

  committed
  11164fd

Commits on Oct 5, 2023

• Add option ana.race.call

  sim642

  committed
  94307d0

Commits on Nov 1, 2023

• Use threadflag path-sensitivity instead of threadid in svcomp conf

  Show description for 35f9323
  sim642

  committed
  35f9323

• Merge branch 'master' into svcomp24-conf

  sim642

  committed
  ebc8cf8

• Merge branch 'sv-comp-yaml' into svcomp24-dev

  sim642

  committed
  b80ba98

• Merge branch 'sv-comp-multiproperty' into svcomp24-dev

  sim642

  committed
  4910a51

• Copy svcomp conf to svcomp24

  sim642

  committed
  f4b3710

• Add YAML witness generation to svcomp confs

  sim642

  committed
  529a415

• Copy svcomp24 conf to svcomp24-validate

  sim642

  committed
  ab9eacc

• Add YAML witness validation to svcomp24-validate conf

  sim642

  committed
  95ee32e

• Update sv-comp/archive.sh for 2024

  sim642

  committed
  ce917e6

• Fix Apron license for unpinned package for SV-COMP

  sim642

  committed
  6bad00c

Commits on Nov 7, 2023

• Warn whenever there's allocated heap memory that's unreachable from globals at program exit

  mrstanb

  committed
  421abcd

• Add test cases for unreachable heap memory from globals

  mrstanb

  committed
  9f7224e

Commits on Nov 8, 2023

• Remove //TODO comment from 76/09

  mrstanb

  committed
  c056b32

• Don't set InvalidMemTrack flag a second time

  Show description for 175b003
  

  mrstanb

  and

  michael-schwarz

  authored
  175b003

• Don't set InvalidMemTrack flag a second time

  Show description for 05e4892
  

  mrstanb

  and

  michael-schwarz

  authored
  05e4892

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

  mrstanb

  committed
  f343d74

Commits on Nov 9, 2023

• Merge branch 'master' into svcomp24-conf

  sim642

  committed
  afdf566

• Merge branch 'master' into svcomp24-conf

  sim642

  committed
  6aed24f

• Merge branch 'svcomp24-conf' into svcomp24-dev

  sim642

  committed
  c88a1fa

• Merge branch 'yaml-witness-2.0' into svcomp24-dev

  sim642

  committed
  0698aad

• Fix relation read_globals_to_locals reading untracked variables

  sim642

  committed
  7fc8343

• Remove default Apron polyhedra in svcomp24-validate conf

  sim642

  committed
  fbc66e3

• Merge branch 'yaml-witness-2.0' into svcomp24-dev

  sim642

  committed
  39b9834

Commits on Nov 15, 2023

• Merge branch 'master' into improve-valid-memtrack-for-single-threaded-programs

  michael-schwarz

  authored
  24fd4e8

• Improve the detection of reachable memory through global struct vars

  mrstanb

  committed
  6decbdd

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

  mrstanb

  committed
  c380426

• Merge branch 'improve-valid-memtrack-for-single-threaded-programs' of github.com:mrstanb/analyzer into improve-valid-memtrack-for-single-threaded-programs

  mrstanb

  committed
  0bec1ac

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

  mrstanb

  committed
  8459104

Commits on Nov 16, 2023

• First attempt to improve precision for multi-threaded valid-memcleanup

  mrstanb

  committed
  f209afd

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

  mrstanb

  committed
  c0fe89e

Commits on Nov 17, 2023

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

  sim642

  committed
  6f54991

• Merge branch 'yaml-witness-2.0' into yaml-witness-location-hack

  sim642

  committed
  eabb461

• Fix bisect_ppx build

  sim642

  committed
  952b90d

• Merge branch 'yaml-witness-location-hack' into svcomp24-dev

  sim642

  committed
  b699aa0

• Fix missing unrolled iterations in YAML witness invariants

  Show description for 4ae3556
  sim642

  committed
  4ae3556

• Refactor YAML witness fundec lookup

  sim642

  committed
  0fb479f

• Fix YamlWitness indentation

  sim642

  committed
  3c89ece

• Merge branch 'yaml-witness-location-hack' into svcomp24-dev

  sim642

  committed
  a69e5b6

• Bump YAML entry size for large unrolled invariants

  sim642

  committed
  b57e80d

• Make YAML output buffer sizing exponential

  sim642

  committed
  f709482

Commits on Nov 18, 2023

• Use solely local state for multi-threaded valid-memcleanup

  mrstanb

  committed
  7289ec3

• Use unrollType and GVarDecl for global vars

  Show description for 6cc01b5
  mrstanb

  committed
  6cc01b5

• Check that addresses in struct fields are singletons and not top

  mrstanb

  committed
  80492cc

Commits on Nov 19, 2023

• IsMallocCalled should be may

  michael-schwarz

  committed
  720cfee

• Use unrollType for non-pointer global struct vars

  mrstanb

  committed
  f2ca6d1

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

  mrstanb

  committed
  0e09d09

• Add unsound example

  michael-schwarz

  committed
  af9ddc7

• Merge branch 'master' into improve-multi-threaded-valid-memcleanup

  michael-schwarz

  committed
  0655fd6

• Make sound by accounting for alloc in global invariant

  michael-schwarz

  committed
  ada8491

• Cleanup

  michael-schwarz

  committed
  e7d6302

• Fix memtrack for multi-threaded case

  michael-schwarz

  committed
  e6cee27

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

  mrstanb

  committed
  97eb715

• Add a few more test cases

  mrstanb

  committed
  987795e

• Add options to produce warnings only for memory leaks

  Show description for 8d55024
  mrstanb

  committed
  8d55024

Commits on Nov 20, 2023

• Make SV-COMP validation strict

  sim642

  committed
  ecd48aa

• Merge branch 'master' into svcomp24-dev

  sim642

  committed
  71517e6

• Add ana.autotune.activated schema

  sim642

  committed
  6797cbb

• Deactivate mhp and region for single-threaded programs

  sim642

  committed
  3af192d

• Update SV-COMP releasing guide for 2024

  sim642

  committed
  0ee71a0

Commits on Nov 21, 2023

• Fix invariant_set elements schema in YAML witnesses

  sim642

  committed
  8b79948

• Add example where better privatization helps

  michael-schwarz

  committed
  ca61360

• Merge branch 'master' into svcomp24-dev

  sim642

  committed
  f75a5ac

• Check at end of main thread that the program is certainly single-threaded.

  Show description for 2cc915f
  jerhard

  committed
  2cc915f

• Add test case for memory leaking from a thead that is not joined, add thread_joins to other test cases.

  jerhard

  committed
  45ec8a6

• Add test case with pthread_exit called in main, remove threadid analysis from params as it is not needed.

  jerhard

  committed
  56c4d62

• Add testcases for thread return and pthread_exit in thread different from main.

  jerhard

  committed
  2fef812

• ThreadAnalysis: Handle pthread_exit like return from thread.

  jerhard

  committed
  645b03c

• Use AD.fold instead of List.fold_left

  mrstanb

  committed
  9153eb3

Commits on Nov 22, 2023

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

  Show description for c6cb63e
  

  jerhard

  and

  sim642

  authored
  c6cb63e

• Remove call to free.

  jerhard

  committed
  f12a392

• Add annotation of nowarn next to pthread_exit.

  jerhard

  committed
  be9171b

• Check in TheadAnalysis.return whether the return is actually a threadreturn before side-effecting.

  jerhard

  committed
  585a65d

• Add test case that checking that analysis distinguishes between thread returns and normal returns of a thread.

  jerhard

  committed
  bc7694b

• MemLeak: Do not consider unions

  michael-schwarz

  committed
  666795f

• Add initial CHANGELOG for SV-COMP 2024

  sim642

  committed
  dd45d19

• Add initial CHANGELOG for v2.3.0

  sim642

  committed
  bf754c0

• Add CHANGELOG for v2.3.0

  sim642

  committed
  9c65057

• Merge branch 'master' into svcomp24-dev

  sim642

  committed
  af1ddef

• Merge remote-tracking branch 'mrstanb/improve-valid-memtrack-for-single-threaded-programs' into svcomp24-dev

  sim642

  committed
  765a64e

• Merge remote-tracking branch 'mrstanb/improve-multi-threaded-valid-memcleanup' into svcomp24-dev

  sim642

  committed
  d629d14

Commits on Nov 23, 2023

• Merge branch 'master' into svcomp24-dev

  sim642

  committed
  e0a0692

Commits on Nov 24, 2023

• Merge branch 'master' into svcomp24-dev

  sim642

  committed
  c2e9465