125 Commits (9670d3c7003e429820f44df73936c6a5973e0b07)

Author SHA1 Message Date
Sungkeun Cho 8dd45eebde [inferbo] Use record environment type for model
7 years ago
Sungkeun Cho ebddb14206 [inferbo] Prune by assert
7 years ago
Mehdi Bouaziz 4fdaf257ae [inferbo/unreachable] Fix FPs with exit at end of block/procedure
7 years ago
Mehdi Bouaziz dbaf9e459d [Inferbo] Do not use deprecated API to log issues
7 years ago
Josh Berdine 63439ecc02 [ocamlformat] Upgrade base and ocamlformat
7 years ago
Sam Blackshear ab3da5b1d1 [cleanup] remove unused dynamic dispatch modes
7 years ago
Mehdi Bouaziz 3fc41af811 [inferbo] Model for folly::split
7 years ago
Jeremy Dubreil 1f6d73269e [infer] simplify the API to report errors
7 years ago
Mehdi Bouaziz 0ed1a51944 [inferbo] Prepare for type models
7 years ago
Jeremy Dubreil 7b8a5a1a2b [infer] always run all the pre-analysis passes independently form the checkers that are being run
7 years ago
Mehdi Bouaziz cd35b2f0a3 [inferbo] Moving Inferbo utils functions
7 years ago
Mehdi Bouaziz 168ce5a6bb [inferbo] Add alloc size safety condition
7 years ago
Mehdi Bouaziz d12371c6c3 [inferbo] Prepare for several kinds of safety conditions
7 years ago
Mehdi Bouaziz cb363d8dcb [inferbo] Modeled functions may also generate proof obligations
7 years ago
Mehdi Bouaziz a73162d8e4 [dispatcher] + Capture function argument
7 years ago
Mehdi Bouaziz d26e227267 [c++] Procname dispatcher
7 years ago
Mehdi Bouaziz 55ff444a74 [inferbo] Sem.eval do not need a location
7 years ago
Josh Berdine f62ab09e61 [ocamlformat] Upgrade ocamlformat to v0.2 from opam
7 years ago
Mehdi Bouaziz 15ffac4e02 [inferbo] Move models to their own module
7 years ago
Mehdi Bouaziz eb33fb7a97 [inferbo] Use a dispatcher for models
7 years ago
Sungkeun Cho 042dd7d9cb [inferbo] revise semantics of vector::data
7 years ago
Josh Berdine f89e687efa [ocamlformat] Use ocamlformat from github
7 years ago
Sungkeun Cho 54de59919e [inferbo] Prune vector's size by vector::empty() condition check
7 years ago
Mehdi Bouaziz eff7bb5bdf [inferbo] Replace buckets with issue types
7 years ago
Mehdi Bouaziz d5c08ee752 [inferbo] Move proof obligations to their own module and split them
7 years ago
Mehdi Bouaziz 26f847f381 [inferbo] Conditions should not have bottom intervals
7 years ago
Mehdi Bouaziz 39ff045569 [ai] No need to create a domain for a bottom_lifted type
7 years ago
Mehdi Bouaziz cfd6148dab [inferbo] Better pp
7 years ago
Sungkeun Cho 9f9dbdb914 [Inferbo] Extend abstract domain for vector::empty
7 years ago
Sam Blackshear fd105802db [thread-safety] don't use Map.choose or Set.choose
7 years ago
Jules Villard 1c375a17ac [log] die more appropriately
7 years ago
Greg Nisbet 7fc5cb7930 exinferbo] check end of procedure for unreachability
7 years ago
Jules Villard 69299ba675 [filtering] improve issue type filtering CLI
7 years ago
Mehdi Bouaziz 5ea80fdb82 [inferbo] Remove temporary logical variables
7 years ago
Sungkeun Cho 1531a3d538 [inferbo] Pruning return value of function call
8 years ago
Josh Berdine bab3d81cb0 Convert Reason to OCaml, and auto-format OCaml
8 years ago
Jules Villard 7e2b5dd161 [inferbo] printing every state of symbolic execution is verbose
8 years ago
Kihong Heo 94d6efb83a [Inferbo] Add traces for buffer overrun bug report
8 years ago
Kihong Heo 7176fc936a [inferbo] fix the semantics of unknown library calls
8 years ago
Mehdi Bouaziz 63fcddb4a7 [inferbo] Do not store dummy idents into stack
8 years ago
Sungkeun Cho 00390d367a [inferbo] Refactor new symbol generation
8 years ago
Sungkeun Cho f45f4cb4c0 [Bufferoverrun] symbolic value for parameter
8 years ago
Sungkeun Cho 52c0caafaf [inferbo] Declare unsigned typed parameters
8 years ago
Sam Blackshear 1f153d3e3f [absint] kill `AbstractInterpreter.Interprocedural` module
8 years ago
Sam Blackshear 2a3032d0e3 [absint] rename confusing compute_and_store_post function
8 years ago
Kihong Heo 8567afdf55 [inferbo] add instantiation for parameters (call-by-ptr/ref)
8 years ago
Jeremy Dubreil cddd1b4ca2 [infer][ondemand] rename the logging functions to outline the deprecated ones
8 years ago
Jules Villard 93cc3266e8 [log] log to a single file with different categories and debug levels
8 years ago
Mehdi Bouaziz ec7b096ff6 [inferbo] Add warnings and errors for unreachable code
8 years ago
Mehdi Bouaziz 8dd041c5af [inferbo] Moving stuff
8 years ago
Mehdi Bouaziz 5d9291b911 [inferbo] Some more debug
8 years ago
Mehdi Bouaziz f521e5fbc0 [inferbo] Models for exit, fgetc
8 years ago
Mehdi Bouaziz 1486b92084 [inferbo] Renamed a few Itv values
8 years ago
Jules Villard 741e527826 [console] print progress-like messages on stderr
8 years ago
Jules Villard 252c78bb0e [clang] initialize dynamically-size stack-allocated arrays
8 years ago
Kihong Heo 984a81413a [inferbo] Top for unanalyzed variables (e.g., global variables)
8 years ago
Jules Villard 93ec47a5f4 [IR] add stride to array type
8 years ago
Jules Villard 1b0ee6fbc3 [clang] add sizeof static value to translation
8 years ago
Mehdi Bouaziz eb477b771e [inferbo] Replace some Bottom by Top
8 years ago
Mehdi Bouaziz 2dbde13335 [inferbo] Use Logging for logging
8 years ago
Mehdi Bouaziz 7d70310691 [inferbo] Yack manucuring
8 years ago
Andrzej Kotulski 029499cd9d [IR] add type qualifiers to Typ.t
8 years ago
Sungkeun Cho 7212890846 [Bufferoverrun] More prune to make some nodes unreachable
8 years ago
Sungkeun Cho b4b32f8d3e [Bufferoverrun] set uninitialized values in array as top
8 years ago
Jeremy Dubreil f5adab59ec [infer][checkers] Prevent the race conditions between the summaries passed as parameter to the checkers and the summaries from the specs table
8 years ago
Jeremy Dubreil 81c0877e20 [infer][ondemnad] remove the call to `Summary.write_summary` in BufferOverrun which is no longer necessary
8 years ago
Jeremy Dubreil 3e6ff023a7 [infer][ondemand] skeleton code to have every checker update their respective payload in the analysis summary
8 years ago
Martino Luca 5448a95ce7 [Infer][Localise] Group all issue types in one place, and provide their human-readable representation
8 years ago
Andrzej Kotulski e363958d34 [codemod] Move `Procname` into `Typ.Procname`
8 years ago
Josh Berdine 95725e4dd0 Refactor StructTyp to Typ.Struct
8 years ago
Cristiano Calcagno b1b5460529 Deprecate further IList functions
8 years ago
Cristiano Calcagno 731dead406 More IList deprecation: fold functions
8 years ago
Cristiano Calcagno 60916922c6 Deprecate more IList functions and use Core List instead
8 years ago
Sam Blackshear 4627bb6f48 [absint] simplify `AbstractInterpreter.Make` functor by hiding `Scheduler` parameter
8 years ago
Kihong Heo cef2f0e055 Inferbo
8 years ago