Leonardo
3a3316393e
Merge pull request #6897 from ethereum/smt_check_pragma_earlier
...
[SMTChecker] Exit early if no pragma
2019-06-05 10:26:25 +02:00
Leonardo
c39ea56f93
Merge pull request #6896 from ethereum/smt_use_portfolio
...
[SMTChecker] Use SMTPortfolio directly
2019-06-05 10:26:05 +02:00
Leonardo
155af48b9d
Merge pull request #6895 from ethereum/smt_keep_assertions
...
[SMTChecker] Keep a copy of assertions that are added to the solvers
2019-06-05 10:25:45 +02:00
Leonardo Alt
4de1e20954
[SMTChecker] Exit early if no pragma
2019-06-04 17:12:15 +02:00
Leonardo Alt
91653526bb
[SMTChecker] Use SMTPortfolio directly instead of pointer to SolverInterface
2019-06-04 17:10:52 +02:00
Leonardo Alt
31ef421fff
[SMTChecker] Keep a copy of assertions that are added to the solvers
2019-06-04 17:09:04 +02:00
Leonardo Alt
d9ce9cab99
[SMTChecker] Use smtlib's implies instead of \!a or b
2019-06-04 14:23:44 +02:00
chriseth
e08f521b7e
Merge pull request #6764 from ethereum/smt_fix_tuple_ice
...
[SMTChecker] Fix ICE in unsupported function calls with multi return values
2019-05-20 15:18:11 +02:00
Leonardo Alt
60a4f03d3d
[SMTChecker] Fix ice in unsupported functions with multi return values
2019-05-16 18:23:42 +02:00
Leonardo Alt
5493a41842
[SMTChecker] Move global variables and functions to encoding context
2019-05-16 18:11:31 +02:00
Leonardo Alt
4e430ba0ae
[SMTChecker] Move expression handling to EncodingContext
2019-05-14 15:56:43 +02:00
Leonardo Alt
ebbe03cad6
[SMTChecker] Move variable handling to EncodingContext
2019-05-13 16:59:28 +02:00
chriseth
01dd9ba2ae
Merge pull request #6717 from ethereum/smt_namespace
...
Move SMT specific code into smt namespace
2019-05-13 12:45:34 +02:00
chriseth
e5d46767f1
Merge pull request #6722 from ethereum/smt_fix_variable_usage
...
[SMTChecker] Fix VariableUsage for IndexAccess
2019-05-13 10:17:26 +02:00
Leonardo Alt
fac383a233
Move SMT specific code into smt namespace
2019-05-10 20:03:11 +02:00
chriseth
cc40e65a4b
Merge pull request #6712 from ethereum/smt_unique_ptr
...
[SMTChecker] Use unique_ptr instead of shared_ptr where applicable
2019-05-10 12:53:53 +02:00
Leonardo Alt
3ea5c112d3
[SMTChecker] Fix VariableUsage for IndexAccess
2019-05-10 11:28:10 +02:00
Leonardo Alt
8d65fd18fc
[SMTChecker] Style changes
2019-05-09 19:15:43 +02:00
chriseth
89700dbcff
Merge pull request #6665 from ethereum/smt_inline_external_this
...
[SMTChecker] Inline external function calls to `this`
2019-05-09 19:09:08 +02:00
Leonardo Alt
ef32bf185f
[SMTChecker] Inline external function calls to this.
2019-05-09 16:53:30 +02:00
Leonardo Alt
c8a017ccd6
[SMTChecker] Use unique_ptr instead of shared_ptr where applicable.
2019-05-09 16:34:22 +02:00
Leonardo Alt
6027383ae5
[SMTChecker] Fix call to function at state var init
2019-05-09 16:12:44 +02:00
Leonardo Alt
3d52a6ca68
[SMTChecker] Fix ICE in branch-inline function call-modify local variable
2019-05-09 09:15:11 +02:00
Leonardo Alt
9893cae27a
[SMTChecker] Make mergeVariables deterministic
2019-05-08 20:46:01 +02:00
Leonardo Alt
0b046897ae
[SMTChecker] Fix unsupported type assignment
2019-05-08 14:28:23 +02:00
Leonardo Alt
3c7540ceb2
[SMTChecker] Support tuples with multiple var decls
2019-05-07 16:57:27 +02:00
Leonardo Alt
2139c20776
[SMTChecker] Support delete
2019-05-06 18:32:10 +02:00
Leonardo
e99efec085
Merge pull request #6652 from ethereum/smt_tuple_function
...
[SMTChecker] Support tuples as function calls with multiple return values
2019-05-06 15:19:24 +02:00
Leonardo Alt
80712f44cb
Fix short circuit with assignments
2019-05-06 11:04:43 +02:00
Leonardo Alt
5440a53d4d
[SMTChecker] Support tuples as function calls with multiple return values
2019-05-03 06:10:22 +02:00
Leonardo Alt
204dcf1771
[SMTChecker] Support tuple assignments
2019-05-02 12:55:34 +02:00
Leonardo Alt
6c7527ac90
[SMTChecker] Support tuple type declaration
2019-05-02 12:05:21 +02:00
Leonardo Alt
66655b87b0
[SMTChecker] Fix ICE in fixed point operations
2019-05-02 10:59:23 +02:00
Leonardo Alt
dd4e938265
[SMTChecker] Fix ICE in inherited state var
2019-05-02 10:03:12 +02:00
Leonardo Alt
a6db37ac9c
[SMTChecker] Fix bad cast in base constructor modifier.
2019-04-30 18:48:13 +02:00
Leonardo Alt
e4989369d0
Refactor cast from identifier ref decl to var decl
2019-04-30 11:08:36 +02:00
Leonardo Alt
762f79f84d
Refactor assignment handling
2019-04-30 11:08:36 +02:00
Leonardo Alt
fc482de695
[SMTChecker] Support address members
2019-04-25 16:24:36 +02:00
Leonardo Alt
dd1afeba52
[SMTChecker] Support this as address
2019-04-18 17:56:52 +02:00
chriseth
fce19bde58
Merge pull request #6545 from ethereum/smt_contracts
...
[SMTChecker] Support contract type
2019-04-18 13:01:18 +02:00
Leonardo Alt
ecd89393ee
[SMTChecker] Support contract type
2019-04-17 16:30:11 +02:00
Leonardo Alt
03d18f1b98
[SMTChecker] Add note about not inlining external function calls
2019-04-17 16:14:07 +02:00
Christian Parpart
721bf367a3
[libsolidity] TypeProvider: eliminate redundant "Type" suffix in provider function signatures.
2019-04-17 14:42:07 +02:00
Christian Parpart
862b65d6e3
[libsolidity] remove ReferenceType::copyForLocationIfReference (use TypeProvider instead)
2019-04-17 13:25:03 +02:00
Christian Parpart
58a45f2cb6
[libsolidity] TypeProvider: adds explicit uint256() accessor and removes default params in integerType(...).
2019-04-16 18:28:40 +02:00
Christian Parpart
bf43eebea9
libsolidity: Introducing TypeProvider API, for clear type system ownership.
2019-04-16 18:26:45 +02:00
Leonardo Alt
07fac9e381
[SMTChecker] Allow SymbolicVariable from smt::Sort
2019-04-15 14:52:46 +02:00
chriseth
bf5792f7ca
Merge pull request #6483 from ethereum/smt_support_mod
...
[SMTChecker] Support mod
2019-04-15 13:42:18 +02:00
chriseth
73ac8f6220
Merge pull request #6421 from ethereum/smt_fix_variable_usage
...
[SMTChecker] Refactor VariableUsage
2019-04-15 13:39:10 +02:00
Leonardo Alt
af9f16e014
[SMTChecker] Support mod
2019-04-12 12:39:25 +02:00
Leonardo Alt
4fe303530a
[SMTChecker] Show unsupported warning for asm blocks
2019-04-05 16:41:15 +02:00
Leonardo Alt
79d8a4e13a
[SMTChecker] Refactor VariableUsage
2019-04-05 11:38:37 +02:00
Leonardo Alt
aa9b9aa87e
[SMTChecker] Support unary inc/dec for array/mapping access
2019-04-02 16:53:19 +02:00
chriseth
84251e5a22
Merge pull request #6405 from ethereum/smt_compound_assignment
...
[SMTChecker] Support arithmetic compound assignment operators.
2019-03-28 18:27:25 +01:00
Leonardo Alt
a7e826a224
[SMTChecker] Implement short circuit
2019-03-28 16:08:30 +01:00
Leonardo Alt
15269067b5
Support arithmetic compound assignment operators
2019-03-28 15:27:52 +01:00
Leonardo Alt
ecbf36f271
Refactor computing symbolic arithmetic operation
2019-03-28 15:27:36 +01:00
Leonardo Alt
1d63b97857
Take inlined function calls into account when collecting touched variables
2019-03-28 14:32:47 +01:00
Leonardo Alt
6f9b69ebc3
Refactor function that retrieves FunctionDefinition from FunctionCall
2019-03-28 14:32:47 +01:00
Leonardo Alt
a207d7f44c
[SMTChecker] Add callstack model to overflow checks
2019-03-21 16:25:33 +01:00
Leonardo Alt
de89733bd6
[SMTChecker] Fix nullptr deref
2019-03-21 15:46:54 +01:00
Leonardo Alt
9659f40c8d
[SMTChecker] Support modifiers
2019-03-20 11:32:20 +01:00
Leonardo Alt
3296fb3764
Add callstack to model report
2019-03-20 10:35:29 +01:00
Leonardo Alt
a8209e9899
[SMTChecker] Shortcut RationalNumber expressions
2019-03-11 12:53:49 +01:00
Leonardo Alt
02d0e609b9
[SMTChecker] Support enums
2019-03-07 15:15:12 +01:00
Leonardo Alt
29b2ab6f66
Handle aliasing
2019-03-06 11:29:54 +01:00
Leonardo Alt
467c34999f
Do not throw on string literals
2019-03-06 11:29:26 +01:00
Leonardo Alt
e74f58130e
Add SMT type support to Solidity arrays
2019-03-06 11:29:26 +01:00
Mathias Baumann
f782125463
Fix SMT Checker crash due to missing type information
2019-02-28 11:55:45 +01:00
Leonardo Alt
bbd2c91e19
[SMTChecker] Replace dynamic_cast by category check
2019-02-26 00:47:59 +01:00
Leonardo Alt
34470f3549
[SMTChecker] Only check for overflow/underflow in the end of the function
2019-02-18 23:55:58 +01:00
chriseth
cb0ad2266c
Merge pull request #6008 from ethereum/smt_fix_abstract_assignment
...
[SMTChecker] Assert type is not function when assigning
2019-02-18 14:54:20 +01:00
Leonardo Alt
22cdfb18d4
[SMTChecker] Assert type is not function when assigning
2019-02-14 13:32:56 +01:00
Daniel Kirchner
8ca6715e18
More style checks.
2019-02-14 11:41:20 +01:00
Leonardo Alt
637546850f
[SMTChecker] Add mod operator
2019-02-07 14:24:40 +01:00
Leonardo Alt
9a33367bc6
[SMTChecker] Warn when no solver was found and there are unhandled queries.
2019-01-29 14:29:07 +01:00
Leonardo Alt
7f8ceaadab
[SMTChecker] Clear state knowledge after external function calls
2019-01-21 12:58:40 +01:00
Leonardo Alt
a10db051de
[SMTChecker] Support basic typecast
2019-01-16 13:00:54 +01:00
Leonardo Alt
cce377833a
Sort includes in libsolidity/formal
2018-12-17 18:26:10 +01:00
Leonardo Alt
9199718ec0
Clear all mapping knowledge after array variable assignment
2018-12-14 12:21:53 +01:00
Leonardo Alt
6a2809a582
[SMTChecker] Support to mapping
2018-12-14 12:21:53 +01:00
Leonardo Alt
08737e43dc
[SMTChecker] Use SymbolicFunctionVariable for uninterpreted functions
2018-12-11 11:28:25 +01:00
Leonardo Alt
de46bb2c42
[SMTChecker] Introduce SymbolicFunctionVariable
2018-12-10 11:34:29 +01:00
Kevin Kelley
fb6fd1b3c2
add a 'readable' format for large hex values
2018-12-05 22:15:02 +01:00
Leonardo Alt
b9f424e373
[SMTChecker] Simplify symbolic variables
2018-12-05 09:56:52 +01:00
Leonardo Alt
8069bb61da
[SMTChecker] Loops are unrolled once
2018-12-04 12:35:19 +01:00
Leonardo Alt
6d41ffb4a5
[SMTChecker] Remove unary plus operator
2018-12-03 10:35:38 +01:00
Leonardo Alt
2f6de12e8c
[SMTChecker] Make smt::Sort::operator== virtual
2018-11-30 10:41:15 +01:00
chriseth
9e9250c961
Fix move bug.
2018-11-29 15:32:38 +01:00
Leonardo Alt
aaaa92012c
[SMTChecker] Unknown answer for constant condition check should not do anything
2018-11-26 12:54:02 +01:00
Leonardo Alt
6251a289dd
Testing with smtlib2 interface always there
2018-11-23 09:43:49 +01:00
Leonardo Alt
dee0c4ded8
Error message stays in the SMTChecker
2018-11-23 09:43:49 +01:00
Leonardo Alt
f3c2309c73
Display better error message in SMTLib2
2018-11-23 09:43:49 +01:00
chriseth
54bed454f6
Rename function and warn if responses are supplied for Z3.
2018-11-23 09:43:49 +01:00
chriseth
bb10be789c
Inject SMTLIB2 queries and responses via standard-json-io.
2018-11-23 09:43:49 +01:00
chriseth
d686807153
Style
2018-11-22 21:13:02 +01:00
Leonardo Alt
ec84a7dc9b
[SMTChecker] Refactor setZeroValue and setUnknownValue
2018-11-22 16:42:51 +01:00
Leonardo Alt
20accf1a90
[SMTChecker] Add ArraySort and array operations
2018-11-22 14:04:20 +01:00
Leonardo Alt
13a142b039
[SMTChecker] Add FunctionSort and refactors the solver interface to create variables
2018-11-22 10:04:04 +01:00
Christian Parpart
d67322a186
Introduce namespace langutil
in liblangutil directory.
...
Also:
- Use {}-style list initialisation for SourceLocation construction
- Introduce new system includes
- Changes the API of the Scanner to take source as value (with move) as opposed to as a reference
2018-11-21 19:13:44 +00:00