aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal
Commit message (Expand)AuthorAgeFilesLines
* Fix move bug.chriseth2018-11-291-1/+2
* [SMTChecker] Unknown answer for constant condition check should not do anythingLeonardo Alt2018-11-261-0/+4
* Testing with smtlib2 interface always thereLeonardo Alt2018-11-231-6/+1
* Error message stays in the SMTCheckerLeonardo Alt2018-11-232-8/+9
* Display better error message in SMTLib2Leonardo Alt2018-11-233-8/+10
* Rename function and warn if responses are supplied for Z3.chriseth2018-11-231-1/+7
* Inject SMTLIB2 queries and responses via standard-json-io.chriseth2018-11-237-18/+39
* Stylechriseth2018-11-231-7/+9
* [SMTChecker] Refactor setZeroValue and setUnknownValueLeonardo Alt2018-11-226-44/+58
* [SMTChecker] Add ArraySort and array operationsLeonardo Alt2018-11-225-2/+76
* [SMTChecker] Add FunctionSort and refactors the solver interface to create va...Leonardo Alt2018-11-2214-128/+134
* Introduce namespace `langutil` in liblangutil directory.Christian Parpart2018-11-222-9/+15
* Isolating files shared between Yul- and Solidity language frontend.Christian Parpart2018-11-227-7/+7
* Merge pull request #5466 from ethereum/smt_refactor_sort_patch1Alex Beregszaszi2018-11-2113-100/+102
|\
| * [SMTChecker] Refactor smt::Sort and its usageLeonardo Alt2018-11-2113-100/+102
* | Removing redundant virtual from override function declarationmordax2018-11-211-18/+18
|/
* [SMTChecker] Support bound function callsLeonardo Alt2018-11-191-0/+12
* [SMTChecker] Implement uninterpreted functions and use it for blockhash()Leonardo Alt2018-11-1515-25/+102
* Add Scanner function that prints source based on SourceLocationLeonardo Alt2018-11-132-2/+7
* Grouping of symbolic variables in the same file and support to FixedBytesLeonardo Alt2018-10-2512-280/+144
* Merge pull request #5272 from ethereum/smt_special_varschriseth2018-10-2413-61/+144
|\
| * Add gasleft constraint and use full member access nameLeonardo Alt2018-10-235-16/+31
| * [SMTChecker] Support msg.*, tx.*, block.*, gasleft and blockhashLeonardo Alt2018-10-1911-51/+119
* | Refactor `solidity::Token` into an `enum class` with `TokenTraits` helper nam...Christian Parpart2018-10-221-6/+6
|/
* Fix possibly effectless map emplaceLeonardo Alt2018-10-181-7/+10
* [SMTChecker] Refactor expressions such that they also use SymbolicVariableLeonardo Alt2018-10-184-77/+57
* Merge pull request #5235 from ethereum/smt_refactor_typesLeonardo2018-10-1814-218/+378
|\
| * Refactor SymbolicAddressVariable and SymbolicVariable allocationLeonardo Alt2018-10-178-51/+159
| * Consistent renaming of 'counters' and 'sequence' to 'index'Leonardo Alt2018-10-1710-71/+71
| * [SMTChecker] Refactoring typesLeonardo Alt2018-10-1712-150/+202
* | Retained move/copy semantics; removed const qualifier from Expression's membe...Bhargava Shastry2018-10-171-2/+4
* | Fix compiler warning: clang-8 warns of explicitly-defined op implicitly delet...Bhargava Shastry2018-10-171-2/+0
|/
* Merge pull request #5209 from ethereum/smt_ssa_refactorchriseth2018-10-159-37/+48
|\
| * Refactor SSAVariable such that it only uses Type and not DeclarationLeonardo Alt2018-10-159-37/+48
* | [SMTChecker] Inline calls to internal functionsLeonardo Alt2018-10-152-68/+243
|/
* Use empty() instead of size() == 0Alex Beregszaszi2018-10-091-1/+1
* Removing extra default cases to force compile time error, instead of runtime.Anurag Dashputre2018-09-302-4/+0
* Split IntegerType into IntegerType and AddressType.Daniel Kirchner2018-09-053-6/+15
* Add workarounds for building against CVC4 on ArchLinux.Daniel Kirchner2018-08-091-0/+11
* SMT: do not crash on referencing MagicVariableDeclarationAlex Beregszaszi2018-08-081-2/+8
* Merge pull request #4603 from ethereum/smtlib2Alex Beregszaszi2018-08-024-18/+44
|\
| * Remove repeated declarations in Z3 and CVC4 as wellLeonardo Alt2018-08-012-7/+15
| * [SMTLib2] Fix repeated declarationsLeonardo Alt2018-07-282-11/+29
* | SMT model variables are sorted and printed as secondary source locationLeonardo Alt2018-08-021-3/+11
* | Replace "value" by "<result>" in the SMT modelLeonardo Alt2018-08-021-3/+3
* | Import dev::solidity namespace in SMTPortfolioAlex Beregszaszi2018-07-281-0/+1
|/
* Fix unterminated parentheses typo in SMTLib2Alex Beregszaszi2018-07-281-1/+1
* [SMTChecker] Add CheckResult::CONFLICTINGLeonardo Alt2018-07-273-4/+10
* [SMTChecker] SMTPortfolio: use all SMT solvers availableLeonardo Alt2018-07-2710-45/+246
* Setting timeout to Z3 and CVC4Leonardo Alt2018-07-273-1/+8
* Only ask for a model if it's SATLeonardo Alt2018-07-273-3/+3
* Merge pull request #4565 from ethereum/smt-stringutils-crashAlex Beregszaszi2018-07-251-1/+9
|\
| * Add better warning on binary operation on non-integer types in SMT CheckerAlex Beregszaszi2018-07-251-1/+8
| * Add assert for both branches in mergeVariables in SMTCheckerAlex Beregszaszi2018-07-251-0/+1
* | More consistent catch statementsAlex Beregszaszi2018-07-251-1/+1
|/
* Code, Changelog, ReleaseChecklist: Fix typos.Cryptomental2018-07-111-1/+1
* Refactoring Declaration -> VariableDeclaration (more precise)Leonardo Alt2018-06-124-43/+42
* Review commentsLeonardo Alt2018-06-122-10/+8
* Refactoring how storage and local variables are managed.Leonardo Alt2018-06-122-29/+29
* Bool variables should not allow arithmetic comparisonLeonardo Alt2018-05-171-5/+1
* [SMTChecker] Declaring all state vars before any function is visitedLeonardo Alt2018-05-152-2/+15
* [SMTChecker] Support to integer and Bool storage varsLeonardo Alt2018-05-153-5/+31
* Revert "BREAKING: Bool variables should not allow arithmetic comparison"chriseth2018-05-021-1/+5
* Merge pull request #4003 from ethereum/bool_vars_comparisonchriseth2018-05-021-5/+1
|\
| * Bool variables should not allow arithmetic comparisonLeonardo Alt2018-04-271-5/+1
* | Add virtual destructors on base classes.Alexander Arlt2018-05-022-0/+2
|/
* [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 2025-03-03 10:38:09 +0800