-
Notifications
You must be signed in to change notification settings - Fork 77
Issues: goblint/analyzer
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.
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
Author
Label
Projects
Milestones
Assignee
Sort
Issues list
Remove support for GraphML witnesses?
cleanup
Refactoring, clean-up
performance
Analysis time, memory usage
sv-comp
SV-COMP (analyses, results), witnesses
Questionable invariants in SV-COMP 2025 witnesses
sv-comp
SV-COMP (analyses, results), witnesses
unsound
usability
Experiment with unassume for mutex analysis
feature
performance
Analysis time, memory usage
proof-of-concept
sv-comp
SV-COMP (analyses, results), witnesses
Vojdani privatization may output read-unprotected variables to witnesses
pr-dependency
Depends or builds on another PR, which should be merged before
sv-comp
SV-COMP (analyses, results), witnesses
#1713
opened Mar 17, 2025 by
sim642
Remaining verdicts SV-COMP (analyses, results), witnesses
Error (both branches dead)
on SV-COMP
bug
sv-comp
SVCOMP: Investigate / Come up with autotuners for new features
relational
Relational analyses (Apron, affeq, lin2var)
sv-comp
SV-COMP (analyses, results), witnesses
Inequalities between pointers do not work
good first issue
precision
sv-comp
SV-COMP (analyses, results), witnesses
Add abstract interface to Refactoring, clean-up
sv-comp
SV-COMP (analyses, results), witnesses
type-safety
Type-safety improvements
Invariant
cleanup
Minimize unnecessary casts and check for overflows in witness invariants
explainability
pr-dependency
Depends or builds on another PR, which should be merged before
relational
Relational analyses (Apron, affeq, lin2var)
sv-comp
SV-COMP (analyses, results), witnesses
Refine float-integer casts in SV-COMP (analyses, results), witnesses
BaseInvariant
feature
precision
sv-comp
#1632
opened Nov 26, 2024 by
sim642
Simplify relational witness invariants
feature
sv-comp
SV-COMP (analyses, results), witnesses
usability
valid-memtrack analysis doesn't check sizes, only checks at end & doesn't consider locals
bug
sv-comp
SV-COMP (analyses, results), witnesses
unsound
Atomic signed integer overflows should not violate SV-COMP no-overflow property
feature
precision
sv-comp
SV-COMP (analyses, results), witnesses
#1621
opened Nov 5, 2024 by
sim642
Imprecise cast overflows in sv-benchmarks
in progress
precision
sv-comp
SV-COMP (analyses, results), witnesses
#1586
opened Sep 30, 2024 by
sim642
13 tasks
Refine using YAML violation witnesses
feature
precision
sv-comp
SV-COMP (analyses, results), witnesses
#1567
opened Sep 10, 2024 by
sim642
Spurious overflow warnings due to partitioned arrays in globals
bug
precision
sv-comp
SV-COMP (analyses, results), witnesses
#1565
opened Sep 6, 2024 by
sim642
Preprocessing not compatible with Linux arm64
bug
preprocessing
C preprocessing
setup
Dependencies, CI, releasing
sv-comp
SV-COMP (analyses, results), witnesses
#1556
opened Aug 7, 2024 by
sim642
Validation of YAML witnesses takes undue amount of time compared to analyis
bug
performance
Analysis time, memory usage
sv-comp
SV-COMP (analyses, results), witnesses
#1539
opened Jul 8, 2024 by
michael-schwarz
Emit invariants for static global variables
bug
relational
Relational analyses (Apron, affeq, lin2var)
sv-comp
SV-COMP (analyses, results), witnesses
#1538
opened Jul 7, 2024 by
michael-schwarz
Remove restriction that no loop unrolling is done when breaks are in the loop
precision
sv-comp
SV-COMP (analyses, results), witnesses
SV-COMP autotuner spuriously enables all integer domains
bug
performance
Analysis time, memory usage
precision
sv-comp
SV-COMP (analyses, results), witnesses
unsound
usability
Previous Next
ProTip!
Exclude everything labeled
bug
with -label:bug.