aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/SMTChecker.cpp
Commit message (Expand)AuthorAgeFilesLines
* [SMTChecker] Unknown answer for constant condition check should not do anythingLeonardo Alt2018-11-261-0/+4
* Error message stays in the SMTCheckerLeonardo Alt2018-11-231-0/+9
* Inject SMTLIB2 queries and responses via standard-json-io.chriseth2018-11-231-2/+2
* [SMTChecker] Refactor setZeroValue and setUnknownValueLeonardo Alt2018-11-221-4/+14
* [SMTChecker] Add FunctionSort and refactors the solver interface to create va...Leonardo Alt2018-11-221-4/+9
* Introduce namespace `langutil` in liblangutil directory.Christian Parpart2018-11-221-0/+1
* Isolating files shared between Yul- and Solidity language frontend.Christian Parpart2018-11-221-1/+1
* [SMTChecker] Refactor smt::Sort and its usageLeonardo Alt2018-11-211-2/+2
* [SMTChecker] Support bound function callsLeonardo Alt2018-11-191-0/+12
* [SMTChecker] Implement uninterpreted functions and use it for blockhash()Leonardo Alt2018-11-151-3/+19
* Add Scanner function that prints source based on SourceLocationLeonardo Alt2018-11-131-1/+3
* Grouping of symbolic variables in the same file and support to FixedBytesLeonardo Alt2018-10-251-2/+0
* Merge pull request #5272 from ethereum/smt_special_varschriseth2018-10-241-18/+97
|\
| * Add gasleft constraint and use full member access nameLeonardo Alt2018-10-231-6/+21
| * [SMTChecker] Support msg.*, tx.*, block.*, gasleft and blockhashLeonardo Alt2018-10-191-18/+82
* | 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-181-44/+19
* Refactor SymbolicAddressVariable and SymbolicVariable allocationLeonardo Alt2018-10-171-3/+3
* Consistent renaming of 'counters' and 'sequence' to 'index'Leonardo Alt2018-10-171-29/+29
* [SMTChecker] Refactoring typesLeonardo Alt2018-10-171-28/+37
* Merge pull request #5209 from ethereum/smt_ssa_refactorchriseth2018-10-151-1/+1
|\
| * Refactor SSAVariable such that it only uses Type and not DeclarationLeonardo Alt2018-10-151-1/+1
* | [SMTChecker] Inline calls to internal functionsLeonardo Alt2018-10-151-64/+219
|/
* 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-301-2/+0
* Split IntegerType into IntegerType and AddressType.Daniel Kirchner2018-09-051-1/+4
* SMT: do not crash on referencing MagicVariableDeclarationAlex Beregszaszi2018-08-081-2/+8
* 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
* [SMTChecker] Add CheckResult::CONFLICTINGLeonardo Alt2018-07-271-0/+5
* [SMTChecker] SMTPortfolio: use all SMT solvers availableLeonardo Alt2018-07-271-15/+2
* 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
* Code, Changelog, ReleaseChecklist: Fix typos.Cryptomental2018-07-111-1/+1
* Refactoring Declaration -> VariableDeclaration (more precise)Leonardo Alt2018-06-121-26/+25
* Review commentsLeonardo Alt2018-06-121-8/+6
* Refactoring how storage and local variables are managed.Leonardo Alt2018-06-121-28/+26
* Bool variables should not allow arithmetic comparisonLeonardo Alt2018-05-171-5/+1
* [SMTChecker] Declaring all state vars before any function is visitedLeonardo Alt2018-05-151-2/+13
* [SMTChecker] Support to integer and Bool storage varsLeonardo Alt2018-05-151-4/+29
* Revert "BREAKING: Bool variables should not allow arithmetic comparison"chriseth2018-05-021-1/+5
* Bool variables should not allow arithmetic comparisonLeonardo Alt2018-04-271-5/+1
* [SMTChecker] Remove 'information is erase' message for if-elseLeonardo Alt2018-04-191-9/+9
* [SMTChecker] Using solUnimplementedAssert instead of solAssert when applicableLeonardo Alt2018-04-181-2/+2
* [SMTChecker] Integration with CVC4Leonardo Alt2018-04-171-0/+4
* [SMTChecker_Bool] Fix PR review comments: method renaming and solAssertLeonardo Alt2018-03-131-7/+8
* [SMTChecker_Bool] Fix PR comments; Add support to gt, ge, lt, le. and tests.Leonardo Alt2018-03-131-16/+32
* [SMTChecker] Support to Bool variablesLeonardo Alt2018-03-131-1/+1
* Supported types listed in SSAVariableLeonardo Alt2018-03-011-2/+2
* Integer min and max values placed under SymbolicIntVar instead of SMTCheckerLeonardo Alt2018-03-011-11/+3
* [SMTChecker] A little refactoring on SSA varsLeonardo Alt2018-03-011-46/+35
* [SMTChecker] Variables are merged after branches (ite variables)Leonardo Alt2018-01-051-7/+25
* [SMTChecker] Fix typo in the code (satisifable->satisfiable)Leonardo Alt2017-12-191-6/+6
* [SMTChecker] Helper functions to add an expression to the solver conjoined wi...Leonardo Alt2017-12-141-5/+15
* [SMTChecker] Keep track of current path conditionsLeonardo Alt2017-12-141-8/+27
* Fix expression creation problems.chriseth2017-11-301-19/+30
* Fix signed division.chriseth2017-11-301-2/+16
* Unary operators and division.chriseth2017-11-301-56/+135
* Fix problem with non-value-typed variables.chriseth2017-11-221-13/+13
* For loop.chriseth2017-11-221-0/+42
* Check for conditions being constant.chriseth2017-11-221-26/+87
* Tests.chriseth2017-11-221-5/+0
* Track usage of variables.chriseth2017-11-221-62/+68
* Handle branches.chriseth2017-11-221-54/+78
* Rename variables in SMT checker.chriseth2017-10-181-9/+9
* SMT should not crash on typecast/structsAlex Beregszaszi2017-10-051-0/+10
* Review changes.chriseth2017-08-231-11/+11
* Use experimental feature pragma for SMT checker.chriseth2017-08-231-6/+1
* Partial support for if statements.chriseth2017-08-231-15/+94
* Format numbers more nicely.chriseth2017-08-231-11/+25
* Refactor Z3 read callback.chriseth2017-08-231-3/+24
* Insert abstraction layer.chriseth2017-08-231-26/+27
* Prepare build system for Z3.chriseth2017-08-231-0/+3
* Cleanup.chriseth2017-08-231-4/+443
* z3 conditionschriseth2017-08-231-0/+36
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-15 21:47:17 +0800