cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity
11,751 Commits 348 Branches 121 Tags 100 MiB
ac980fb89b
Commit Graph

65 Commits

Author SHA1 Message Date
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 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
Alex Beregszaszi
f024efb7ab SMT: do not crash on referencing MagicVariableDeclaration 2018-08-07 20:43:20 +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
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
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
Leonardo Alt
ab251c7e7d Bool variables should not allow arithmetic comparison 2018-04-27 11:35:58 +02:00
Leonardo Alt
ba3d16fc58 [SMTChecker] Remove 'information is erase' message for if-else 2018-04-19 09:28:44 +02:00
Leonardo Alt
78ba34608f [SMTChecker] Using solUnimplementedAssert instead of solAssert when applicable 2018-04-18 13:17:59 +02:00
Leonardo Alt
ae3350ae03 [SMTChecker] Integration with CVC4 2018-04-17 12:26:58 +01:00
Leonardo Alt
9b64dc501d [SMTChecker_Bool] Fix PR review comments: method renaming and solAssert 2018-03-12 20:16:47 +01:00
Leonardo Alt
c2d26eb6a2 [SMTChecker_Bool] Fix PR comments; Add support to gt, ge, lt, le. and tests. 2018-03-12 20:16:47 +01:00
Leonardo Alt
6a940f0a99 [SMTChecker] Support to Bool variables 2018-03-12 20:16:47 +01:00
Leonardo Alt
21c6b80fc9 Supported types listed in SSAVariable 2018-02-28 18:05:20 +01: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
a256983320 Fix expression creation problems. 2017-11-30 01:20:21 +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