aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/SMTChecker.h
Commit message (Expand)AuthorAgeFilesLines
* 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 va...Leonardo Alt2018-11-221-1/+1
* Introduce namespace `langutil` in liblangutil directory.Christian Parpart2018-11-221-9/+14
* 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 usageLeonardo Alt2018-11-211-1/+1
* | Removing redundant virtual from override function declarationmordax2018-11-211-18/+18
|/
* [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 wi...Leonardo Alt2017-12-141-0/+4
* [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 (git 2.34.1) at 2024-11-18 04:47:56 +0800