issues
search
goblint
/
analyzer
Static analysis framework for C
https://goblint.in.tum.de
MIT License
160
stars
72
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Clean up `destabilize_vs`
#1434
Red-Panda64
closed
1 month ago
2
Dubious code duplication in `destabilize_vs`
#1433
Red-Panda64
opened
2 months ago
9
Multiset domain for recursive must-locksets
#1432
sim642
opened
2 months ago
0
More useful stats output by privPrecCompare
#1431
michael-schwarz
closed
2 months ago
3
Refactor must-locksets to use definite mvals instead of addresses
#1430
sim642
closed
1 month ago
2
Fix SV-COMP Apron unassume crash
#1429
sim642
closed
2 months ago
0
Investigate apron, apron2, termination and OSX "Excellent: ignored check"-s
#1428
sim642
closed
2 months ago
0
Pass `ctx` to context & Simplify callstring-based approaches
#1427
michael-schwarz
closed
1 month ago
1
MacOS CI newly fails
#1426
michael-schwarz
closed
2 months ago
1
Investigate all "Excellent: ignored check"-s
#1425
sim642
opened
2 months ago
5
Improve `dune runtest` output
#1424
sim642
closed
2 months ago
0
Type-safe global query system
#1423
sim642
opened
2 months ago
3
Dedicated Context Constructions for Termination Analysis
#1422
michael-schwarz
opened
2 months ago
0
Crash on `pthread_mutex_lock` with complicated argument
#1421
michael-schwarz
opened
2 months ago
5
`dbg.timeout` somtimes not respected
#1420
michael-schwarz
closed
1 month ago
3
Missing division by zero treatment in MaySignedOverflow
#1419
DrMichaelPetter
closed
2 months ago
1
Unsoundness for `malloc(0)`
#1418
michael-schwarz
opened
2 months ago
2
Tracking Benchmark Changes for Thesis
#1417
michael-schwarz
opened
2 months ago
3
Fix pthread mutex type from initializer on OSX
#1416
sim642
closed
2 months ago
0
Document implementation-defined behavior following GCC
#1415
michael-schwarz
opened
2 months ago
0
`PTHREAD_MUTEX_DEFAULT` handling is unsound
#1414
sim642
closed
2 months ago
2
`DefExc`,`Enums`: More precise `of_interval` and `starting` and `ending`
#1413
michael-schwarz
closed
2 months ago
5
Lin2var relations fine-tuning - switching from array to map
#1412
DrMichaelPetter
closed
1 month ago
5
Add flag `AnalysisState.executing_speculative_computations` to avoid flagging overflows during `invariant`
#1411
michael-schwarz
closed
2 months ago
2
Fix NULL pointer dereference error for NULL mutexattr
#1410
sim642
closed
2 months ago
0
Check semantic indices of unlocked mutex
#1409
sim642
closed
3 months ago
0
Improve `invariant` for unsigned types
#1408
michael-schwarz
closed
2 months ago
0
Avoid emitting reflexive pointer refines for locking
#1407
sim642
closed
1 month ago
1
Suppress Overflow Warnings for Computations Not in the Program
#1406
michael-schwarz
closed
3 months ago
0
Improve output for `NullByte`
#1405
michael-schwarz
closed
3 months ago
0
Move unit tests to tests/unit/
#1404
sim642
closed
3 months ago
0
Record statement copies during loop unrolling
#1403
sim642
closed
3 months ago
1
Disable SV-COMP syntactic loop unrolling
#1402
sim642
closed
3 months ago
2
Bump actions/configure-pages from 4 to 5
#1401
dependabot[bot]
closed
3 months ago
0
Change YAML witness columns to 1-indexed
#1400
sim642
closed
2 months ago
0
Ego-Lane-Derived-Digests for Privatizations: `Lock- ` & `Write-Centered` Privatizations
#1399
michael-schwarz
closed
3 months ago
0
Ego-Lane-Derived-Digests for Privatizations: `ProtectionBasedTIDPriv`
#1398
michael-schwarz
closed
3 months ago
1
Introduce `Analyses.IdentityUnitContextsSpec` & Replace `Lattice.Unit` contexts with `Printable.Unit`
#1397
michael-schwarz
closed
3 months ago
0
Avoid base invariant fallback not understood message on reflexive pointer literal equality
#1396
sim642
closed
3 months ago
7
Use ppx_deriving_hash 0.1.2
#1395
sim642
closed
3 months ago
5
Generate flow-insensitive YAML witness invariants with ghosts for privatized variables
#1394
sim642
opened
3 months ago
0
Automatically add newline to trace output
#1393
sim642
closed
3 months ago
2
Improve `dune runtest` output
#1392
sim642
opened
3 months ago
0
Cannot have `location_invariant` before loop in witness
#1391
sim642
opened
3 months ago
0
Fix alloc varinfo name with no thread ID but with counter
#1390
sim642
closed
3 months ago
0
Marshall CIL file for GobView
#1389
stilscher
closed
3 months ago
0
With `dbg.full-output` off: Combination of `ana.malloc.unique_address_count` >= `2` &`threadid` analysis deactivated unsound
#1388
michael-schwarz
closed
3 months ago
2
Fix test for relational unassume with strengthening
#1387
sim642
closed
3 months ago
0
Improve output for `NullByte` domain
#1386
michael-schwarz
closed
3 months ago
0
Unsoundness on SV-COMP for No-Overflow & Memory Properties
#1385
michael-schwarz
opened
3 months ago
3
Previous
Next