cerc-io/solidity
11
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
9,345 Commits 348 Branches 121 Tags
7530592a583dcb1a02bc5c8a01bde89a399a448d
Commit Graph
74 Commits
Author SHA1 Message Date
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 0e2a9658d2 Explain IntIntFun and merge assertion. 2017-11-23 19:02:47 +01:00
chriseth 762d591a47 Introduce sorts for smt expressions. 2017-11-22 15:20:26 +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 95a65dc04c Fix boolean constants. 2017-11-22 02:35:34 +00:00
chriseth 22c689d516 Check for conditions being constant. 2017-11-22 02:35:34 +00:00
chriseth e5de4a66ed Tests. 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 7d0e46bf59 Merge pull request #3030 from ethereum/smt-variable-types 
SMT enforce variable types
 2017-10-20 16:55:09 +02:00
Alex Beregszaszi 7a4c165518 Remove unused variable in Z3 2017-10-18 23:18:11 +01:00
chriseth 153ae98878 Catch exception in Z3. 
Note: This exception might not be the result of resource limitation,
it might also hint towards usage error.
 2017-10-17 18:30:10 +01:00
Alex Beregszaszi a71c6faf0f Remove duplicate >= in Z3 2017-10-17 18:30:07 +01:00
chriseth 1f97c1ea8f Rename variables in SMT checker. 2017-10-17 18:29:53 +01:00
Alex Beregszaszi 18ae0c3d78 SMT enforce variable types 2017-10-05 12:29:20 +01:00
Alex Beregszaszi 10529e994f SMT should not crash on typecast/structs 2017-10-05 11:41:11 +01:00
Alex Beregszaszi 66b188cce9 Merge pull request #3022 from ethereum/assert 
Use solAssert and not assert
 2017-10-04 14:11:43 +01:00
Alex Beregszaszi a9847c9551 Use solAssert and not assert 2017-10-04 13:05:55 +01:00
chriseth 5ee3ceaef7 Remove leftover couts. 2017-09-29 12:44:39 +02:00
Alex Beregszaszi 1c0c5d923a Mark constructors explicit 2017-09-20 01:23:21 +01:00
chriseth 9e63710b8e Remove parameter names for defaulted functions. 2017-08-31 12:16:41 +02:00
chriseth cf5e1d6120 Review changes. 2017-08-23 17:37:35 +02:00
chriseth c93f0434cd Use experimental feature pragma for SMT checker. 2017-08-23 17:37:35 +02:00
chriseth 75f09f2a84 Partial support for if statements. 2017-08-23 17:37:35 +02:00
chriseth 5bfd5d98c1 Format numbers more nicely. 2017-08-23 17:37:35 +02:00
chriseth 1e05ebe50e Refactor Z3 read callback. 2017-08-23 17:37:35 +02:00
chriseth 9ac2ac14c1 Rename read file callback. 2017-08-23 17:37:35 +02:00
chriseth ab5e3a8f6d Introduce native Z3 support. 2017-08-23 17:37:35 +02:00
chriseth 4cea3d4aa4 Insert abstraction layer. 2017-08-23 17:37:35 +02:00
chriseth c9cf24458b Prepare build system for Z3. 2017-08-23 17:37:35 +02:00
chriseth b3f8ed457a Cleanup. 2017-08-23 14:24:30 +02:00
chriseth 39fc798999 Use file to communicate with z3. 2017-08-23 14:24:05 +02:00
chriseth df848859da Rewrite using SMTLIB2 interface. 2017-08-23 14:24:05 +02:00
chriseth 1ece7bf443 z3 conditions 2017-08-23 14:24:04 +02:00
Alex Beregszaszi 555dc4f46f Remove Why3 generator 2017-06-25 12:26:16 +01:00
Rhett Aultman 89b60ffbd4 Refactor error reporting 
This commit introduces ErrorReporter, a utility class which consolidates
all of the error logging functionality into a common set of functions.
It also replaces all direct interactions with an ErrorList with calls to
an ErrorReporter.

This commit resolves issue #2209
 2017-05-30 07:28:31 -07:00
djudjuu 1d22233a43 refactoring functionCallAnnotation 2017-05-19 15:48:07 +02:00
Alex Beregszaszi 3ae88377d6 Change references to FunctionType::Location 2017-03-16 12:49:52 +00:00
VoR0220 3f9f725737 Fix licensing headers 
Signed-off-by: VoR0220 <rj@erisindustries.com>
 2016-11-23 12:22:33 +01:00
Rhett Aultman 4524ad0870 Add support for do/while loops 
This commit adds support for a standard do <statement> while <expr>;
form of statement.  While loops were already being supported; supporting
a do/while loop mostly involves reusing code from while loops but putting
the conditional checking last.
 2016-11-10 07:07:25 -08:00
Yoichi Hirai ab1f4632aa Chack for non-version pragmas 2016-10-11 00:07:11 +02:00
Yoichi Hirai 092e5829d8 formal: ignore pragmas during Why3 code generation 
Fixes #1177
 2016-10-11 00:01:29 +02:00
Yoichi Hirai 4337e70cca Prepare for leaky exceptions 
Now toFormalType() reports errors by exceptions, they will be
sometimes leaked to the wider context.  This commits adds a catch.
 2016-09-09 20:15:13 +02:00