aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal
Commit message (Expand)AuthorAgeFilesLines
* 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