aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/Why3Translator.cpp
Commit message (Expand)AuthorAgeFilesLines
* refactoring functionCallAnnotationdjudjuu2017-05-191-1/+1
* Change references to FunctionType::LocationAlex Beregszaszi2017-03-161-7/+7
* Fix licensing headersVoR02202016-11-231-4/+4
* 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-111-0/+5
* Prepare for leaky exceptionsYoichi Hirai2016-09-101-0/+4
* toFormalType reports errors by an exceptionYoichi Hirai2016-09-101-19/+68
* 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
* Fix a typo and whitespacesYoichi Hirai2016-09-071-1/+1
* Fix crash when using json compiler with exponentiation.chriseth2016-08-201-2/+7
* Handle external effects.chriseth2016-07-131-46/+154
* 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
* Do not store elements of a contract by AST node type.chriseth2015-11-261-10/+5
* Style.chriseth2015-11-251-1/+2
* Again some why3 fixes with regards to separators in blocks.chriseth2015-11-251-19/+24
* Style.chriseth2015-11-231-2/+5
* addmod and mulmod for why3.chriseth2015-11-231-17/+36
* Why3: Direct references to variables using `#`.chriseth2015-11-231-1/+68
* Formal Verification: State variables.chriseth2015-11-191-20/+64
* Fix problems with statement blocks.chriseth2015-11-111-18/+40
* Rename error type.chriseth2015-10-281-1/+1
* Preliminary why3 code output.chriseth2015-10-271-0/+525