Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Static analysis framework for C
CHANGES:
setjmp
/longjmp
analysis (Soundly handlesetjmp
andlongjmp
goblint/analyzer#887, Analysis of longjmp/setjmp goblint/analyzer#970, Refactorsetjmp
/longjmp
analysis goblint/analyzer#1015, Autotuner forlongjmp
goblint/analyzer#1019).Base.combine
goblint/analyzer#553, Taint analysis to improve the precision loss of partial contexts goblint/analyzer#952).all_array_index_exp
goblint/analyzer#1044, Witness invariants for arrays and principled handling of unknown indices goblint/analyzer#1045, Unassume benchmarking fixes goblint/analyzer#1124).AddressSet.meet
: Convert offsets to intdomain values to check overlap goblint/analyzer#967, Unsound address set equality with mismatching offsets goblint/analyzer#564, Make address semantic equality more precise for 0-index goblint/analyzer#1032, Address domain bucket conflict with first field offset goblint/analyzer#998, Remove unnecessary lval domain special cases goblint/analyzer#1031).varEq
analysis goblint/analyzer#984, Escaped variables are not communicated between threads goblint/analyzer#1074, ThreadEscape: Collect set of escaping threads flow-insensitively goblint/analyzer#1078).compinfo
keys not updated incrementally goblint/analyzer#678, Incremental: Reset ckeys for anonymous structs and unions goblint/analyzer#942, Reluctant incremental analysis does not reach fixpoint and is unsound in some cases goblint/analyzer#949, Fix Unreached Fixpoint in Reluctant Incremental Analysis goblint/analyzer#950, Fix: not found global should be added not removed goblint/analyzer#957, Incremental goblint crashes withGoblint_lib.Lattice.BotValue
on some commits of chrony and zstd goblint/analyzer#955, Fixpoint not reached in incremental analysis on some commits of chrony goblint/analyzer#954, Only pass stablereluctant_vs
to postsolver goblint/analyzer#960, Reluctant incremental Goblint does not reach fixpoint on some commits of chrony goblint/analyzer#959, Fix incremental write-only restarting for side effects from deleted nodes goblint/analyzer#1004, Allow incremental octagon Apron analysis goblint/analyzer#558, Clear TD3sides
when not reusingwpoint
incrementally goblint/analyzer#1010, Fixpoint not reached in some incremental runs on chrony goblint/analyzer#1091).cfg/lookup
request goblint/analyzer#997, Handle pseudo return nodes inNode.of_id
and improve their location goblint/analyzer#1000, Addarg/lookup
request to server mode goblint/analyzer#1001, Addglobal-state
request to server mode goblint/analyzer#1013,arg/eval
andarg/eval-int
give wrong results for globals after reanalysis goblint/analyzer#1018, Fix incremental invariant parser for server mode goblint/analyzer#1017, Recursive functions causearg/lookup
to return edges that point to nodes that don't exist goblint/analyzer#1026, Exclude pruned witness lifter prevs from ARG construction goblint/analyzer#1027).lib.activated
goblint/analyzer#1028, Convert library functions to new specifications goblint/analyzer#1079, Incorrectmemmove
library function specification goblint/analyzer#1121, Add support forquick_exit
goblint/analyzer#1135, Library functions that are used inthe silver searcher
including some from thepcre
library goblint/analyzer#1138).