aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal
Commit message (Collapse)AuthorAgeFilesLines
* This z3 option is necessary for good solving performanceLeonardo Alt2018-03-041-0/+1
|
* Fix PR commentsLeonardo Alt2018-03-013-12/+0
|
* Fix PR commentsLeonardo Alt2018-03-016-23/+37
|
* Supported types listed in SSAVariableLeonardo Alt2018-03-014-3/+20
|
* Integer min and max values placed under SymbolicIntVar instead of SMTCheckerLeonardo Alt2018-03-014-19/+9
|
* [SMTChecker] A little refactoring on SSA varsLeonardo Alt2018-03-018-54/+395
|
* [SMTChecker] Variables are merged after branches (ite variables)Leonardo Alt2018-01-052-13/+37
|
* [SMTChecker] Fix typo in the code (satisifable->satisfiable)Leonardo Alt2017-12-192-8/+8
|
* [SMTChecker] Helper functions to add an expression to the solver conjoined ↵Leonardo Alt2017-12-142-5/+19
| | | | with or implied by the current path conditions
* [SMTChecker] Keep track of current path conditionsLeonardo Alt2017-12-143-8/+41
|
* Fix expression creation problems.chriseth2017-11-301-19/+30
|
* Fix signed division.chriseth2017-11-302-2/+20
|
* Unary operators and division.chriseth2017-11-304-60/+154
|
* Explain IntIntFun and merge assertion.chriseth2017-11-241-3/+7
|
* Introduce sorts for smt expressions.chriseth2017-11-223-48/+37
|
* Fix problem with non-value-typed variables.chriseth2017-11-222-14/+16
|
* For loop.chriseth2017-11-222-0/+43
|
* Fix boolean constants.chriseth2017-11-221-2/+7
|
* Check for conditions being constant.chriseth2017-11-224-27/+102
|
* Tests.chriseth2017-11-221-5/+0
|
* Track usage of variables.chriseth2017-11-224-70/+215
|
* Handle branches.chriseth2017-11-222-54/+88
|
* Merge pull request #3030 from ethereum/smt-variable-typeschriseth2017-10-202-1/+16
|\ | | | | SMT enforce variable types
| * SMT enforce variable typesAlex Beregszaszi2017-10-052-1/+16
| |
* | Remove unused variable in Z3Alex Beregszaszi2017-10-191-1/+1
| |
* | Catch exception in Z3.chriseth2017-10-181-18/+27
| | | | | | | | | | Note: This exception might not be the result of resource limitation, it might also hint towards usage error.
* | Remove duplicate >= in Z3Alex Beregszaszi2017-10-181-2/+1
| |
* | Rename variables in SMT checker.chriseth2017-10-182-11/+11
| |
* | SMT should not crash on typecast/structsAlex Beregszaszi2017-10-051-0/+10
|/
* Merge pull request #3022 from ethereum/assertAlex Beregszaszi2017-10-041-1/+1
|\ | | | | Use solAssert and not assert
| * Use solAssert and not assertAlex Beregszaszi2017-10-041-1/+1
| |
* | Remove leftover couts.chriseth2017-09-291-7/+0
|/
* Mark constructors explicitAlex Beregszaszi2017-09-201-1/+1
|
* Remove parameter names for defaulted functions.chriseth2017-08-311-4/+4
|
* Review changes.chriseth2017-08-235-24/+24
|
* Use experimental feature pragma for SMT checker.chriseth2017-08-231-6/+1
|
* Partial support for if statements.chriseth2017-08-234-16/+128
|
* Format numbers more nicely.chriseth2017-08-231-11/+25
|
* Refactor Z3 read callback.chriseth2017-08-236-133/+46
|
* Rename read file callback.chriseth2017-08-233-4/+6
|
* Introduce native Z3 support.chriseth2017-08-232-0/+244
|
* Insert abstraction layer.chriseth2017-08-235-148/+225
|
* Prepare build system for Z3.chriseth2017-08-231-0/+3
|
* Cleanup.chriseth2017-08-238-715/+685
|
* Use file to communicate with z3.chriseth2017-08-233-14/+274
|
* Rewrite using SMTLIB2 interface.chriseth2017-08-234-63/+233
|
* z3 conditionschriseth2017-08-234-0/+636
|
* Remove Why3 generatorAlex Beregszaszi2017-06-252-1045/+0
|
* Refactor error reportingRhett Aultman2017-05-302-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 functionCallAnnotationdjudjuu2017-05-191-1/+1
|
* Change references to FunctionType::LocationAlex Beregszaszi2017-03-161-7/+7
|
* Fix licensing headersVoR02202016-11-232-8/+8
| | | | Signed-off-by: VoR0220 <rj@erisindustries.com>
* Add support for do/while loopsRhett Aultman2016-11-101-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 pragmasYoichi Hirai2016-10-111-1/+10
|
* formal: ignore pragmas during Why3 code generationYoichi Hirai2016-10-112-0/+6
| | | | Fixes #1177
* Prepare for leaky exceptionsYoichi Hirai2016-09-101-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 exceptionYoichi Hirai2016-09-102-21/+71
| | | | This allows error reporting without passing `ASTNode` to `toFormalType()`
* Translate mapping types into Why3 arrays when keys are integersYoichi Hirai2016-09-101-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 preludeYoichi Hirai2016-09-081-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_whitespacechriseth2016-09-082-2/+2
|\ | | | | Fix a typo and a whitespace inconsistency
| * Fix a typo and whitespacesYoichi Hirai2016-09-072-2/+2
| |
* | Append an issue id #1043 to a @todo comment about itYoichi Hirai2016-09-071-1/+1
|/
* Fix crash when using json compiler with exponentiation.chriseth2016-08-201-2/+7
|
* Handle external effects.chriseth2016-07-132-48/+169
|
* Simplify interface of RationalNumber.chriseth2016-05-111-2/+2
|
* changed names for Rational Constants and categoriesVoR02202016-05-101-4/+4
|
* initial work for fixed types...potentially needing a constant literal type ↵RJ Catalano2016-05-101-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 warningsBob Summerwill2016-03-181-1/+1
|
* - inline and assembly keywords addedLianaHus2016-03-121-1/+1
| | | | - some style fixes
* Do not store elements of a contract by AST node type.chriseth2015-11-262-11/+6
|
* Fix MSVC errors and warnings.chriseth2015-11-261-1/+1
|
* Style.chriseth2015-11-251-1/+2
|
* Again some why3 fixes with regards to separators in blocks.chriseth2015-11-252-26/+34
|
* Style.chriseth2015-11-231-2/+5
|
* addmod and mulmod for why3.chriseth2015-11-231-17/+36
|
* Why3: Direct references to variables using `#`.chriseth2015-11-232-1/+75
|
* Formal Verification: State variables.chriseth2015-11-192-20/+70
|
* Fix problems with statement blocks.chriseth2015-11-112-21/+46
|
* Rename error type.chriseth2015-10-281-1/+1
|
* Preliminary why3 code output.chriseth2015-10-272-0/+640
generated by cgit (git 2.34.1) at 2024-11-18 14:10:55 +0800