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 |