goblint/analyzer

Issues

• JSON5 conf files

  #1524 opened 6 months ago by sim642
  1

• valid-memtrack analysis doesn't check sizes, only checks at end & doesn't consider locals

  #1622 opened 2 months ago by sim642
  8

• `thread` analysis requires context-sensitive threadids

  #1615 opened 2 months ago by michael-schwarz
  6

• Atomic signed integer overflows should not violate SV-COMP no-overflow property

  #1621 opened 2 months ago by sim642
  0

• Use CIL `fallthrough` field for CFG construction

  #1620 opened 2 months ago by sim642
  0

• Error message from library mechanism are unhelpful to users

  #1616 opened 2 months ago by michael-schwarz
  3

• Fix code scanning alert - Semgrep Finding: semgrep.fold-exists

  #1618 opened 2 months ago by michael-schwarz
  1

• Apron analysis does not support trivial assertions

  #1610 opened 2 months ago by sim642
  3

• Quickcheck int domain abstract operation properties

  #1609 opened 2 months ago by sim642
  0

• Investigate soundness of boundedness check for termination

  #1608 opened 2 months ago by sim642
  0

• Audit for missing type unrollings

  #1600 opened 2 months ago by sim642
  0

• Variable hashes have too many collisions

  #1594 opened 2 months ago by arkocal
  15

• Avoid populating `dep` table in TD3 when non-incremental

  #1566 opened 4 months ago by sim642
  0

• sv-benchmarks unsoundness pre-SV-COMP 2025

  #1578 opened 3 months ago by sim642
  0

• SV-Comp incorrect result in no-overflow tasks

  #1501 opened 2 months ago by DrMichaelPetter
  3

• Consider submitting C2PO tests to SV-COMP

  #1571 opened 3 months ago by michael-schwarz
  3

• Spurious segfaults in sv-benchmarks runs

  #1520 opened 3 months ago by sim642
  9

• Use sets for widening thresholds instead of lists

  #1591 opened 3 months ago by sim642
  0

• Imprecise cast overflows in sv-benchmarks

  #1586 opened 3 months ago by sim642
  0

• `ERROR` verdict for both branches dead in SV-COMP

  #1576 opened 3 months ago by sim642
  4

• Success messages with topological sorting from deadlock analysis

  #1581 opened 3 months ago by sim642
  0

• Success messages with bounds from termination analysis

  #1577 opened 3 months ago by sim642
  2

• Provide per-fundec context gas

  #1569 opened 3 months ago by michael-schwarz
  0

• Handle `Lattice.BotValue` in `Lattice.LiftBot` and similar

  #1572 opened 3 months ago by sim642
  0

• Parsing Error

  #1564 opened 4 months ago by pvouzis
  11

• Refine using YAML violation witnesses

  #1567 opened 4 months ago by sim642
  0

• Running on coreutils yields exception from library mechansim

  #1541 opened 4 months ago by michael-schwarz
  4

• Spurious overflow warnings due to partitioned arrays in globals

  #1565 opened 4 months ago by sim642
  0

• Mutex-Meet-TID less precise than Mutex-Meet

  #1557 opened 5 months ago by michael-schwarz
  7

• Mutex-Meet unsound (function pointers get lost)

  #1558 opened 5 months ago by michael-schwarz
  2

• `Mutex-Meet-TID` without clusters more precise than approach with clusters

  #1551 opened 5 months ago by michael-schwarz
  13

• Preprocessing not compatible with Linux arm64

  #1556 opened 5 months ago by sim642
  0

• Clean up library function spawning in base analysis

  #1553 opened 5 months ago by sim642
  0

• Timing for multithreaded use

  #1550 opened 5 months ago by FelixKrayer
  2

• Investigate: Need for `sides-pp` widening strategy exacerbated

  #1507 opened 6 months ago by michael-schwarz
  3

• Investigate instances of `fold_right`

  #1536 opened 6 months ago by michael-schwarz
  0

• YAML: Relational invariants about escaped variables are incorrect (due to Apron->CIL conversion not considering escaping)

  #1547 opened 5 months ago by michael-schwarz
  0

• Verified Polyhedra Library support

  #1548 opened 5 months ago by sim642
  0

• Apron: Invariants for variables of type `unsigned long` wrong

  #1542 opened 6 months ago by michael-schwarz
  12

• Clear up meaning of `MayEscape` & Distinguish a local becoming reachable via globals from being reachable by other threads

  #1544 opened 5 months ago by michael-schwarz
  1

• Narrowing with bottom does not produce bottom

  #1540 opened 5 months ago by Red-Panda64
  7

• Validation of YAML witnesses takes undue amount of time compared to analyis

  #1539 opened 6 months ago by michael-schwarz
  4

• Printing of `Apron` values very slow

  #1513 opened 6 months ago by michael-schwarz
  14

• Emit invariants for static global variables

  #1538 opened 6 months ago by michael-schwarz
  1

• YAML witnesses get evaluated at unrelated nodes

  #1537 opened 6 months ago by michael-schwarz
  4

• `Relational Analyses`: Deep invalidation for library functions havocs all variables (also those that don't have their address taken)

  #1535 opened 6 months ago by michael-schwarz
  1

• Relational analysis always populates result table even when not dumping

  #1526 opened 6 months ago by michael-schwarz
  0

• Provide a description in the opam file

  #1528 opened 6 months ago by michael-schwarz
  0

• Investigate replacing `Set` with François Pottier's sets from the `baby` library

  #1525 opened 6 months ago by michael-schwarz
  1

• Reconsider notion of path-sensitive but context-insensitive analysis

  #1509 opened 7 months ago by michael-schwarz
  2