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 |
|
Daniel Marjamäki
|
1769af4a6c
|
ExprEngine: Passing variable address to function
|
2019-09-24 19:53:33 +02:00 |
|
Daniel Marjamäki
|
c1ff3419a6
|
ExprEngine: Value truncation
|
2019-09-23 20:28:12 +02:00 |
|
Daniel Marjamäki
|
9025b47f82
|
ExprEngine: some handling of NULL pointer
|
2019-09-23 18:10:06 +02:00 |
|
Daniel Marjamäki
|
28d13e7567
|
ExprEngine: Implement basic float handling
|
2019-09-22 21:14:36 +02:00 |
|
Daniel Marjamäki
|
6e17853ea9
|
ExprEngine: Guess function call return value
|
2019-09-22 16:40:48 +02:00 |
|
Daniel Marjamäki
|
5c07cfd2e8
|
ExprEngine: Better handling of pointer aliasing
|
2019-09-22 15:58:55 +02:00 |
|
Daniel Marjamäki
|
ec4b7c1f4b
|
ExprEngine: Better handling of pointers
|
2019-09-22 10:56:57 +02:00 |
|
Daniel Marjamäki
|
7d6fd915be
|
ExprEngine: Better handling of compound assignments
|
2019-09-21 21:15:51 +02:00 |
|
Daniel Marjamäki
|
da91c139d5
|
ExprEngine: Passing array to function, array data might be overwritten
|
2019-09-21 19:34:06 +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 |
|
Daniel Marjamäki
|
6c59957109
|
ExprEngine: Better handling of conditions
|
2019-09-20 21:27:51 +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 |