Leonardo Alt
a8209e9899
[SMTChecker] Shortcut RationalNumber expressions
2019-03-11 12:53:49 +01:00
Leonardo Alt
29b2ab6f66
Handle aliasing
2019-03-06 11:29:54 +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
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
chriseth
bb10be789c
Inject SMTLIB2 queries and responses via standard-json-io.
2018-11-23 09:43:49 +01:00
Leonardo Alt
ec84a7dc9b
[SMTChecker] Refactor setZeroValue and setUnknownValue
2018-11-22 16:42:51 +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
Christian Parpart
87821c53c3
Isolating files shared between Yul- and Solidity language frontend.
2018-11-21 18:58:12 +00:00
Alex Beregszaszi
2c6e1888eb
Merge pull request #5466 from ethereum/smt_refactor_sort_patch1
...
[SMTChecker] Refactor smt::Sort and its usage
2018-11-21 15:17:58 +00:00
Leonardo Alt
01ce43e51b
[SMTChecker] Refactor smt::Sort and its usage
2018-11-21 15:46:47 +01:00
mordax
ea8b7d803e
Removing redundant virtual from override function declaration
...
Remove trailing whitespace
Remove changelog change
2018-11-21 14:37:32 +00:00
Leonardo Alt
70bb0eaf95
[SMTChecker] Implement uninterpreted functions and use it for blockhash()
2018-11-15 09:12:42 +01:00
Leonardo Alt
9a4fd946c3
Add Scanner function that prints source based on SourceLocation
2018-11-13 13:49:29 +01:00
Leonardo Alt
d8cbf321da
Grouping of symbolic variables in the same file and support to FixedBytes
2018-10-25 09:30:48 +02:00
Leonardo Alt
b46b827c30
[SMTChecker] Support msg.*, tx.*, block.*, gasleft and blockhash
2018-10-19 15:52:16 +02:00
Leonardo Alt
c92d3b537d
[SMTChecker] Refactor expressions such that they also use SymbolicVariable
2018-10-17 18:36:24 +02:00
Leonardo Alt
aa23326e06
Consistent renaming of 'counters' and 'sequence' to 'index'
2018-10-17 15:58:13 +02:00
Leonardo Alt
ec39fdcb3c
[SMTChecker] Refactoring types
2018-10-17 15:58:13 +02:00
Leonardo Alt
e4851cf59e
[SMTChecker] Inline calls to internal functions
2018-10-15 15:11:21 +02:00
Leonardo Alt
207d5859d1
Refactoring Declaration -> VariableDeclaration (more precise)
2018-06-12 10:58:50 +02:00
Leonardo Alt
48652c88af
Review comments
2018-06-12 10:58:50 +02:00
Leonardo Alt
678a769cd7
Refactoring how storage and local variables are managed.
2018-06-12 10:58:50 +02:00
Leonardo Alt
4117e859eb
[SMTChecker] Declaring all state vars before any function is visited
2018-05-15 14:28:08 +02:00
Leonardo Alt
2dbb35d4a8
[SMTChecker] Support to integer and Bool storage vars
2018-05-15 14:22:50 +02:00
Leonardo Alt
ba3d16fc58
[SMTChecker] Remove 'information is erase' message for if-else
2018-04-19 09:28:44 +02:00
Leonardo Alt
3b2851ee41
Integer min and max values placed under SymbolicIntVar instead of SMTChecker
2018-02-28 18:05:20 +01:00
Leonardo Alt
f41591b3dd
[SMTChecker] A little refactoring on SSA vars
2018-02-28 18:05:20 +01:00
Leonardo Alt
d0abc5359b
[SMTChecker] Variables are merged after branches (ite variables)
2018-01-04 18:20:12 +01:00
Leonardo Alt
b588134840
[SMTChecker] Fix typo in the code (satisifable->satisfiable)
2017-12-18 17:31:27 +01:00
Leonardo Alt
a1e296e392
[SMTChecker] Helper functions to add an expression to the solver conjoined with or implied by the current path conditions
2017-12-13 17:59:36 +01:00
Leonardo Alt
2af4d7c7dd
[SMTChecker] Keep track of current path conditions
2017-12-13 17:39:10 +01:00
chriseth
d160ec8595
Fix signed division.
2017-11-30 01:20:21 +01:00
chriseth
19e067465a
Unary operators and division.
2017-11-30 01:20:21 +01:00
chriseth
8538a25f8d
Fix problem with non-value-typed variables.
2017-11-22 02:35:34 +00:00
chriseth
19d5c42429
For loop.
2017-11-22 02:35:34 +00:00
chriseth
22c689d516
Check for conditions being constant.
2017-11-22 02:35:34 +00:00
chriseth
b37377641d
Track usage of variables.
2017-11-22 02:35:34 +00:00
chriseth
f62caf587e
Handle branches.
2017-11-22 02:35:34 +00:00
chriseth
1f97c1ea8f
Rename variables in SMT checker.
2017-10-17 18:29:53 +01:00
chriseth
cf5e1d6120
Review changes.
2017-08-23 17:37:35 +02:00
chriseth
75f09f2a84
Partial support for if statements.
2017-08-23 17:37:35 +02:00
chriseth
9ac2ac14c1
Rename read file callback.
2017-08-23 17:37:35 +02:00
chriseth
4cea3d4aa4
Insert abstraction layer.
2017-08-23 17:37:35 +02:00
