9839 Commits (df4ce1995436c4f3777baad83aba088967d5ddd4)
 

Author SHA1 Message Date
Josh Berdine 9e373fb68c [sledge] Generalize Context.Subst.compose to support shadowed bindings
4 years ago
Josh Berdine 5f8989fc39 [sledge] Revise quantifier elimination of disjunctive formulas
4 years ago
Josh Berdine 8f40a85cd8 [sledge] Refactor QE in Sh.simplify to simplify Context interface
4 years ago
Josh Berdine d574b14dc7 [sledge] Improve Sh.simplify using stronger Context.elim
4 years ago
Josh Berdine 1c37a0f146 [sledge] Generalize Context.elim and make it more robust
4 years ago
Josh Berdine 7f835bf80a [sledge] Fix Context.fold_uses_of
4 years ago
Josh Berdine ee177a980d [sledge] Fix type of Context.fold_uses_of
4 years ago
Josh Berdine d72d83bfb4 [sledge] Freshen nested existentials also wrt ancestor universals
4 years ago
Josh Berdine e9fd3b603d [sledge] Add fast path to Sh.simplify for unsat formulas
4 years ago
Josh Berdine d8d8f947d7 [sledge] Delay unsat check in exec_assume until after simplify
4 years ago
Josh Berdine df37767a93 [sledge] Detect unsat symbolic heaps earlier during simplification
4 years ago
Josh Berdine 69a979612b [sledge] Use unsat context and ff pure constraints in unsat symbolic heaps
4 years ago
Josh Berdine c065e6f384 [sledge] Additional tracing
4 years ago
Josh Berdine a18165c553 [sledge] Improve tracing
4 years ago
Josh Berdine 0879afe950 [sledge] Remove dead Domain.is_false
4 years ago
Josh Berdine edb60837b3 [sledge] Rename Sh.is_false to is_unsat
4 years ago
Josh Berdine a7b547ccdf [sledge] Fix Context.apply_subst to preserve rest of representation
4 years ago
Josh Berdine e0312f1274 [sledge] Add fast path for applying an empty substitution
4 years ago
Loc Le 12c582a698 [pulse] explicit isl error specs for free/delete
4 years ago
Daiva Naudziuniene 16718384b3 [pulse] Optional Empty Access false positives we want to address
4 years ago
Loc Le 92341d8ffc isl summary for memory store
4 years ago
Kevin Higgs afc9666e15 Fix SIL to HIL conversion for Exp.Var inside Lfield and Lindex (#1372)
4 years ago
Luka Rahne 66d0eaa357 Fix #1366; apply xml escaping on generated xml report (#1367)
4 years ago
Gabriela Cunha Sampaio e065b0b0b2 Change Pulse Checker from experimental for C++ and Java to experimental for Java only
4 years ago
Jules Villard 2ac2f019df [clang] fix some loops with no brackets
4 years ago
Jules Villard ad45bbe28d [clang] fix order of translation for [this]
4 years ago
Loc Le 6eb79feaaf [Pulse] explicit Ok/Error summaries: bi-abduction for memory read
4 years ago
Sungkeun Cho 1166c13cb1 [log] Add a missing line space
4 years ago
dependabot[bot] 9f98368e49 Bump ini from 1.3.5 to 1.3.8 in /website (#1359)
4 years ago
Franco Raimondi 366ca37ff9 apache commons lang3 string utils model (#1346)
4 years ago
Sora Morimoto c5a0593be3 Update website stuff (#1311)
4 years ago
Petr Plavjanik f22edd95c7 Fix link to Infer workflow from Hello, World! (#1347)
4 years ago
Jules Villard 60119943a6 [nullsafe] do not crash when java_class_info is empty
4 years ago
Daiva Naudziuniene 47954fc428 [pulse] Do not drop astates in ExitScope instruction
4 years ago
Daiva Naudziuniene 0c6eedc835 [pulse] Model std::__optional_storage_base::has_value
4 years ago
Sungkeun Cho b4b75c4ffb [config] Use not-reversed list types for `Config` variables
4 years ago
Sungkeun Cho 153005c3cb [config] Add RevList for explicit reversed list in Config
4 years ago
Artem Pianykh edc8754727 [nullsafe] Fix behaviour of --no-nullsafe-optimistic-third-party-in-default-mode
4 years ago
Nikos Gorogiannis f779ed8951 [memtrace] allow memory tracing of analysis workers
4 years ago
Nikos Gorogiannis ea321b42a2 [buck] fix no-inline arguments order when doing a query
4 years ago
Martin Trojer 212068f89b Make buck tests more robust
4 years ago
Martin Trojer 4487513a2f [ndkbuild] only make ndkbuild test build for x86
4 years ago
Martin Trojer 1a04fc8f53 Make buck_flavors_deterministic_test more robust
4 years ago
Artem Pianykh 9d2daee569 [nullsafe] Fix checkState model
4 years ago
Loc Le b1d371e54d Pulse with explicit Ok/Error summaries
4 years ago
Ezgi Çiçek d02f0b322e [cost] Record zero operation cost for procedures that simply throw
4 years ago
Nikos Gorogiannis 72a59553d2 [buck] store query args in argument file
4 years ago
Ezgi Çiçek 731b632632 [cost] Procedures with empty body gets 0 cost
4 years ago
Loc Le 9228899f38 ISL tests
4 years ago
Jules Villard b5bd85c967 [pulse] quantifier elimination using var_eqs
4 years ago