aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/SMTChecker.h
Commit message (Collapse)AuthorAgeFilesLines
* Sort includes in libsolidity/formalLeonardo Alt2018-12-181-3/+1
|
* Clear all mapping knowledge after array variable assignmentLeonardo Alt2018-12-141-1/+9
|
* [SMTChecker] Support to mappingLeonardo Alt2018-12-141-1/+4
|
* [SMTChecker] Use SymbolicFunctionVariable for uninterpreted functionsLeonardo Alt2018-12-111-12/+12
|
* Inject SMTLIB2 queries and responses via standard-json-io.chriseth2018-11-231-1/+6
|
* [SMTChecker] Refactor setZeroValue and setUnknownValueLeonardo Alt2018-11-221-0/+2
|
* [SMTChecker] Add FunctionSort and refactors the solver interface to create ↵Leonardo Alt2018-11-221-1/+1
| | | | variables
* Introduce namespace `langutil` in liblangutil directory.Christian Parpart2018-11-221-9/+14
| | | | | | | 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-221-1/+1
|
* Merge pull request #5466 from ethereum/smt_refactor_sort_patch1Alex Beregszaszi2018-11-211-1/+1
|\ | | | | [SMTChecker] Refactor smt::Sort and its usage
| * [SMTChecker] Refactor smt::Sort and its usageLeonardo Alt2018-11-211-1/+1
| |
* | Removing redundant virtual from override function declarationmordax2018-11-211-18/+18
|/ | | | | | Remove trailing whitespace Remove changelog change
* [SMTChecker] Implement uninterpreted functions and use it for blockhash()Leonardo Alt2018-11-151-0/+6
|
* Add Scanner function that prints source based on SourceLocationLeonardo Alt2018-11-131-1/+4
|
* Grouping of symbolic variables in the same file and support to FixedBytesLeonardo Alt2018-10-251-1/+1
|
* [SMTChecker] Support msg.*, tx.*, block.*, gasleft and blockhashLeonardo Alt2018-10-191-6/+10
|
* [SMTChecker] Refactor expressions such that they also use SymbolicVariableLeonardo Alt2018-10-181-2/+1
|
* Consistent renaming of 'counters' and 'sequence' to 'index'Leonardo Alt2018-10-171-13/+13
|
* [SMTChecker] Refactoring typesLeonardo Alt2018-10-171-4/+9
|
* [SMTChecker] Inline calls to internal functionsLeonardo Alt2018-10-151-4/+24
|
* Refactoring Declaration -> VariableDeclaration (more precise)Leonardo Alt2018-06-121-12/+12
|
* Review commentsLeonardo Alt2018-06-121-2/+2
|
* Refactoring how storage and local variables are managed.Leonardo Alt2018-06-121-1/+3
|
* [SMTChecker] Declaring all state vars before any function is visitedLeonardo Alt2018-05-151-0/+2
|
* [SMTChecker] Support to integer and Bool storage varsLeonardo Alt2018-05-151-0/+2
|
* [SMTChecker] Remove 'information is erase' message for if-elseLeonardo Alt2018-04-191-1/+1
|
* Integer min and max values placed under SymbolicIntVar instead of SMTCheckerLeonardo Alt2018-03-011-3/+0
|
* [SMTChecker] A little refactoring on SSA varsLeonardo Alt2018-03-011-8/+4
|
* [SMTChecker] Variables are merged after branches (ite variables)Leonardo Alt2018-01-051-6/+12
|
* [SMTChecker] Fix typo in the code (satisifable->satisfiable)Leonardo Alt2017-12-191-2/+2
|
* [SMTChecker] Helper functions to add an expression to the solver conjoined ↵Leonardo Alt2017-12-141-0/+4
| | | | with or implied by the current path conditions
* [SMTChecker] Keep track of current path conditionsLeonardo Alt2017-12-141-0/+9
|
* Fix signed division.chriseth2017-11-301-0/+4
|
* Unary operators and division.chriseth2017-11-301-3/+11
|
* Fix problem with non-value-typed variables.chriseth2017-11-221-1/+3
|
* For loop.chriseth2017-11-221-0/+1
|
* Check for conditions being constant.chriseth2017-11-221-0/+13
|
* Track usage of variables.chriseth2017-11-221-8/+17
|
* Handle branches.chriseth2017-11-221-0/+10
|
* Rename variables in SMT checker.chriseth2017-10-181-2/+2
|
* Review changes.chriseth2017-08-231-6/+6
|
* Partial support for if statements.chriseth2017-08-231-0/+16
|
* Rename read file callback.chriseth2017-08-231-1/+1
|
* Insert abstraction layer.chriseth2017-08-231-2/+2
|
* Cleanup.chriseth2017-08-231-6/+59
|
* z3 conditionschriseth2017-08-231-0/+45
generated by cgit v1.2.3 (git 2.25.1) at 2025-02-08 07:29:09 +0800