Daniel Marjamäki
|
ee280a94fb
|
ExprEngine: New handling of << and >>
|
2019-10-14 17:20:35 +02:00 |
|
Daniel Marjamäki
|
4e49b14721
|
ExprEngine: << and >> are not handled well, throw exception for now.
|
2019-10-14 11:56:39 +02:00 |
|
Daniel Marjamäki
|
c7a56529bb
|
ExprEngine: Clarify verificationIntegerOverflow message
|
2019-10-14 11:54:43 +02:00 |
|
Daniel Marjamäki
|
530d4d2427
|
ExprEngine: Throw exception if we do not handle array well yet
|
2019-10-10 20:29:43 +02:00 |
|
Daniel Marjamäki
|
c2b514dc45
|
ExprEngine: Throw exception if assignment in loop is not handled
|
2019-10-10 11:12:36 +02:00 |
|
Daniel Marjamäki
|
5b9bc4918e
|
ExprEngine: Better error output when solver fails
|
2019-10-09 22:16:30 +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
|
ab6354754f
|
ExprEngine: Catch z3::exception and print message
|
2019-10-09 09:42:18 +02:00 |
|
Daniel Marjamäki
|
b27fe83da4
|
ExprEngine: Handle << and >>
|
2019-10-08 21:38:10 +02:00 |
|
Daniel Marjamäki
|
3e50150dbf
|
ExprEngine: Fix the checking for integer overflows
|
2019-10-08 20:13:25 +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
|
05aae9569b
|
ExprEngine: Execute false execution path even if there is no else, upon Z3 exception assume that value is in range (safe option)
|
2019-10-06 18:26:40 +02:00 |
|
Daniel Marjamäki
|
6c0c9ba6d3
|
ExprEngine: Handle 'break' and 'while (0);'
|
2019-10-06 17:43:30 +02:00 |
|
Daniel Marjamäki
|
dcf8a7213f
|
ExprEngine: ExprData::getConstraintExpr
|
2019-10-06 14:47:50 +02:00 |
|
Daniel Marjamäki
|
4e525e52ec
|
ExprEngine: Avoid endless recursion for struct members that have struct type
|
2019-10-05 18:29:41 +02:00 |
|
Daniel Marjamäki
|
e686699294
|
ExprEngine: Fix ExprEngin::IntRange::isIntValueInRange
|
2019-10-05 16:33:40 +02:00 |
|
Daniel Marjamäki
|
fcccd5f42e
|
ExprEngine: Small tweaks
|
2019-10-04 17:58:18 +02:00 |
|
Daniel Marjamäki
|
f80d387374
|
ExprEngine: Arrays if-then-else
|
2019-10-03 20:16:06 +02:00 |
|
Daniel Marjamäki
|
555890fdfa
|
ExprEngine: Removed NullPointerDereference checker for now.
|
2019-10-03 19:24:14 +02:00 |
|
Daniel Marjamäki
|
b79283306f
|
ExprEngine: Rename Data::conditions => Data::constraints
|
2019-10-03 08:48:05 +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
|
03ff32993e
|
Fixed Cppcheck warning
|
2019-09-29 17:32:26 +02:00 |
|
Daniel Marjamäki
|
1979b64170
|
ExprEngine: Bailout when for|while|switch is seen
|
2019-09-29 17:28:12 +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
|
3f587bef65
|
ExprEngine: Add some CWE476 (Null pointer dereference) checks
|
2019-09-28 19:28:12 +02:00 |
|
Daniel Marjamäki
|
1acd78a038
|
ExprEngine: Translate uninitialized values to value ranges
|
2019-09-28 16:16:36 +02:00 |
|
Daniel Marjamäki
|
2e5d663ae9
|
ExprEngine: Handle void* -> int* casts better
|
2019-09-28 15:40:00 +02:00 |
|
Daniel Marjamäki
|
f6c0550c41
|
ExprEngine: Do not bailout if function type is not known if the result is not used anyway
|
2019-09-28 11:55:06 +02:00 |
|
Daniel Marjamäki
|
b2239f04ba
|
ExprEngine: Improve 'division by zero' warning
|
2019-09-28 11:03:20 +02:00 |
|
Daniel Marjamäki
|
0de3e76b2d
|
ExprEngine: Clarify when analysis is aborted
|
2019-09-28 10:59:28 +02:00 |
|
Daniel Marjamäki
|
a3cad7fa51
|
Fix Coverity warning CID 1405837; negative bit shift
|
2019-09-28 06:34:51 +02:00 |
|
Daniel Marjamäki
|
8b8701d078
|
ExprEngine: Cleanup output when variable declaration and initialization is separated
|
2019-09-27 21:03:47 +02:00 |
|
Daniel Marjamäki
|
398cfc1f5a
|
ExprEngine: Create array value in struct
|
2019-09-27 18:58:49 +02:00 |
|
Daniel Marjamäki
|
2b4fe66908
|
Try to make Travis happy
|
2019-09-27 16:13:43 +02:00 |
|
Daniel Marjamäki
|
f7a8075001
|
ExprEngine: Disable integerOverflow check
|
2019-09-27 15:07:56 +02:00 |
|
Daniel Marjamäki
|
7ea8b69235
|
ExprEngine: Robustness
|
2019-09-27 14:36:33 +02:00 |
|
Daniel Marjamäki
|
69016e38bc
|
ExprEngine: Add a temporary overflow check
|
2019-09-27 14:20:17 +02:00 |
|
Daniel Marjamäki
|
8ccbdfe725
|
ExprEngine: Better output
|
2019-09-27 13:30:09 +02:00 |
|
Daniel Marjamäki
|
71aa9a531a
|
ExprEngine: Create symbolic expression for string arguments
|
2019-09-27 13:12:16 +02:00 |
|
Daniel Marjamäki
|
350363616c
|
Fix Cppcheck naming convention
|
2019-09-27 08:17:46 +02:00 |
|
Daniel Marjamäki
|
dffae8f7d9
|
Try to make Travis happy
|
2019-09-26 21:43:29 +02:00 |
|
Daniel Marjamäki
|
371babc322
|
ExprEngine: Improved handling of structs
|
2019-09-26 21:35:29 +02:00 |
|
Daniel Marjamäki
|
f47aaed21e
|
ExprEngine: Improve output
|
2019-09-26 21:00:36 +02:00 |
|
Daniel Marjamäki
|
f1b42fe05c
|
ExprEngine: Extend output
|
2019-09-26 20:49:03 +02:00 |
|
Daniel Marjamäki
|
2e1cbbeb14
|
ExprEngine: Fix output for StructValue
|
2019-09-26 19:39:30 +02:00 |
|
Daniel Marjamäki
|
cd816f42eb
|
ExprEngine: fix code for float comparisons
|
2019-09-26 12:13:14 +02:00 |
|
Daniel Marjamäki
|
d7d22f51b7
|
ExprEngine: Minor output cleanup
|
2019-09-26 10:07:31 +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
|
7cf8327b31
|
ExprEngine: Sign extension in truncateValue
|
2019-09-24 20:31:12 +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
|
ba035074f0
|
ExprEngine: Extended value truncation
|
2019-09-24 13:28:14 +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
|
8fba2af267
|
Try to make Travis happy
|
2019-09-20 07:04:58 +02:00 |
|
Daniel Marjamäki
|
6c38b69e11
|
Rename dataIndex to mDataIndex according to our naming conventions
|
2019-09-20 06:12:35 +02:00 |
|
Daniel Marjamäki
|
5f0f8afc27
|
ExprEngine: Print some 'debug' output
|
2019-09-19 20:18:55 +02:00 |
|
Daniel Marjamäki
|
745c91106e
|
Removed unused Data::dump
|
2019-09-19 09:16:18 +02:00 |
orbitcowboy
|
b37b0c0f78
|
Running astyle [ci skip]
|
2019-09-19 08:03:29 +02:00 |
amai2012
|
d97c826319
|
Compile fix for VisualStudio
|
2019-09-18 22:07:42 +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 |