Leonardo Alt
|
06c3f0953a
|
[SMTChecker] Support bound function calls
|
2018-11-19 15:29:00 +01: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 |
|
chriseth
|
01566c2e1a
|
Merge pull request #5272 from ethereum/smt_special_vars
[SMTChecker] Support msg.*, tx.*, block.*, gasleft and blockhash
|
2018-10-24 14:34:17 +02:00 |
|
Leonardo Alt
|
e2cf5f6ed9
|
Add gasleft constraint and use full member access name
|
2018-10-22 18:19:11 +02:00 |
|
Christian Parpart
|
f112377dd4
|
Refactor solidity::Token into an enum class with TokenTraits helper namespace
|
2018-10-22 17:00:51 +02:00 |
|
Leonardo Alt
|
b46b827c30
|
[SMTChecker] Support msg.*, tx.*, block.*, gasleft and blockhash
|
2018-10-19 15:52:16 +02:00 |
|
Leonardo Alt
|
070471d8d4
|
Fix possibly effectless map emplace
|
2018-10-17 19:00:38 +02:00 |
|
Leonardo Alt
|
c92d3b537d
|
[SMTChecker] Refactor expressions such that they also use SymbolicVariable
|
2018-10-17 18:36:24 +02:00 |
|
Leonardo
|
3db1ce0e14
|
Merge pull request #5235 from ethereum/smt_refactor_types
[SMTChecker] Refactoring types
|
2018-10-17 18:35:48 +02:00 |
|
Bhargava Shastry
|
67fd3ca4a7
|
Retained move/copy semantics; removed const qualifier from Expression's members name (of type std::string) and arguments (of type std::vector<Expression>)
|
2018-10-17 16:46:18 +02:00 |
|
Bhargava Shastry
|
546b08c158
|
Fix compiler warning: clang-8 warns of explicitly-defined op implicitly deleted for Expression object's copy and move constructors
|
2018-10-17 16:42:51 +02:00 |
|
Leonardo Alt
|
afe83cc28b
|
Refactor SymbolicAddressVariable and SymbolicVariable allocation
|
2018-10-17 15:58:13 +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 |
|
chriseth
|
2384947521
|
Merge pull request #5209 from ethereum/smt_ssa_refactor
[SMTChecker] Refactor SSAVariable such that it only uses Type and not Declaration
|
2018-10-15 16:49:47 +02:00 |
|
Leonardo Alt
|
e4851cf59e
|
[SMTChecker] Inline calls to internal functions
|
2018-10-15 15:11:21 +02:00 |
|
Leonardo Alt
|
4a4620ac95
|
Refactor SSAVariable such that it only uses Type and not Declaration
|
2018-10-15 14:20:54 +02:00 |
|
Alex Beregszaszi
|
fa0ce6a7e7
|
Use empty() instead of size() == 0
|
2018-10-09 04:29:37 +01:00 |
|
Anurag Dashputre
|
3321000f67
|
Removing extra default cases to force compile time error, instead of runtime.
|
2018-09-30 12:40:38 +05:30 |
|
Daniel Kirchner
|
87804b6419
|
Split IntegerType into IntegerType and AddressType.
|
2018-09-05 12:19:14 +02:00 |
|
Daniel Kirchner
|
9b4546c487
|
Add workarounds for building against CVC4 on ArchLinux.
|
2018-08-08 19:02:59 +02:00 |
|
Alex Beregszaszi
|
f024efb7ab
|
SMT: do not crash on referencing MagicVariableDeclaration
|
2018-08-07 20:43:20 +01:00 |
|
Alex Beregszaszi
|
6003ed2abd
|
Merge pull request #4603 from ethereum/smtlib2
[SMTLib2] Fix repeated declarations
|
2018-08-02 12:04:58 +01:00 |
|
Leonardo Alt
|
90f319615f
|
SMT model variables are sorted and printed as secondary source location
|
2018-08-01 23:27:46 +02:00 |
|
Leonardo Alt
|
b6a2655513
|
Replace "value" by "<result>" in the SMT model
|
2018-08-01 23:27:11 +02:00 |
|
Leonardo Alt
|
41ac3d6cfb
|
Remove repeated declarations in Z3 and CVC4 as well
|
2018-08-01 11:12:56 +02:00 |
|
Alex Beregszaszi
|
179427fd65
|
Import dev::solidity namespace in SMTPortfolio
|
2018-07-27 23:17:17 +01:00 |
|
Leonardo Alt
|
f249f9c86f
|
[SMTLib2] Fix repeated declarations
|
2018-07-27 17:34:44 +01:00 |
|
Alex Beregszaszi
|
dea0567e06
|
Fix unterminated parentheses typo in SMTLib2
Found by @leonardoalt
|
2018-07-27 17:33:53 +01:00 |
|
Leonardo Alt
|
55c1fb60b4
|
[SMTChecker] Add CheckResult::CONFLICTING
|
2018-07-27 16:16:26 +01:00 |
|
Leonardo Alt
|
87a38e1abe
|
[SMTChecker] SMTPortfolio: use all SMT solvers available
|
2018-07-27 16:15:34 +01:00 |
|
Leonardo Alt
|
b356f6a7f9
|
Setting timeout to Z3 and CVC4
|
2018-07-27 16:01:48 +02:00 |
|
Leonardo Alt
|
06dbcb3afe
|
Only ask for a model if it's SAT
|
2018-07-27 14:13:22 +02:00 |
|
Alex Beregszaszi
|
ae15b52d93
|
Merge pull request #4565 from ethereum/smt-stringutils-crash
Add assert for both branches in mergeVariables in SMTChecker
|
2018-07-25 11:08:47 +01:00 |
|
Alex Beregszaszi
|
a5a61a0b77
|
More consistent catch statements
Also take const& in all cases.
|
2018-07-25 01:18:09 +01:00 |
|
Alex Beregszaszi
|
d30a6de942
|
Add better warning on binary operation on non-integer types in SMT Checker
|
2018-07-24 23:23:54 +01:00 |
|
Alex Beregszaszi
|
278372c13d
|
Add assert for both branches in mergeVariables in SMTChecker
|
2018-07-24 22:43:05 +01:00 |
|
Cryptomental
|
140dbfdbd8
|
Code, Changelog, ReleaseChecklist: Fix typos.
Refs: #4442
|
2018-07-11 00:26:23 +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
|
0b6eea0c55
|
Bool variables should not allow arithmetic comparison
|
2018-05-16 18:32:47 +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 |
|
chriseth
|
8debded743
|
Revert "BREAKING: Bool variables should not allow arithmetic comparison"
|
2018-05-02 15:56:59 +02:00 |
|
chriseth
|
42289b642f
|
Merge pull request #4003 from ethereum/bool_vars_comparison
BREAKING: Bool variables should not allow arithmetic comparison
|
2018-05-02 15:56:06 +02:00 |
|
Alexander Arlt
|
f94b793472
|
Add virtual destructors on base classes.
|
2018-05-02 13:29:16 +02:00 |
|
Leonardo Alt
|
ab251c7e7d
|
Bool variables should not allow arithmetic comparison
|
2018-04-27 11:35:58 +02:00 |
|