Issues
- 11
Parsing Error
#1564 opened by pvouzis - 0
Refine using YAML violation witnesses
#1567 opened by sim642 - 4
- 0
Make use of OCaml 4.14 features
#1477 opened by sim642 - 0
Avoid populating `dep` table in TD3 when non-incremental
#1566 opened by sim642 - 0
- 2
- 7
Mutex-Meet-TID less precise than Mutex-Meet
#1557 opened by michael-schwarz - 2
Mutex-Meet unsound (function pointers get lost)
#1558 opened by michael-schwarz - 13
`Mutex-Meet-TID` without clusters more precise than approach with clusters
#1551 opened by michael-schwarz - 0
Preprocessing not compatible with Linux arm64
#1556 opened by sim642 - 0
Clean up library function spawning in base analysis
#1553 opened by sim642 - 5
Both branches dead in char_generic_nvram_read_nvram_write_nvram.i with octagon enabled analysis
#1498 opened by DrMichaelPetter - 3
Apron: Both branches dead after malloc
#1489 opened by michael-schwarz - 2
Timing for multithreaded use
#1550 opened by FelixKrayer - 4
- 4
Apron: Both branches dead when branching over global variable declared as `extern`
#1482 opened by michael-schwarz - 3
- 0
Investigate instances of `fold_right`
#1536 opened by michael-schwarz - 0
YAML: Relational invariants about escaped variables are incorrect (due to Apron->CIL conversion not considering escaping)
#1547 opened by michael-schwarz - 0
Verified Polyhedra Library support
#1548 opened by sim642 - 12
- 1
Clear up meaning of `MayEscape` & Distinguish a local becoming reachable via globals from being reachable by other threads
#1544 opened by michael-schwarz - 7
Narrowing with bottom does not produce bottom
#1540 opened by Red-Panda64 - 4
Validation of YAML witnesses takes undue amount of time compared to analyis
#1539 opened by michael-schwarz - 14
Printing of `Apron` values very slow
#1513 opened by michael-schwarz - 1
Emit invariants for static global variables
#1538 opened by michael-schwarz - 4
YAML witnesses get evaluated at unrelated nodes
#1537 opened by michael-schwarz - 1
`Relational Analyses`: Deep invalidation for library functions havocs all variables (also those that don't have their address taken)
#1535 opened by michael-schwarz - 1
Reconsider not writing to known addresses if a pointer contains an unknown element
#1461 opened by michael-schwarz - 0
Relational analysis always populates result table even when not dumping
#1526 opened by michael-schwarz - 2
`BaseAnalysis`: Investigate why `join` over alternatives for non-definite AD target does not work
#1465 opened by michael-schwarz - 8
Spurious segfaults in sv-benchmarks runs
#1520 opened by sim642 - 0
Provide a description in the opam file
#1528 opened by michael-schwarz - 1
Investigate replacing `Set` with François Pottier's sets from the `baby` library
#1525 opened by michael-schwarz - 0
JSON5 conf files
#1524 opened by sim642 - 2
- 4
Strange overflow behaviour
#1499 opened by DrMichaelPetter - 1
SV-Comp incorrect result in no-overflow tasks
#1501 opened by DrMichaelPetter - 0
Narrowing by fixed number of `meet`s
#1494 opened by sim642 - 4
- 0
Setup issues with Ubuntu 24.04
#1488 opened by michael-schwarz - 5
Apron: Both branches dead due to escaping local
#1479 opened by michael-schwarz - 1
- 3
- 2
Interval sets are unsound due to larger-than-type ranges
#1473 opened by sim642 - 5
SV-COMP autotuner spuriously enables all integer domains
#1472 opened by sim642 - 1
- 2
- 0
Affine Equalities Mostly Contain Only Small Portions of Actual Information
#1459 opened by DrMichaelPetter