aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal
Commit message (Expand)AuthorAgeFilesLines
* [SMTChecker] Remove 'information is erase' message for if-elseLeonardo Alt2018-04-192-10/+10
* [SMTChecker] Using solUnimplementedAssert instead of solAssert when applicableLeonardo Alt2018-04-181-2/+2
* [SMTChecker] Integration with CVC4Leonardo Alt2018-04-176-19/+287
* [SMTChecker] Removing usage of UFs to access SSA indicesLeonardo Alt2018-04-056-10/+20
* [SMTChecker_Bool] Fix PR review comments: method renaming and solAssertLeonardo Alt2018-03-133-16/+17
* [SMTChecker_Bool] Fix PR comments; Add support to gt, ge, lt, le. and tests.Leonardo Alt2018-03-1310-41/+85
* [SMTChecker] Support to Bool variablesLeonardo Alt2018-03-136-8/+107
* 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 wi...Leonardo Alt2017-12-142-5/+19
* [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 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
* | 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 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
* refactoring functionCallAnnotationdjudjuu2017-05-191-1/+1
* Change references to FunctionType::LocationAlex Beregszaszi2017-03-161-7/+7
* Fix licensing headersVoR02202016-11-232-8/+8
* Add support for do/while loopsRhett Aultman2016-11-101-0/+10
* Chack for non-version pragmasYoichi Hirai2016-10-111-1/+10
* formal: ignore pragmas during Why3 code generationYoichi Hirai2016-10-112-0/+6
* Prepare for leaky exceptionsYoichi Hirai2016-09-101-0/+4
* toFormalType reports errors by an exceptionYoichi Hirai2016-09-102-21/+71
* Translate mapping types into Why3 arrays when keys are integersYoichi Hirai2016-09-101-0/+14
* Add Address module in the WhyML preludeYoichi Hirai2016-09-081-0/+9
* Merge pull request #1041 from pirapira/typo_and_whitespacechriseth2016-09-082-2/+2
|\
| * 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 fo...RJ Catalano2016-05-101-2/+10
* Fixed Windows warningsBob Summerwill2016-03-181-1/+1
* - inline and assembly keywords addedLianaHus2016-03-121-1/+1
* 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 v1.2.3 (git 2.25.1) at 2024-10-30 08:40:13 +0800