Commit Graph

46 Commits

Author SHA1 Message Date
Daniel Marjamäki 542158d0f4 Bug hunting; checking uninitialized struct member 2020-06-18 13:49:11 +02:00
Daniel Marjamäki 4947a3b7ab Bug hunting; review and improve handling of multi dimensional arrays 2020-06-16 22:50:45 +02:00
Daniel Marjamäki f482eb49cd ExprEngine; Fixed bug. Constraint expressions must be boolean 2020-05-27 19:37:07 +02:00
Philipp Kloke 32923b7ac5 Refactorization: Fixed a couple of compiler warnings about reusing variable names 2020-05-19 08:35:12 +02:00
Daniel Marjamäki 08ddd84780 Update copyright year 2020-05-10 11:16:32 +02:00
Daniel Marjamäki 3e0218299b Revert "Update copyright year"
This reverts commit 6eec6c4bd5.
2020-05-10 11:13:05 +02:00
Daniel Marjamäki 6eec6c4bd5 Update copyright year 2020-05-10 11:11:34 +02:00
Daniel Marjamäki dab8b9fd31 ExprEngine: Improved checking of contracts in function calls 2020-04-28 17:16:13 +02:00
Daniel Marjamäki f7096a2232 Bug hunting: basic handling of contracts through GUI 2020-04-27 09:08:50 +02:00
Oliver Stöneberg 2c1e36e63e
cleaned up includes based on include-what-you-use (#2600)
* cleaned up includes based on include-what-you-use

* check.h: trying to work around Visual Studio 2012 bug

* fixed Visual Studio compilation
2020-04-13 13:44:48 +02:00
Daniel Marjamäki 0e75f16510 verificationUninit: ignore bailout values until it's less noisy 2020-01-12 14:52:15 +01:00
Daniel Marjamäki 55ea06354b ExprEngine: BailoutValue is uninitialized 2020-01-12 10:42:20 +01:00
Daniel Marjamäki 75fd4809e6 Fix compiler warning 2020-01-10 15:08:53 +01:00
Daniel Marjamäki 35a8cd8418 Verification; fix division by zero false negative when value might be uninitialized 2020-01-09 19:40:15 +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 d247ffb13a Fix compiler warning 2019-12-29 21:22:20 +01:00
Daniel Marjamäki 2710a94b4b Verification; Merged handling of pointers and arrays 2019-12-29 16:26:11 +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 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 93f10da981 Verification; Detect errors after bailout 2019-12-22 21:03:43 +01:00
cyy cf5dd48994 add override (#2305) 2019-10-29 20:06:40 +01:00
Daniel Marjamäki 2fa9a29ea7 --verify: Fix false negative in itc test suite 2019-10-27 16:40:16 +01:00
Sebastian b7e48a9b27
Fix #9399 (Build Failure on x86: error: unknown type name '__int128_t') (#2254)
https://stackoverflow.com/questions/16088282/is-there-a-128-bit-integer-in-gcc
suggests to test for __SIZEOF_INT128__. This test is added now and
Cppcheck now also compiles for a 32 bit target with the expected
warning that there is no 128-bit integer. "make test" also works.
2019-10-09 10:25:21 +02:00
Daniel Marjamäki 3e50150dbf ExprEngine: Fix the checking for integer overflows 2019-10-08 20:13:25 +02:00
Daniel Marjamäki e686699294 ExprEngine: Fix ExprEngin::IntRange::isIntValueInRange 2019-10-05 16:33:40 +02:00
Daniel Marjamäki d916379f9f ExprEngine: Better handling of if/else 2019-10-02 21:47:00 +02:00
Daniel Marjamäki 7ab22c7176 ExprEngine: Use smt solver Z3 2019-10-02 17:59:04 +02:00
Daniel Marjamäki 40c3e68e07 ExprEngine: Add --debug-verify, fixed handling of global arrays 2019-09-29 15:00:54 +02:00
Daniel Marjamäki 69016e38bc ExprEngine: Add a temporary overflow check 2019-09-27 14:20:17 +02:00
Daniel Marjamäki 2e1cbbeb14 ExprEngine: Fix output for StructValue 2019-09-26 19:39:30 +02:00
Daniel Marjamäki c5302d20a3 ExprEngine: ConditionalValues, output symbolic expressions 2019-09-26 10:03:58 +02:00
Daniel Marjamäki 9e76630a4b ExprEngine: Restructure handling of arrays to handle dynamic buffers better 2019-09-25 18:33:21 +02:00
Daniel Marjamäki 0011fb5a36 ExprEngine: Temporary hardcoding for calloc 2019-09-24 22:22:16 +02:00
Daniel Marjamäki c1ff3419a6 ExprEngine: Value truncation 2019-09-23 20:28:12 +02:00
Daniel Marjamäki 28d13e7567 ExprEngine: Implement basic float handling 2019-09-22 21:14:36 +02:00
Daniel Marjamäki ec4b7c1f4b ExprEngine: Better handling of pointers 2019-09-22 10:56:57 +02:00
Daniel Marjamäki b2cab003ff ExprEngine: Fix output for arrays 2019-09-21 14:17:16 +02:00
Daniel Marjamäki 3d0d3ec4c5 ExprEngine: handling array initialization with string literal 2019-09-21 11:36:34 +02:00
Oliver Stöneberg b5c598cca4 added missing OVERRIDE usage and removed redundant virtual (#2190) 2019-09-20 21:57:16 +02:00
Sebastian bf55e835aa
Windows testrunner: Add testexprengine.cpp (#2184)
Add export of executeAllFunctions() in exprengine.h
2019-09-19 19:40:00 +02:00
amai2012 5a6084fbec Map #warning to #pragma message for VisualStudio 2019-09-18 21:50:23 +02:00
Daniel Marjamäki b66d701599 Fix Cppcheck warnings 2019-09-17 22:28:36 +02:00
Daniel Marjamäki 2d651b09fc ExprEngine: Add new experimental path-sensitive data flow analysis. Initially used for 'verification' but could possibly later be used as a complement in the normal analysis. The code is work-in-progress and hacky! 2019-09-17 21:00:59 +02:00