8920 Commits (7f9afea4110c83e46c4f391e344f76f722f6cd1a)
 

Author SHA1 Message Date
Josh Berdine d7cd987780 [sledge] Build: Do not clean help file
4 years ago
Josh Berdine 5f82adbf37 [sledge] Improve: Replace naive implementation of Fol.equal_or_opposite
4 years ago
Josh Berdine d8114b4688 [sledge] Improve: Normalize polarity of conditional formulas
4 years ago
Josh Berdine 74086e926a [sledge] Improve: Normalize order of symmetric binary formulas
4 years ago
Josh Berdine d87d8f7ef2 [sledge] Test: Update test infra
4 years ago
Josh Berdine 4c52102882 [sledge] Test: Add executable for manipulating reports
4 years ago
Josh Berdine 334661b474 [sledge] Improve: result status reporting and unhandled exceptions
4 years ago
Josh Berdine f160ac8a62 [sledge] Improve: Print locations with relative pathnames
4 years ago
Josh Berdine 2c16e15c92 [sledge] Add: __llair_choice intrinsic
4 years ago
Josh Berdine 6f435a74d7 [sledge] Add sledge llvm disassemble subcommand
4 years ago
Josh Berdine ca02dbd4aa [sledge][buck] Use same mode for buck root as buck build
4 years ago
Josh Berdine 7fd5dc49be [sledge] Add: SMT-LIB frontend to SLEdge's internal first-order theory solver
4 years ago
Josh Berdine f12ca72f07 [sledge] Fix: Replace Formula.disjuncts with DNF in Sh.pure
4 years ago
Josh Berdine 3e7aeed230 [sledge] Improve: Sh.fold_dnf to use iter vs list
4 years ago
Josh Berdine edda611c9c [sledge] Add: Iter library
4 years ago
Josh Berdine 60248165fd [sledge] Fix: Sh.pure
4 years ago
Josh Berdine 93c6dcc480 [sledge] Refactor: Replace Sh.with_pure with ~ignore_pure arg to Sh.fv
4 years ago
Josh Berdine 8ca41a9639 [sledge] Test: Move test modules into test directory
4 years ago
Josh Berdine 02ddb5a59f [sledge] Test: Move tests from Equality to Fol
4 years ago
Josh Berdine b0cd050d6f [sledge] Add: Replay debugging for more entry points
4 years ago
Josh Berdine 19cc35b65e [sledge] Add: Context.inter
4 years ago
Josh Berdine 53a1160bdb [sledge] Refactor: Reorder Context definitions
4 years ago
Josh Berdine ec7f02a585 [sledge] Add: Normalization of constant, equal and negated subterms/formulas
4 years ago
Josh Berdine 85b135dcbb [sledge] Build: Require dune >= 2.7
4 years ago
Ezgi Çiçek 9681317f57 [preanalysis] Add mli file and documentation for the preanalysis about specializing methods with blocks
4 years ago
Nikos Gorogiannis db9828809e [sourcefiles] use custom serializer
4 years ago
Nikos Gorogiannis a2c1aa79c8 [procname] preserve sharing when serialising
4 years ago
Nikos Gorogiannis 1db53f43b5 [biabduction][models] move to sqlite
4 years ago
Nikos Gorogiannis cb2243741c [sqlite] remove proc_name_hum field
4 years ago
Nikos Gorogiannis e9a6195b52 [sqlite] index on proc_uid
4 years ago
Nikos Gorogiannis 343d6b1bea [preanal] do not rewrite capture db
4 years ago
Sungkeun Cho 65dd303415 [cost] Add new experimental cost kind
4 years ago
Ezgi Çiçek dab523f7eb [cost] Remove unused IO Cost kind
4 years ago
Qianyi Shu c3909c0434 [cost] add iterator model for NSOrderedSet
4 years ago
Qianyi Shu 5ed04a8e9a [frontend] Add translation of dictionaryWithObjects:forKeys:count:
4 years ago
Daiva Naudziuniene 20a8890fd5 [frontend] Clean up method creation
4 years ago
Sungkeun Cho 44ff6df1d6 [frontend] Add autoreleasepool code block
4 years ago
Josh Berdine cf322a4e84 [sledge] Style: fix make fmt
4 years ago
Qianyi Shu d908accd0c [cost] add inferbo model for NSArray.arrayByAddingObjectsFromArray, NSMutableArray.initWithCapacity
4 years ago
Daiva Naudziuniene 4401701578 [pulse] Model for std::function copy constructor
4 years ago
Ezgi Çiçek 2b1e036a15 [inferbo] Add model for NSDictionary.dictionary
4 years ago
Nikos Gorogiannis 1d908ff327 [sqlite] localise statements to where they are used
4 years ago
Ezgi Çiçek 06489dced0 [cost] Add FP test for NSDictionary initialization
4 years ago
Ezgi Çiçek 7cb8145ef6 [litho] Fix FN caused by special treatment of ResType suffixes
4 years ago
Dulma Churchill fdb1640e12 [closures preanalysis] [3/n] Adding models to dispatch functions and remove code for previous specialization and dispatch models
4 years ago
Dulma Churchill 2e66bf6b8f [closures preanalysis][2/n] Add second preanalysis that fills the body of the specialized methods with blocks
4 years ago
Dulma Churchill 892b16b8c0 [closures preanalysis] [1/n] Adding first step of preanalysis to specialize methods with concrete closures they are called with
4 years ago
Daiva Naudziuniene 0a4af7754d [pulse] Fix std::function::operator()
4 years ago
Qianyi Shu bb828a92af [cost] refactor cost model and add NSArray.sort cost model.
4 years ago
Qianyi Shu b71521a90a [cost] add iterator support for nsdictionary
4 years ago