goblint/analyzer

Issues

• Strange overflow behaviour

  #1499 opened 7 months ago
  4

• Both branches dead in char_generic_nvram_read_nvram_write_nvram.i with octagon enabled analysis

  #1498 opened 5 months ago
  5

• Narrowing by fixed number of `meet`s

  #1494 opened 7 months ago
  0

• Proposal: Unify handling of malloc and escaping locals

  #1491 opened 7 months ago
  2

• ApronPrecCompare runs >= 35h and consumes 40GB of RAM

  #1490 opened 7 months ago
  4

• Apron: Both branches dead after malloc

  #1489 opened 5 months ago
  3

• Setup issues with Ubuntu 24.04

  #1488 opened 10 days ago
  1

• Relational: `exp.hide-std-globals` makes analysis unsound

  #1486 opened 7 months ago
  1

• Apron: Both branches dead when branching over global variable declared as `extern`

  #1482 opened 7 months ago
  4

• Apron: Both branches dead due to escaping local

  #1479 opened 7 months ago
  5

• Fixpoint not reached with Octagons and `assume_overflow` = `None`

  #1478 opened 7 months ago
  4

• Make use of OCaml 4.14 features

  #1477 opened 7 months ago
  0

• Regression from #1427: Calls to `top ()` where that is unsupported

  #1474 opened 7 months ago
  3

• Interval sets are unsound due to larger-than-type ranges

  #1473 opened 7 months ago
  2

• SV-COMP autotuner spuriously enables all integer domains

  #1472 opened 7 months ago
  5

• Meet of string pointers in address domain imprecise

  #1467 opened 7 months ago
  1

• `BaseAnalysis`: Investigate why `join` over alternatives for non-definite AD target does not work

  #1465 opened 7 months ago
  2

• Reconsider not writing to known addresses if a pointer contains an unknown element

  #1461 opened 7 months ago
  1

• Affine Equalities Mostly Contain Only Small Portions of Actual Information

  #1459 opened 7 months ago
  0

• All Non-Relational Privatizations except Miné-W unsound

  #1457 opened 7 months ago
  2

• Protection-Based Privatization more Precise than Write-Centered

  #1456 opened 7 months ago
  11

• Refinement causes (spurious) reports of unreached fixpoints

  #1455 opened 8 months ago
  2

• `ID.project` to enable additional domains only works when `ana.int.refinement` is activated

  #1454 opened 8 months ago
  0

• Witness generation crashes in `combine_env` with abortUnless analysis

  #1453 opened 7 months ago
  0

• Improve output for component of blob indicating whether it was created with `malloc` or `calloc`

  #1451 opened 7 months ago
  1

• Split octagon autotuner to separate octagonAnalysis and octagonVars autotuners

  #1449 opened 8 months ago
  1

• Housekeeping relational analyses

  #1446 opened 8 months ago
  8

• Relational mutex-meet unsound on ConcurrencySafety-Main

  #1440 opened 3 months ago
  8

• Rename `ctx`

  #1438 opened 9 days ago
  0

• Switch from `BatEnum` to `Seq`

  #1437 opened 8 months ago
  0

• Dubious code duplication in `destabilize_vs`

  #1433 opened 8 months ago
  9

• Multiset domain for recursive must-locksets

  #1432 opened 8 months ago
  0

• MacOS CI newly fails

  #1426 opened 8 months ago
  1

• Inconsistent behavior for startstate in incremental analysis based on whether AST or CFG comparison is used

  #1425 opened 8 months ago
  5

• Dedicated Context Constructions for Termination Analysis

  #1422 opened 8 months ago
  0

• Crash on `pthread_mutex_lock` with complicated argument

  #1421 opened 8 months ago
  5

• `dbg.timeout` somtimes not respected

  #1420 opened 8 months ago
  3

• Unsoundness for `malloc(0)`

  #1418 opened 8 months ago
  2

• Improve `dune runtest` output

  #1392 opened 10 months ago
  0

• Cannot have `location_invariant` before loop in witness

  #1391 opened 10 months ago
  0

• With `dbg.full-output` off: Combination of `ana.malloc.unique_address_count` >= `2` &`threadid` analysis deactivated unsound

  #1388 opened 10 months ago
  2

• Improve output for `NullByte` domain

  #1386 opened 9 months ago
  0

• Unsoundness on SV-COMP for No-Overflow & Memory Properties

  #1385 opened 2 months ago
  4

• qcheck-ounit missing from make dev

  #1384 opened 10 months ago
  1

• `make setup` segfault

  #1383 opened 10 months ago
  5

• `tnliboG` framework for backwards analysis

  #1382 opened 10 months ago
  0

• `--enable justcil` does not print `__attribute__((__goblint_relation_track__))` for formals of functions

  #1381 opened 10 months ago
  2

• Principled fix for Apron-Domain Top

  #1380 opened 10 months ago
  1

• First-Class Support for Callstring-derived Contexts

  #1379 opened 7 months ago
  1

• Replace `Lattice.Unit` contexts in analyses with `Printable.Unit`

  #1378 opened 9 months ago
  0