| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | Catch exception in Z3. | chriseth | 2017-10-18 | 1 | -18/+27 |
| | | | | | | Note: This exception might not be the result of resource limitation, it might also hint towards usage error. | ||||
| * | Remove duplicate >= in Z3 | Alex Beregszaszi | 2017-10-18 | 1 | -2/+1 |
| | | |||||
| * | Rename variables in SMT checker. | chriseth | 2017-10-18 | 2 | -11/+11 |
| | | |||||
| * | SMT should not crash on typecast/structs | Alex Beregszaszi | 2017-10-05 | 1 | -0/+10 |
| | | |||||
| * | Merge pull request #3022 from ethereum/assert | Alex Beregszaszi | 2017-10-04 | 1 | -1/+1 |
| |\ | | | | | Use solAssert and not assert | ||||
| | * | Use solAssert and not assert | Alex Beregszaszi | 2017-10-04 | 1 | -1/+1 |
| | | | |||||
| * | | Remove leftover couts. | chriseth | 2017-09-29 | 1 | -7/+0 |
| |/ | |||||
| * | Mark constructors explicit | Alex Beregszaszi | 2017-09-20 | 1 | -1/+1 |
| | | |||||
| * | Remove parameter names for defaulted functions. | chriseth | 2017-08-31 | 1 | -4/+4 |
| | | |||||
| * | Review changes. | chriseth | 2017-08-23 | 5 | -24/+24 |
| | | |||||
| * | Use experimental feature pragma for SMT checker. | chriseth | 2017-08-23 | 1 | -6/+1 |
| | | |||||
| * | Partial support for if statements. | chriseth | 2017-08-23 | 4 | -16/+128 |
| | | |||||
| * | Format numbers more nicely. | chriseth | 2017-08-23 | 1 | -11/+25 |
| | | |||||
| * | Refactor Z3 read callback. | chriseth | 2017-08-23 | 6 | -133/+46 |
| | | |||||
| * | Rename read file callback. | chriseth | 2017-08-23 | 3 | -4/+6 |
| | | |||||
| * | Introduce native Z3 support. | chriseth | 2017-08-23 | 2 | -0/+244 |
| | | |||||
| * | Insert abstraction layer. | chriseth | 2017-08-23 | 5 | -148/+225 |
| | | |||||
| * | Prepare build system for Z3. | chriseth | 2017-08-23 | 1 | -0/+3 |
| | | |||||
| * | Cleanup. | chriseth | 2017-08-23 | 8 | -715/+685 |
| | | |||||
| * | Use file to communicate with z3. | chriseth | 2017-08-23 | 3 | -14/+274 |
| | | |||||
| * | Rewrite using SMTLIB2 interface. | chriseth | 2017-08-23 | 4 | -63/+233 |
| | | |||||
| * | z3 conditions | chriseth | 2017-08-23 | 4 | -0/+636 |
| | | |||||
| * | Remove Why3 generator | Alex Beregszaszi | 2017-06-25 | 2 | -1045/+0 |
| | | |||||
| * | Refactor error reporting | Rhett Aultman | 2017-05-30 | 2 | -26/+20 |
| | | | | | | | | | | 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 | ||||
| * | refactoring functionCallAnnotation | djudjuu | 2017-05-19 | 1 | -1/+1 |
| | | |||||
| * | Change references to FunctionType::Location | Alex Beregszaszi | 2017-03-16 | 1 | -7/+7 |
| | | |||||
| * | Fix licensing headers | VoR0220 | 2016-11-23 | 2 | -8/+8 |
| | | | | | Signed-off-by: VoR0220 <rj@erisindustries.com> | ||||
| * | Add support for do/while loops | Rhett Aultman | 2016-11-10 | 1 | -0/+10 |
| | | | | | | | | 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. | ||||
| * | Chack for non-version pragmas | Yoichi Hirai | 2016-10-11 | 1 | -1/+10 |
| | | |||||
| * | formal: ignore pragmas during Why3 code generation | Yoichi Hirai | 2016-10-11 | 2 | -0/+6 |
| | | | | | Fixes #1177 | ||||
| * | Prepare for leaky exceptions | Yoichi Hirai | 2016-09-10 | 1 | -0/+4 |
| | | | | | | Now toFormalType() reports errors by exceptions, they will be sometimes leaked to the wider context. This commits adds a catch. | ||||
| * | toFormalType reports errors by an exception | Yoichi Hirai | 2016-09-10 | 2 | -21/+71 |
| | | | | | This allows error reporting without passing `ASTNode` to `toFormalType()` | ||||
| * | Translate mapping types into Why3 arrays when keys are integers | Yoichi Hirai | 2016-09-10 | 1 | -0/+14 |
| | | | | | | Even when the keys are signed the translation is supposed to work because Why3 arrays allow negative indices. | ||||
| * | Add Address module in the WhyML prelude | Yoichi Hirai | 2016-09-08 | 1 | -0/+9 |
| | | | | | | | In the `--formal` output, this commit adds a module called `Address`, which defines the address type as unsigned integer type bounded at 2^160-1. | ||||
| * | Merge pull request #1041 from pirapira/typo_and_whitespace | chriseth | 2016-09-08 | 2 | -2/+2 |
| |\ | | | | | Fix a typo and a whitespace inconsistency | ||||
| | * | Fix a typo and whitespaces | Yoichi Hirai | 2016-09-07 | 2 | -2/+2 |
| | | | |||||
| * | | Append an issue id #1043 to a @todo comment about it | Yoichi Hirai | 2016-09-07 | 1 | -1/+1 |
| |/ | |||||
| * | Fix crash when using json compiler with exponentiation. | chriseth | 2016-08-20 | 1 | -2/+7 |
| | | |||||
| * | Handle external effects. | chriseth | 2016-07-13 | 2 | -48/+169 |
| | | |||||
| * | Simplify interface of RationalNumber. | chriseth | 2016-05-11 | 1 | -2/+2 |
| | | |||||
| * | changed names for Rational Constants and categories | VoR0220 | 2016-05-10 | 1 | -4/+4 |
| | | |||||
| * | initial work for fixed types...potentially needing a constant literal type ↵ | RJ Catalano | 2016-05-10 | 1 | -2/+10 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | for this notation Rational implemented...trying to figure out exponential fix for token bug, also quick fix for the wei and seconds fixed problem with var...probably a conversion problem for fixed in size capabilities adding fixed type tests Removing bitshift and regrouping fixed type tests together size capabilities functioning properly for fixed types got exponents up and working with their inverse, changed a few of the tests....something is working that likely shouldn't be slight changes to how to flip the rational negative around...still trying to figure it out tests added updated tests odd differences in trying soltest from solc binary, let me know if you can replicate test not working for odd reason fixed test problem with fixed literals...still need a way to log this error broken up the tests, added some, changed some things in types and began compiler work moar tests and prepping for rebuilding much of the types.cpp file further fixing initial work for fixed types...potentially needing a constant literal type for this | ||||
| * | Fixed Windows warnings | Bob Summerwill | 2016-03-18 | 1 | -1/+1 |
| | | |||||
| * | - inline and assembly keywords added | LianaHus | 2016-03-12 | 1 | -1/+1 |
| | | | | | - some style fixes | ||||
| * | Do not store elements of a contract by AST node type. | chriseth | 2015-11-26 | 2 | -11/+6 |
| | | |||||
| * | Fix MSVC errors and warnings. | chriseth | 2015-11-26 | 1 | -1/+1 |
| | | |||||
| * | Style. | chriseth | 2015-11-25 | 1 | -1/+2 |
| | | |||||
| * | Again some why3 fixes with regards to separators in blocks. | chriseth | 2015-11-25 | 2 | -26/+34 |
| | | |||||
| * | Style. | chriseth | 2015-11-23 | 1 | -2/+5 |
| | | |||||
| * | addmod and mulmod for why3. | chriseth | 2015-11-23 | 1 | -17/+36 |
| | | |||||
| * | Why3: Direct references to variables using `#`. | chriseth | 2015-11-23 | 2 | -1/+75 |
| | | |||||
| * | Formal Verification: State variables. | chriseth | 2015-11-19 | 2 | -20/+70 |
| | | |||||
| * | Fix problems with statement blocks. | chriseth | 2015-11-11 | 2 | -21/+46 |
| | | |||||
| * | Rename error type. | chriseth | 2015-10-28 | 1 | -1/+1 |
| | | |||||
| * | Preliminary why3 code output. | chriseth | 2015-10-27 | 2 | -0/+640 |
 |
index : dexon-solidity | |
| DEXON fork of Solidity (https://github.com/dexon-foundation/dsolidity) |
| aboutsummaryrefslogtreecommitdiffstats |