aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal
Commit message (Collapse)AuthorAgeFilesLines
* [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 ↵Leonardo Alt2018-11-2214-128/+134
| | | | variables
* Introduce namespace `langutil` in liblangutil directory.Christian Parpart2018-11-222-9/+15
| | | | | | | Also: - Use {}-style list initialisation for SourceLocation construction - Introduce new system includes - Changes the API of the Scanner to take source as value (with move) as opposed to as a reference
* 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 usage
| * [SMTChecker] Refactor smt::Sort and its usageLeonardo Alt2018-11-2113-100/+102
| |
* | Removing redundant virtual from override function declarationmordax2018-11-211-18/+18
|/ | | | | | Remove trailing whitespace Remove changelog change
* [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
|\ | | | | [SMTChecker] Support msg.*, tx.*, block.*, gasleft and blockhash
| * 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 ↵Christian Parpart2018-10-221-6/+6
|/ | | | namespace
* 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
|\ | | | | [SMTChecker] Refactoring types
| * 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 ↵Bhargava Shastry2018-10-171-2/+4
| | | | | | | | members name (of type std::string) and arguments (of type std::vector<Expression>)
* | Fix compiler warning: clang-8 warns of explicitly-defined op implicitly ↵Bhargava Shastry2018-10-171-2/+0
|/ | | | deleted for Expression object's copy and move constructors
* Merge pull request #5209 from ethereum/smt_ssa_refactorchriseth2018-10-159-37/+48
|\ | | | | [SMTChecker] Refactor SSAVariable such that it only uses Type and not Declaration
| * 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
|\ | | | | [SMTLib2] Fix repeated declarations
| * 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
| | | | Found by @leonardoalt
* [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 assert for both branches in mergeVariables in SMTChecker
| * 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
|/ | | | Also take const& in all cases.
* Code, Changelog, ReleaseChecklist: Fix typos.Cryptomental2018-07-111-1/+1
| | | | Refs: #4442
* 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
|\ | | | | BREAKING: Bool variables should not allow arithmetic comparison
| * 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 ↵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 v1.2.3 (git 2.25.1) at 2024-11-15 21:48:25 +0800