8659 Commits (0f7ecbe9fec89bee3fd86140fcfa778278d67d49)
 

Author SHA1 Message Date
Dulma Churchill d2f8028e77 [preanalysis] Adding a preanalysis to resolve local closures
4 years ago
Daiva Naudziuniene 1c5e47d91e [frontend] Record lambda's captured variables in `operator()` procdesc
4 years ago
Sungkeun Cho 831741c5eb [inferbo] Fix a bug in eval_arr
4 years ago
Qianyi Shu 8d648b9c5a [cost] add cost model for most common NSString functions
4 years ago
Ezgi Çiçek e6ed605d67 [cost] Fix unreachable node Top poisoning
4 years ago
Daiva Naudziuniene 50d659b750 Update type of procdesc and closure expression to contain information about capture variable mode
4 years ago
Sungkeun Cho 9b5820bf32 [CCBM] Add semantics of return
4 years ago
Sungkeun Cho 549bd43ef8 [cost] Print where cost become top
4 years ago
Dulma Churchill 795ceadb46 [clang] Remove protocols from the list of superclasses of ObjC classes
4 years ago
Sungkeun Cho 2e319e7a16 [CCBM] Extend the value domain to express multiple markers
4 years ago
Sungkeun Cho 9c33957d7e [CCBM] Rename MarkerSet/InvMarkerSet
4 years ago
Sungkeun Cho 8e264fd669 [CCBM] Add semantics of assigning marker to local variable
4 years ago
Sungkeun Cho 095b946a13 [CCBM] Support another QE check form
4 years ago
Nikos Gorogiannis 2821cf8fdd [buck-clang] revert 500c1b12c95cbf38d45c1eb4a51c47247cf076ec
4 years ago
Qianyi Shu dc502676ea [cost] add model for NSString.string_with_utf8_string_linear and NSString.length
4 years ago
Qianyi Shu 75e5e94f2c [cost] add inferbo model for NSNumber
4 years ago
Qianyi Shu 1c39d7768f [cost] add inferbo model for NSArray
4 years ago
Amar Paul bb5a349c26 [infer][PR] Update CI to build infer with c analyzers
4 years ago
Sora Morimoto 350b6d1b82 [infer][PR] Update website dependencies
4 years ago
Josh Berdine b741bcd490 [sledge] Refactor: Move diff_classes from Equality to Context
4 years ago
Josh Berdine e3cbb0f27d [sledge] Add: Uninterpreted function symbols and applications to Fol
4 years ago
Josh Berdine c122577c18 [sledge] Change: Generalize Fol functional array indices from int to term
4 years ago
Josh Berdine 48833cc63b [sledge] Refactor: Expose constructors for record Terms
4 years ago
Josh Berdine d39dd1fee2 [sledge] Add: Array hash and sexp functions
4 years ago
Josh Berdine 04f7336301 [sledge] Build: Disable warning 30
4 years ago
Josh Berdine 32206a282f [sledge] Build: Suppress compiler error message noise
4 years ago
Josh Berdine 049b62f097 [sledge] Change: Sh.compare to ignore first-order context
4 years ago
Josh Berdine 8725d5fe81 [sledge] Refactor: pretty-printing of classes out of Ses to Fol
4 years ago
Josh Berdine 58dae840d3 [sledge] Change: Improve build info slightly
4 years ago
Josh Berdine a366b388a9 [sledge] Style: Autoformat dune-project and dune-workspace files
4 years ago
Josh Berdine 7e77bad4d2 [sledge] Change: Implement Fol using a solver-independent intermediate type
4 years ago
Josh Berdine a6dabc7924 [sledge] Refactor: Separate out conversion from Llair to Fol
4 years ago
Josh Berdine 896e9602f8 [sledge] Refactor: Rename Formula.conditional to Formula.cond
4 years ago
Josh Berdine 94e8b07997 [sledge] Refactor: Rename Formula.true_ and false_ to tt and ff
4 years ago
Josh Berdine 8d2bb0ddcf [sledge] Refactor: Move Ses.Term.Var.Subst to Fol.Var.Subst
4 years ago
Josh Berdine 79a4db7771 [sledge] Refactor: Make Term and Equality independent of Var.Subst
4 years ago
Josh Berdine 9cb74ac9ac [sledge] Refactor: Move Equality replay debugging to Fol
4 years ago
Josh Berdine 0568f2ee2d [sledge] Refactor: Distinguish Fol term and formula types
4 years ago
Josh Berdine 0998ce011f [sledge] Refactor: Add `formula` alias for `term` type, and use appropriately
4 years ago
Josh Berdine 4308ca649f [sledge] Remove unnecessary hash functions
4 years ago
Josh Berdine 967185e02a [sledge] Refactor: Reduce Fol sig to needed interface
4 years ago
Josh Berdine 3d1fbf3840 [sledge] Refactor: Expand sig of Fol submodules
4 years ago
Josh Berdine 0aed6eeab6 [sledge] Refactor: Rename to use "first-order logical context" terminology
4 years ago
Josh Berdine a629486c9f [sledge] Refactor: Rename Fol.Equality to Fol.Context
4 years ago
Josh Berdine dd2e7b4782 [sledge] Refactor: Add Fol module to be used for external interface of solver
4 years ago
Josh Berdine eca73cf39b [sledge] Build: Move sledge equality solver to separate lib
4 years ago
Josh Berdine 33d59b8642 [sledge] Refactor: Add Option.Import including Monad_infix and Monad_syntax
4 years ago
Josh Berdine c7556364b7 [sledge] Change: Strengthen Term invariant that exponents are integers
4 years ago
Josh Berdine 6b44eaf2e6 [sledge] Style: set ocamlformat config break-struct = force
4 years ago
Ezgi Çiçek ebc9f58f6f [cost] Add back the UI thread message
4 years ago