List view

Use generic <code>Spec</code> lifters for delayed widening

cleanupRefactoring, clean-upRefactoring, clean-up

Status: Merged (completed).

goblint/analyzernumber 1731

#1731 In goblint/analyzer;

· by sim642 was closed on Apr 18, 2025

Weaken <code>Lattice.Lift{,2}Conf</code> arguments, remove <code>Lattice.LiftPO</code>

cleanupRefactoring, clean-upRefactoring, clean-up

type-safetyType-safety improvementsType-safety improvements

Status: Merged (completed).

goblint/analyzernumber 1728

#1728 In goblint/analyzer;

· by sim642 was closed on Apr 17, 2025

Remove dummy <code>top</code> and <code>is_top</code> implementations from int domains

bug

cleanupRefactoring, clean-upRefactoring, clean-up

type-safetyType-safety improvementsType-safety improvements

unsound

Status: Merged (completed).

goblint/analyzernumber 1727

#1727 In goblint/analyzer;

· by sim642 was closed on Apr 17, 2025

Document def_exc and enums exclusion bit range assumption

documentationDocumentation, commentsDocumentation, comments

Status: Merged (completed).

goblint/analyzernumber 1726

#1726 In goblint/analyzer;

· by sim642 was closed on Apr 15, 2025

Explicitly specify no-argument function pointers in tests

cleanupRefactoring, clean-upRefactoring, clean-up

testing

type-safetyType-safety improvementsType-safety improvements

Status: Merged (completed).

goblint/analyzernumber 1724

#1724 In goblint/analyzer;

· by sim642 was closed on Apr 22, 2025

Fallback for malloc uniqueness for when threading analyses are disabled

precision

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

Status: Merged (completed).

goblint/analyzernumber 1721

#1721 In goblint/analyzer;

· by michael-schwarz was closed on Apr 9, 2025

<code>IsMultiple</code> in <code>MallocWrapper</code>: Check uniqueness of allocating(!) thread

bug

precision

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

unsound

Status: Merged (completed).

goblint/analyzernumber 1720

#1720 In goblint/analyzer;

· by michael-schwarz was closed on Mar 27, 2025

Goblint cannot handle even simple cases of malloc'ed mutexes

precision

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

Status: Closed (completed).

Feature

#1719 In goblint/analyzer;

· by michael-schwarz was closed on Mar 27, 2025

Change YAML witness generation default to version 2.0 with only <code>invariant_set</code>

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

usability

Status: Merged (completed).

goblint/analyzernumber 1718

#1718 In goblint/analyzer;

· by sim642 was closed on Apr 18, 2025

Use LazyEval instead of Lazy in C2PODomain.

relationalRelational analyses (Apron, affeq, lin2var)Relational analyses (Apron, affeq, lin2var)

testing

Status: Merged (completed).

goblint/analyzernumber 1717

#1717 In goblint/analyzer;

· by jerhard was closed on Mar 26, 2025

Fix test 82/04

bug

testing

Status: Merged (completed).

goblint/analyzernumber 1714

#1714 In goblint/analyzer;

· by arkocal was closed on Mar 21, 2025

Update 56-witness/*-tm-inv-tranfer* tests

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

testing

Status: Merged (completed).

goblint/analyzernumber 1707

#1707 In goblint/analyzer;

· by sim642 was closed on Mar 27, 2025

Fix flaky cram tests where <code>vid</code>s leak into witnesses

bug

testing

Status: Merged (completed).

goblint/analyzernumber 1703

#1703 In goblint/analyzer;

· by michael-schwarz was closed on Mar 5, 2025

Fix refinement in <code>baseInvariant</code> for more complicated lvals

bug

unsound

Status: Merged (completed).

goblint/analyzernumber 1701

#1701 In goblint/analyzer;

· by michael-schwarz was closed on Mar 3, 2025

Unit tests: Remove usages of polymorphic equality

bug

testing

Status: Merged (completed).

goblint/analyzernumber 1695

#1695 In goblint/analyzer;

· by michael-schwarz was closed on Mar 4, 2025

Extract generic <code>Spec</code> domain and context lifters

cleanupRefactoring, clean-upRefactoring, clean-up

Status: Merged (completed).

goblint/analyzernumber 1692

#1692 In goblint/analyzer;

· by sim642 was closed on Mar 4, 2025

HashCachedContextLifter: Introduce the lifter and the option

feature

performanceAnalysis time, memory usageAnalysis time, memory usage

Status: Merged (completed).

goblint/analyzernumber 1690

#1690 In goblint/analyzer;

· by arkocal was closed on Feb 20, 2025

Audit usages of <code>fold_right</code>

cleanupRefactoring, clean-upRefactoring, clean-up

Status: Merged (completed).

goblint/analyzernumber 1688

#1688 In goblint/analyzer;

· by michael-schwarz was closed on Feb 24, 2025

DefExc: unit tests use polymorphic equality

good first issue

testing

Status: Closed (completed).

Bug

#1686 In goblint/analyzer;

· by michael-schwarz was closed on Mar 4, 2025

Ensure that <code>__goblint_check</code> does not affect memLeak analysis

bug

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

testing

Status: Merged (completed).

goblint/analyzernumber 1682

#1682 In goblint/analyzer;

· by karoliineh was closed on Feb 17, 2025

Change <code>Offset.MakeLattice.to_index</code> to return bytes, not bits

bug

cleanupRefactoring, clean-upRefactoring, clean-up

unsound

Status: Merged (completed).

goblint/analyzernumber 1679

#1679 In goblint/analyzer;

· by sim642 was closed on Feb 17, 2025

memLeak analysis is affected by <code>__goblint_check</code>

good first issue

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

testing

Status: Closed (completed).

Bug

#1678 In goblint/analyzer;

· by sim642 was closed on Feb 17, 2025

Add missing type unrollings

cleanupRefactoring, clean-upRefactoring, clean-up

precision

Status: Merged (completed).

goblint/analyzernumber 1677

#1677 In goblint/analyzer;

· by sim642 was closed on Mar 4, 2025

Enums: Take care in refinement that no new elements appear

bug

Status: Merged (completed).

goblint/analyzernumber 1675

#1675 In goblint/analyzer;

· by michael-schwarz was closed on Feb 12, 2025

Fixpoint not reached because narrowing for Enums does not guarantee termination

Status: Closed (completed).

Bug

#1673 In goblint/analyzer;

· by michael-schwarz was closed on Feb 12, 2025