53 Commits

Author SHA1 Message Date
Daniel Marjamäki
b052843655 exprengine: Use and tweak ExprEngine::ArrayValue::MAXSIZE 2020-10-04 11:21:13 +02:00
Daniel Marjamäki
36b9e545ac Bug hunting; more bailout warnings in uninit check 2020-07-13 20:23:44 +02:00
Daniel Marjamäki
d4bd3016da ExprEngine; Improved handling of for loop, loop variable 2020-06-28 17:28:40 +02:00
Daniel Marjamäki
bcaf792e30 Bug hunting; Fix FP for struct with uninitialized members passed to function in C 2020-06-27 22:11:12 +02:00
Daniel Marjamäki
d353a4ecba ExprEngine; copy Data => copy arrays 2020-06-27 18:09:43 +02:00
Daniel Marjamäki
c62e345340 Fix Cppcheck warning 2020-06-19 14:11:49 +02:00
Daniel Marjamäki
cbe038e694 ExprEngine: execute functions in same TU 2020-06-19 10:27:59 +02:00
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 6eec6c4bd53d42e3a1179fd3a8a7dae5a43d4d50.
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