List view

Location fixes for YAML witness generation/validation

bug

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

Status: Merged (completed).

goblint/analyzernumber 1372

#1372 In goblint/analyzer;

· by sim642 was closed on Apr 4, 2024

Add cram tests for YAML witnesses

bug

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

testing

Status: Merged (completed).

goblint/analyzernumber 1357

#1357 In goblint/analyzer;

· by sim642 was closed on Apr 4, 2024

Add option witness.invariant.all-locals to only print locals definitely in scope

feature

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

Status: Merged (completed).

goblint/analyzernumber 1362

#1362 In goblint/analyzer;

· by michael-schwarz was closed on Feb 19, 2024

Unroll typedefs in witness invariants

bug

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

Status: Merged (completed).

goblint/analyzernumber 1375

#1375 In goblint/analyzer;

· by sim642 was closed on Apr 5, 2024

Improve autotune for octagon

precision

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

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

Status: Merged (completed).

goblint/analyzernumber 1450

#1450 In goblint/analyzer;

· by karoliineh was closed on May 23, 2024

Fix enums domain to not emit witness invariants for top booleans

bug

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

Status: Merged (completed).

goblint/analyzernumber 1436

#1436 In goblint/analyzer;

· by sim642 was closed on Apr 29, 2024

Adjust loop unrolling defaults

performanceAnalysis time, memory usageAnalysis time, memory usage

precision

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

Status: Merged (completed).

goblint/analyzernumber 1584

#1584 In goblint/analyzer;

· by karoliineh was closed on Oct 2, 2024

Do not unroll loops in stub functions

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

Status: Merged (completed).

goblint/analyzernumber 1583

#1583 In goblint/analyzer;

· by karoliineh was closed on Sep 30, 2024

Refactor loopUnrolling autotuner

cleanupRefactoring, clean-upRefactoring, clean-up

Status: Merged (completed).

goblint/analyzernumber 1582

#1582 In goblint/analyzer;

· by karoliineh was closed on Sep 30, 2024

Change Machdep based on SV-COMP architecture

feature

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

unsound

Status: Merged (completed).

goblint/analyzernumber 1574

#1574 In goblint/analyzer;

· by sim642 was closed on Oct 2, 2024

Change YAML witness columns to 1-indexed

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

Status: Merged (completed).

goblint/analyzernumber 1400

#1400 In goblint/analyzer;

· by sim642 was closed on Apr 15, 2024

Update results table in relationalAnalysis only if exp.relation.prec-dump is set

performanceAnalysis time, memory usageAnalysis time, memory usage

Status: Merged (completed).

goblint/analyzernumber 1530

#1530 In goblint/analyzer;

· by karoliineh was closed on Jun 28, 2024

Remove fixed malloc wrappers from svcomp conf

cleanupRefactoring, clean-upRefactoring, clean-up

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

Status: Merged (completed).

goblint/analyzernumber 1592

#1592 In goblint/analyzer;

· by sim642 was closed on Oct 5, 2024

Remove witness exclude-vars from svcomp conf

cleanupRefactoring, clean-upRefactoring, clean-up

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

Status: Merged (completed).

goblint/analyzernumber 1593

#1593 In goblint/analyzer;

· by sim642 was closed on Oct 22, 2024

Record statement copies during loop unrolling

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

Status: Merged (completed).

goblint/analyzernumber 1403

#1403 In goblint/analyzer;

· by sim642 was closed on Apr 4, 2024

Fix witness enter sync map when caller state changes

bug

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

Status: Merged (completed).

goblint/analyzernumber 1462

#1462 In goblint/analyzer;

· by sim642 was closed on May 27, 2024

Separate soundness settings from precision improvements in the autotuner

cleanupRefactoring, clean-upRefactoring, clean-up

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

unsound

unsound-usability

usability

Status: Merged (completed).

goblint/analyzernumber 1469

#1469 In goblint/analyzer;

· by karoliineh was closed on May 23, 2024

Add ARG tests

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

testing

Status: Merged (completed).

goblint/analyzernumber 1470

#1470 In goblint/analyzer;

· by sim642 was closed on May 27, 2024

Make privatization sync Join more precise when threadflag is path-sensitive

performanceAnalysis time, memory usageAnalysis time, memory usage

precision

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

Status: Merged (completed).

goblint/analyzernumber 1475

#1475 In goblint/analyzer;

· by sim642 was closed on May 22, 2024

Add primitive verdict-based YAML violation witness rejection

feature

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

Status: Merged (completed).

goblint/analyzernumber 1512

#1512 In goblint/analyzer;

· by sim642 was closed on Sep 10, 2024

Check overflows when generating witnesses

bug

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

unsound

Status: Merged (completed).

goblint/analyzernumber 1546

#1546 In goblint/analyzer;

· by michael-schwarz was closed on Jul 17, 2024

Fix SV-COMP Apron unassume crash

bug

Status: Merged (completed).

goblint/analyzernumber 1429

#1429 In goblint/analyzer;

· by sim642 was closed on Apr 23, 2024

Activate abortUnless in svcomp conf

feature

precision

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

Status: Merged (completed).

goblint/analyzernumber 1464

#1464 In goblint/analyzer;

· by sim642 was closed on May 27, 2024

make cil_exp_of_linexpr1 work with fractional expressions

bug

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

Status: Merged (completed).

goblint/analyzernumber 1493

#1493 In goblint/analyzer;

· by DrMichaelPetter was closed on Jul 2, 2024

Consider all spawning functions in autotuner

bug

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

unsound

Status: Merged (completed).

goblint/analyzernumber 1604

#1604 In goblint/analyzer;

· by sim642 was closed on Oct 24, 2024