417 Commits (bb625c6ca8a965eca79c32ed38e814acde13793b)

Author SHA1 Message Date
Mehdi Bouaziz 1b8927badd [inferbo/cost] Do not produce inferbo issues on Cost and Purity analysis
6 years ago
Sungkeun Cho ca463d17c1 [inferbo] Add strcpy model
6 years ago
Sungkeun Cho 6226722c22 [inferbo] Add a test of comparison operator as function
6 years ago
Sungkeun Cho 371dc2060f [inferbo] Add strndup model
6 years ago
Sungkeun Cho 7fda4f1cc2 [inferbo] Revise strncpy model
6 years ago
Sungkeun Cho 1bcdc6e761 [inferbo] Extend conditional proof obligation for inequalities
6 years ago
Sungkeun Cho 0d07a240ea [inferbo] Literal string on stack location
6 years ago
Sungkeun Cho 6e04a9469b [inferbo] Revise memcpy model
6 years ago
Sungkeun Cho 9bd1191669 [inferbo] Add fgets model
6 years ago
Sungkeun Cho 58cdefc118 [inferbo] Add strlen model
6 years ago
Sungkeun Cho 5aa26dc32e [inferbo] Add an allocsite type for literal strings
6 years ago
Sungkeun Cho db441ffc8a [inferbo] Prevent deduplication of issues when different conditions
6 years ago
Sungkeun Cho 98cd2e59da [inferbo] Add tests: values representing multiple values
6 years ago
Sungkeun Cho 10f4ad06ba [inferbo] Add traces on cast
6 years ago
Sungkeun Cho 6a8f389c35 [inferbo] Prune (p=null)
6 years ago
Mehdi Bouaziz 5616940ec0 [inferbo] Symbols for one value
6 years ago
Mehdi Bouaziz 5ce86a1501 [inferbo] Do not compare deref_kind
6 years ago
Mehdi Bouaziz 1827b42f68 [inferbo] Improve traces of binary operators when nothing changes
6 years ago
Mehdi Bouaziz de3c7bac45 [inferbo][easy] Shift right zero
6 years ago
Sungkeun Cho fc26f79b92 [inferbo] Weaken canonical path in on-demand value generation
6 years ago
Sungkeun Cho 6920532e12 [inferbo] Forget only updated locations from latest prune at Store
6 years ago
Sungkeun Cho 4ad5d38b69 [inferbo] Revise join of LatestPrune
6 years ago
Sungkeun Cho 2531c75cea [inferbo] Add literal string assignment
6 years ago
Mehdi Bouaziz fd8b4795b8 [inferbo] Symbolic length for no-size flexible arrays
6 years ago
Mehdi Bouaziz 5c4de212fb [inferbo] New test + more debug
6 years ago
Sungkeun Cho a8dbaf082d [inferbo] Weak update for array contents
6 years ago
Sungkeun Cho f9161b164f [inferbo] On-demand heap symbol using path
6 years ago
Sungkeun Cho 98d05044fb [inferbo] Visit every nodes at narrowing
6 years ago
Mehdi Bouaziz a689301c53 [inferbo] eval_locs
6 years ago
Ezgi Çiçek 6017c2ec54 [cost] Fix control variables to pick up global vars in prune instructions
6 years ago
Sungkeun Cho 4b2c65f2e2 Revert "[inferbo] Instantiate symbolic locations in function parameters"
6 years ago
Sungkeun Cho 760fabe825 [inferbo] Ignore __variable_initialization
6 years ago
Sungkeun Cho 2a94e907e2 [inferbo] Revise pp of Symb.partial
6 years ago
Sungkeun Cho 4e166f3375 [inferbo] Instantiate symbolic locations in function parameters
6 years ago
Jules Villard 1c668c4d41 [SIL][preanalysis] add call flag for functions treating first formal as return
6 years ago
Jules Villard 55586b581b [preanalysis] do not delay killing variables taken by reference
6 years ago
Sungkeun Cho 15b77ee8c8 [inferbo] Give semantics for unsigned int casting of minus one
6 years ago
Sungkeun Cho 5f925869b6 [infer] Translate more casts (unsigned int)
6 years ago
Sungkeun Cho 442fecc030 [inferbo] Fix performance of issue deduplication
6 years ago
Mehdi Bouaziz e505fd2dba [inferbo] Pointer comparison
6 years ago
Mehdi Bouaziz 5f60ffaa8f [inferbo] Trace refactoring
6 years ago
Sungkeun Cho edc090544a [inferbo] Improve pp of Inferbo in traceview
6 years ago
Mehdi Bouaziz d6423cf598 [inferbo] Preparing for trace rewrite
6 years ago
Martino Luca 664978d654 Revert D12819709 to patch OOM events
6 years ago
Sungkeun Cho b4683d965d [inferbo] Resize array on casting
6 years ago
Sungkeun Cho 1486a5f105 [infer] Translate casting expressions of integer pointers
6 years ago
Jules Villard 646aa30797 [cfg] print dotty *after* pre-analysis
6 years ago
Ezgi Çiçek 5fa89e2563 [purity] Disable clang
6 years ago
Mehdi Bouaziz 8fcbfcb741 [inferbo] Pretty-print more abstract locations
6 years ago
Sungkeun Cho e912bf2aa5 [inferbo] Prune more for "(x + e1) < e2" cases
6 years ago
Sungkeun Cho e190325b82 [inferbo] Distinguish collection add against array access in pp
6 years ago
Sungkeun Cho 0d2b0e1ab7 [inferbo] Fix check function for is_collection_add
6 years ago
Mehdi Bouaziz fac9932168 [inferbo] Add traces to Conditions always true/false and Unreachable code
6 years ago
Sungkeun Cho 1503f63c27 [inferbo] Fix evaluation of multi-dimensional arrays
6 years ago
Sungkeun Cho 07f8855185 [inferbo] Fix condition check of multi-dimensional array
6 years ago
Mehdi Bouaziz 0ba4c2c892 [cost] Pretty-printing exponents
6 years ago
Mehdi Bouaziz 5ed59b1655 [Inferbo/cost] Improve pretty-printing
6 years ago
Mehdi Bouaziz 42b16d45fa [inferbo] New tests
6 years ago
Martino Luca 0547878898 Update InferBO tests
6 years ago
Sungkeun Cho 1cbcbe6fb3 [inferbo] Improve division on constant
6 years ago
Sungkeun Cho 01a83e694b [inferbo] Improve semantics of binary and
6 years ago
Jules Villard 9aa5582caa [clang] leave markers of variable initialization for pulse
6 years ago
Sungkeun Cho 2401f6f6eb [inferbo] Give a widening threshold of zero
6 years ago
Sungkeun Cho 00081274cb [inferbo] Preciser pruning: (x != 0)
6 years ago
Sungkeun Cho b2189c1c17 [inferbo] Loosen similar bounds condition
6 years ago
Sungkeun Cho bf29bd9772 [inferbo] Fix xcompare of Itv
6 years ago
Sungkeun Cho fed56fd0d8 [inferbo] Revise deduplication
6 years ago
Sungkeun Cho 9e9deb93be [inferbo] Use set instead of list on get_symbols
6 years ago
Sungkeun Cho a2312462eb [inferbo] Use values of global constant variables in C
6 years ago
Sungkeun Cho 87dd2047ec [infer] Use big int in IntLit
6 years ago
Sungkeun Cho 120c8785eb [inferbo] Update pp of buffer overflow condition
6 years ago
Sungkeun Cho 423b732cb4 [inferbo] Fix condition of narrowing termination
6 years ago
Mehdi Bouaziz 10804588b2 New function pointer preanalysis without recursion
6 years ago
Sungkeun Cho a40a7984c7 [inferbo] Try division on minmax value conservatively
6 years ago
Sungkeun Cho 3f71cf327b [inferbo] Separate offset and index in condition
6 years ago
Mehdi Bouaziz 3ee96263a7 [inferbo] Simplify and improve Itv.prune_comp
6 years ago
Mehdi Bouaziz 2824056af5 [inferbo] Normalize intervals after substitution
6 years ago
Mehdi Bouaziz ecedb27d77 Add missing FB copyrights
6 years ago
Sungkeun Cho fd3f298156 [inferbo] Add narrowing
6 years ago
Mehdi Bouaziz 3dd97cc40f [inferbo] Use WTO abstract interpreter
6 years ago
Mehdi Bouaziz e72cd6c00f [inferbo] More precise min/max
6 years ago
Sungkeun Cho 38ab5fda4e [inferbo] Add some tests of imprecise pruning on unsigned int
6 years ago
Mehdi Bouaziz 592efbf5fa [inferbo] Refine <= for MinMax
6 years ago
Sungkeun Cho 3f969414fe [inferbo] Check integer overflow when really need
6 years ago
Sungkeun Cho 5d9f11c68e [inferbo] Do not raise integer overflow when multiplying 1
6 years ago
Sungkeun Cho cd1981a567 [inferbo] Change pp of BinaryOperationCondition
6 years ago
Mehdi Bouaziz 6d9943f2aa Uninit: fix test
6 years ago
Sungkeun Cho fb4086c6f6 [inferbo] Add integer overflow issue type
6 years ago
Mehdi Bouaziz 81f31068e2 [Uninit][9/13] Check rhs using prestate
6 years ago
Dino Distefano 3d07754275 Giving cost 1 to procedure with empty body
6 years ago
Mehdi Bouaziz c3f2fbc8c6 [inferbo] Do not alias values representing multiple values (Java, C partially)
6 years ago
Mehdi Bouaziz eca0b491d6 Weak Topological Order and Abstract Interpreter using it
6 years ago
Mehdi Bouaziz 5679105c15 [Uninit][7/13] Add new tests
6 years ago
Jules Villard 7615963bf4 [proc-cfg][2/5] fix duplicate symbols detection
6 years ago
Sungkeun Cho 96cbdb15c7 [inferbo] Use big_int in interval domain
6 years ago
Sungkeun Cho 86d1560984 [inferbo] Add tests of integer overflow and unsafe casting
6 years ago
Jules Villard a29e769b61 [kill -a][1/4] stop using `-a foo` in the infer repo
6 years ago
Thomas M. DuBuisson 75e4226ea3 [infer][PR] Fix getcwd model to allow NULL argument
6 years ago
Julian Sutherland 5cf66f6da8 InferBO strncpy model
6 years ago
Julian Sutherland a5d3203ce8 inferBO calloc model
6 years ago