List view

Fix address set meet

bug

unsound

Status: Merged (completed).

goblint/analyzernumber 924

#924 In goblint/analyzer;

· by jerhard was closed on Nov 23, 2022

Add some further library functions

bug

precision

Status: Merged (completed).

goblint/analyzernumber 878

#878 In goblint/analyzer;

· by michael-schwarz was closed on Nov 2, 2022

First approximation of <code>pthread_setspecific</code> by escaping things reachable from the argument and invalidating all globals

bug

unsound

Status: Merged (completed).

goblint/analyzernumber 877

#877 In goblint/analyzer;

· by michael-schwarz was closed on Nov 2, 2022

Generate invariants about local variables again in EvalAssert transformation

bug

cleanupRefactoring, clean-upRefactoring, clean-up

Status: Merged (completed).

goblint/analyzernumber 851

#851 In goblint/analyzer;

· by jerhard was closed on Oct 13, 2022

Use correct <code>ikind</code> for result in <code>inv_exp</code>

bug

hacktoberfest-acceptedhttps://hacktoberfest.digitalocean.com/https://hacktoberfest.digitalocean.com/

precision

Status: Merged (completed).

goblint/analyzernumber 858

#858 In goblint/analyzer;

· by michael-schwarz was closed on Oct 17, 2022

Interval Analysis for Floating-point values

feature

practical-coursePractical Course at TUMPractical Course at TUM

precision

student-job

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

Status: Merged (completed).

goblint/analyzernumber 761

#761 In goblint/analyzer;

· by Dudeldu was closed on Jul 27, 2022

Pass Escaped Locals to Callee as They Need to Be Considered Globals

unsound

Status: Merged (completed).

goblint/analyzernumber 779

#779 In goblint/analyzer;

· by michael-schwarz was closed on Jul 12, 2022

Fix verify errors on sv-benchmarks

bug

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

Status: Merged (completed).

goblint/analyzernumber 827

#827 In goblint/analyzer;

· by sim642 was closed on Sep 20, 2022

Fixed errors when using Unroll ArrayDomain on svcomp-tests

bug

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

Status: Merged (completed).

goblint/analyzernumber 806

#806 In goblint/analyzer;

· by leunam99 was closed on Jul 29, 2022

Autotuning of Configuration

feature

performanceAnalysis time, memory usageAnalysis time, memory usage

precision

student-job

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

Status: Merged (completed).

goblint/analyzernumber 772

#772 In goblint/analyzer;

· by leunam99 was closed on Oct 10, 2022

Add definitions for library functions used in <code>cp</code> program

feature

hacktoberfest-acceptedhttps://hacktoberfest.digitalocean.com/https://hacktoberfest.digitalocean.com/

precision

Status: Merged (completed).

goblint/analyzernumber 865

#865 In goblint/analyzer;

· by michael-schwarz was closed on Oct 26, 2022

var_eq unsoundness with dereferenced floats

bug

cleanupRefactoring, clean-upRefactoring, clean-up

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

unsound

Status: Merged (completed).

goblint/analyzernumber 871

#871 In goblint/analyzer;

· by sim642 was closed on Oct 31, 2022

Equip float domain to handle definite NaN, +Inf, -Inf, and some missing float stubs

feature

precision

Status: Merged (completed).

goblint/analyzernumber 869

#869 In goblint/analyzer;

· by michael-schwarz was closed on Oct 31, 2022

Add <code>abortUnless</code> analysis

feature

precision

Status: Merged (completed).

goblint/analyzernumber 875

#875 In goblint/analyzer;

· by michael-schwarz was closed on Nov 3, 2022

SV-COMP 2023 setup

hacktoberfest-acceptedhttps://hacktoberfest.digitalocean.com/https://hacktoberfest.digitalocean.com/

setupDependencies, CI, releasingDependencies, CI, releasing

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

Status: Merged (completed).

goblint/analyzernumber 859

#859 In goblint/analyzer;

· by sim642 was closed on Oct 24, 2022

Fix base Invariant query lval and offset handling

bug

hacktoberfest-acceptedhttps://hacktoberfest.digitalocean.com/https://hacktoberfest.digitalocean.com/

Status: Merged (completed).

goblint/analyzernumber 861

#861 In goblint/analyzer;

· by sim642 was closed on Oct 19, 2022

Fix EvalAssert transformation to work on coreutil programs

benchmarking

bug

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

Status: Merged (completed).

goblint/analyzernumber 855

#855 In goblint/analyzer;

· by jerhard was closed on Oct 28, 2022

Catch <code>Top</code> case for <code>TS.elements</code> call in <code>threadAnalysis</code>

bug

Status: Merged (completed).

goblint/analyzernumber 907

#907 In goblint/analyzer;

· by michael-schwarz was closed on Nov 16, 2022

Add library functions for <code>__atomic_{store,load}_n</code>

c11

precision

Status: Merged (completed).

goblint/analyzernumber 884

#884 In goblint/analyzer;

· by michael-schwarz was closed on Nov 4, 2022

Add missing <code>__VERIFIER_nondet_X()</code>s

precision

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

Status: Merged (completed).

goblint/analyzernumber 886

#886 In goblint/analyzer;

· by michael-schwarz was closed on Nov 7, 2022

Do not produce overflow warnings from Apron &amp; Unroll typedefs for <code>invariant</code>

bug

precision

Status: Merged (completed).

goblint/analyzernumber 890

#890 In goblint/analyzer;

· by michael-schwarz was closed on Nov 7, 2022

Handle overflows in congruence domain more precisely

precision

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

Status: Merged (completed).

goblint/analyzernumber 894

#894 In goblint/analyzer;

· by jerhard was closed on Nov 16, 2022

Fix handling of labels in unrolling &amp; add possibility to run CIL checks on CFGs

bug

pr-dependencyDepends or builds on another PR, which should be merged beforeDepends or builds on another PR, which should be merged before

Status: Merged (completed).

goblint/analyzernumber 896

#896 In goblint/analyzer;

· by michael-schwarz was closed on Nov 10, 2022

Autotune: Conditionally activate congruence integer domain

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

Status: Merged (completed).

goblint/analyzernumber 911

#911 In goblint/analyzer;

· by jerhard was closed on Nov 22, 2022

Fix Apron reading globals with offsets

bug

performanceAnalysis time, memory usageAnalysis time, memory usage

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

Status: Merged (completed).

goblint/analyzernumber 916

#916 In goblint/analyzer;

· by sim642 was closed on Nov 18, 2022