Daniel Marjamäki
|
6ec15b6d7b
|
ExprEngine; Simple handling of increment/decrement
|
2020-06-19 17:35:35 +02:00 |
|
Daniel Marjamäki
|
d0ac583b97
|
Add 'bughuntingchecks'
|
2020-06-19 13:16:48 +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
|
6faad9cd90
|
Bug hunting; better handling when assigning multidimensional array in for loop
|
2020-06-15 22:42:45 +02:00 |
|
Daniel Marjamäki
|
f482eb49cd
|
ExprEngine; Fixed bug. Constraint expressions must be boolean
|
2020-05-27 19:37:07 +02:00 |
|
Daniel Marjamäki
|
871cf379d5
|
ExprData: Better handling of ternary operator
|
2020-05-15 21:34:52 +02:00 |
|
Daniel Marjamäki
|
76f4fae806
|
Bug hunting; Started to activate some itc tests for uninitialized variables
|
2020-05-15 20:58:33 +02:00 |
|
Daniel Marjamäki
|
4afaff059b
|
Fix replacement in TestExprEngine
|
2020-05-13 09:56:21 +02:00 |
|
Daniel Marjamäki
|
0c97625aa0
|
github actions: Fix TestExprEngine
|
2020-05-13 09:50:25 +02:00 |
|
Daniel Marjamäki
|
046f8eb6c6
|
ExprEngine: improved handling when lhs/rhs for && has unknown value
|
2020-05-10 22:50:23 +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
|
02d88cb191
|
Travis: Run TestExprEngine tests
|
2020-05-08 12:21:22 +02:00 |
|
Daniel Marjamäki
|
34572a40ab
|
Bug hunting: Fixed handling of switch 'case %char%'
|
2020-05-01 15:15:24 +02:00 |
|
Daniel Marjamäki
|
b97250e0fa
|
ExprEngine; Try to handle assignments better
|
2020-04-30 21:05:34 +02:00 |
|
Daniel Marjamäki
|
dab8b9fd31
|
ExprEngine: Improved checking of contracts in function calls
|
2020-04-28 17:16:13 +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 |
|
Oliver Stöneberg
|
1dd8d4afaf
|
fixes for Clang and clang-tidy 10 (#2588)
* clang_tidy.cmake: added clang-tidy-10 to program list
* fixed -Wrange-loop-construct Clang warnings
* fixed readability-qualified-auto clang-tidy warnings
* .clang-tidy: actually disable clang-analyzer-* warnings
* .clang-tidy: disabled some new warnings introduced with clang-tidy-10
|
2020-04-04 11:44:59 +02:00 |
|
Daniel Marjamäki
|
4235a29501
|
ExprEngine: Handle variable annotations better
|
2020-01-21 18:55:07 +01:00 |
|
Daniel Marjamäki
|
c79ec9e956
|
ExprEngine: sizeof()
|
2020-01-15 15:24:36 +01:00 |
|
Daniel Marjamäki
|
7820b5dbcc
|
Rename 'Verification' to 'Bug hunting'
|
2020-01-14 21:17:07 +01:00 |
|
Daniel Marjamäki
|
d4ec8075a4
|
Verification; Fix false positive in while loops
|
2019-12-31 22:32:16 +01:00 |
|
Daniel Marjamäki
|
043634be27
|
Verification; Better handling of assignment in while
|
2019-12-31 20:31:31 +01:00 |
|
Daniel Marjamäki
|
4b5585e75b
|
Verification; floating point division by zero
|
2019-12-30 19:47:18 +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
|
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
|
4b4f7ea60b
|
Verification; Updated report
|
2019-12-27 19:05:22 +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
|
8c5c070d6a
|
ExprEngine: Improved handling of struct member assignments in loop
|
2019-10-14 19:41:32 +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
|
21774cbdc4
|
ExprEngine: Handle while/for loops
|
2019-10-07 17:45:06 +02:00 |
|
Daniel Marjamäki
|
d82b1b29ce
|
ExprEngine: Initial handling of switch
|
2019-10-06 19:58:51 +02:00 |
|
Daniel Marjamäki
|
e686699294
|
ExprEngine: Fix ExprEngin::IntRange::isIntValueInRange
|
2019-10-05 16:33:40 +02:00 |
|
Daniel Marjamäki
|
7e850e3e4b
|
ExprEngine: test pointer
|
2019-10-03 21:08:42 +02:00 |
|
Daniel Marjamäki
|
f80d387374
|
ExprEngine: Arrays if-then-else
|
2019-10-03 20:16:06 +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
|
1ccc303602
|
ExprEngine: Simplify array value if possible, ensure each array data has a unique name
|
2019-09-29 21:20:57 +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
|
60e1cf8b8d
|
ExprEngine: Fix NULL pointer dereference tests
|
2019-09-29 08:26:09 +02:00 |
|
Daniel Marjamäki
|
0de3e76b2d
|
ExprEngine: Clarify when analysis is aborted
|
2019-09-28 10:59:28 +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
|
0471e74489
|
ExprEngine: Handle char literals
|
2019-09-24 20:11:07 +02:00 |