Commit Graph

117 Commits

Author SHA1 Message Date
Daniel Marjamäki 446256a503 Verification; assume non-const pointer argument might point at uninitialized data 2019-12-31 17:51:58 +01:00
Daniel Marjamäki 10010eba95 Verification; Avoid fp for array declaration 2019-12-31 16:50:20 +01:00
Daniel Marjamäki f55d72e821 Verification; uninitialized local variable 2019-12-31 14:57:42 +01:00
Daniel Marjamäki 48be067dd1 Verification; Added --verify-diff option 2019-12-31 12:05:08 +01:00
Daniel Marjamäki 3af3219076 Verification; Juliet *_float_* division by zero tests 2019-12-31 09:02:06 +01:00
Daniel Marjamäki fde86b696d Verification; Use ValueFlow for improved accuracy 2019-12-31 05:59:06 +01:00
Daniel Marjamäki 3ff31b799c Verification: Use separate id for floating point division by zero 2019-12-30 19:50:22 +01:00
Daniel Marjamäki 4b5585e75b Verification; floating point division by zero 2019-12-30 19:47:18 +01:00
Daniel Marjamäki a60efa6774 Verification; Experimental checking for uninit 2019-12-30 18:55:16 +01:00
Daniel Marjamäki 6ea1875a84 Verification; Ensure assertions for variable type limits are added 2019-12-30 12:53:59 +01:00
Daniel Marjamäki 29b599b0e5 Verification; callbacks in executeCast 2019-12-29 19:17:36 +01:00
Daniel Marjamäki 9723b28385 Verification; struct pointer member 2019-12-29 18:42:35 +01:00
Daniel Marjamäki 2710a94b4b Verification; Merged handling of pointers and arrays 2019-12-29 16:26:11 +01:00
Daniel Marjamäki d16ea3293e Verification; Fix testing 2019-12-28 22:09:16 +01:00
Daniel Marjamäki ab2e87191f Verification; Avoid crash 2019-12-27 20:27:21 +01:00
Daniel Marjamäki 49ed1a82b4 Verification; save report in custom file 2019-12-27 19:25:06 +01:00
Daniel Marjamäki 4b4f7ea60b Verification; Updated report 2019-12-27 19:05:22 +01:00
Dmitry-Me 147cf9319f Restore compilation in gcc-4.6 2019-12-27 18:26:44 +03:00
Daniel Marjamäki ec4668353d Verification; Determine argument number properly 2019-12-26 18:32:59 +01:00
Daniel Marjamäki 8c652afd6e Verification: Added IntRange::isLessThan and IntRange::isGreaterThan 2019-12-26 15:39:08 +01:00
Daniel Marjamäki 0cd2935dc7 Verification; Verify that function call argument values meet annotations 2019-12-25 09:23:07 +01:00
Daniel Marjamäki f0ac19514b Verification: Handle Cppcheck annotations __cppcheck_low__ and __cppcheck_high__ 2019-12-24 21:14:14 +01:00
Daniel Marjamäki 755e2d261c Fixed #9402 (ExprEngine: && and || in condition) 2019-12-24 15:52:02 +01:00
Daniel Marjamäki 747a01f74d Verification; Check function argument values 2019-12-23 22:10:43 +01:00
Daniel Marjamäki eb551728a5 Verification; Avoid FP for known values 2019-12-22 21:24:39 +01:00
Daniel Marjamäki 93f10da981 Verification; Detect errors after bailout 2019-12-22 21:03:43 +01:00
Daniel Marjamäki c3c9559bee Fix Cppcheck warning 2019-10-27 18:22:47 +01:00
Daniel Marjamäki c899d7becf --verify: Fix false negative in itc 2019-10-27 16:47:56 +01:00
Daniel Marjamäki 83a7987f6f --verify: Fix false negative in itc test suite 2019-10-27 16:23:37 +01:00
Daniel Marjamäki c56a45840a Verify: Fix false negative in itc 2019-10-27 15:35:04 +01:00
Daniel Marjamäki 37bb19f02c Verify: Fix a false negative in the itc test suite 2019-10-25 21:46:02 +02:00
Daniel Marjamäki 8cfc833381 ExprEngine: Better handling of container arguments 2019-10-23 22:04:48 +02:00
Daniel Marjamäki 052c02f8ee ExprEngine: Refactoring 2019-10-23 18:42:40 +02:00
Daniel Marjamäki bcfc0d32fe ExprEngine: :: 2019-10-23 18:23:25 +02:00
Daniel Marjamäki 7b50b76b89 ExprEngine: container value 2019-10-23 18:06:10 +02:00
Daniel Marjamäki 4d218d1b47 ExprEngine: Clarify output 2019-10-23 16:40:49 +02:00
Daniel Marjamäki 3699227b12 ExprEngine: Throw exception if there is unhandled expression in assignment LHS 2019-10-22 18:39:59 +02:00
Daniel Marjamäki d98ac017f7 ExprEngine: Improved handling of struct member assignments in loops 2019-10-14 22:04:12 +02:00
Daniel Marjamäki 8c5c070d6a ExprEngine: Improved handling of struct member assignments in loop 2019-10-14 19:41:32 +02:00
Daniel Marjamäki ee280a94fb ExprEngine: New handling of << and >> 2019-10-14 17:20:35 +02:00
Daniel Marjamäki 4e49b14721 ExprEngine: << and >> are not handled well, throw exception for now. 2019-10-14 11:56:39 +02:00
Daniel Marjamäki c7a56529bb ExprEngine: Clarify verificationIntegerOverflow message 2019-10-14 11:54:43 +02:00
Daniel Marjamäki 530d4d2427 ExprEngine: Throw exception if we do not handle array well yet 2019-10-10 20:29:43 +02:00
Daniel Marjamäki c2b514dc45 ExprEngine: Throw exception if assignment in loop is not handled 2019-10-10 11:12:36 +02:00
Daniel Marjamäki 5b9bc4918e ExprEngine: Better error output when solver fails 2019-10-09 22:16:30 +02:00
Daniel Marjamäki 63bd182e83 ExprEngine: Adapt to z3 handling of bool/int expressions 2019-10-09 20:18:17 +02:00
Daniel Marjamäki 273a1a7402 ExprEngine: Fix FP for 'int' overflows 2019-10-09 11:24:57 +02:00
Daniel Marjamäki ab6354754f ExprEngine: Catch z3::exception and print message 2019-10-09 09:42:18 +02:00
Daniel Marjamäki b27fe83da4 ExprEngine: Handle << and >> 2019-10-08 21:38:10 +02:00
Daniel Marjamäki 3e50150dbf ExprEngine: Fix the checking for integer overflows 2019-10-08 20:13:25 +02:00