Commit Graph
29 Commits
Author SHA1 Message Date
VoR0220 3f9f725737 Fix licensing headers
Signed-off-by: VoR0220 <rj@erisindustries.com>
2016-11-23 12:22:33 +01:00
Rhett Aultman 4524ad0870 Add support for do/while loops
This commit adds support for a standard do <statement> while <expr>;
form of statement.  While loops were already being supported; supporting
a do/while loop mostly involves reusing code from while loops but putting
the conditional checking last.
2016-11-10 07:07:25 -08:00
Yoichi Hirai ab1f4632aa Chack for non-version pragmas 2016-10-11 00:07:11 +02:00
Yoichi Hirai 092e5829d8 formal: ignore pragmas during Why3 code generation
Fixes #1177
2016-10-11 00:01:29 +02:00
Yoichi Hirai 4337e70cca Prepare for leaky exceptions
Now toFormalType() reports errors by exceptions, they will be
sometimes leaked to the wider context.  This commits adds a catch.
2016-09-09 20:15:13 +02:00
Yoichi Hirai ac7c6ae7d2 toFormalType reports errors by an exception
This allows error reporting without passing `ASTNode` to `toFormalType()`
2016-09-09 20:15:08 +02:00
Yoichi Hirai c861cf579d Translate mapping types into Why3 arrays when keys are integers
Even when the keys are signed the translation is supposed to work
because Why3 arrays allow negative indices.
2016-09-09 19:11:15 +02:00
Yoichi Hirai a98edb22e5 Add Address module in the WhyML prelude
In the `--formal` output, this commit adds a module called `Address`,
which defines the address type as unsigned integer type bounded at
2^160-1.
2016-09-07 20:39:23 +02:00
chriseth ce11580988 Merge pull request #1041 from pirapira/typo_and_whitespace
Fix a typo and a whitespace inconsistency
2016-09-07 20:05:30 +02:00
Yoichi Hirai 0a8f0fb051 Append an issue id #1043 to a @todo comment about it 2016-09-07 15:21:02 +02:00
Yoichi Hirai c9b23d9829 Fix a typo and whitespaces 2016-09-07 14:29:01 +02:00
chriseth 345c0f36fb Fix crash when using json compiler with exponentiation. 2016-08-20 03:45:39 +02:00
chriseth 26e5faa038 Handle external effects. 2016-07-13 11:16:00 +02:00
chriseth 656405240e Simplify interface of RationalNumber. 2016-05-10 19:40:37 +02:00
VoR0220 4b749fc333 changed names for Rational Constants and categories 2016-05-09 11:41:02 -05:00
RJ Catalano 9a075458ad initial work for fixed types...potentially needing a constant literal type for this
notation

Rational implemented...trying to figure out exponential

fix for token bug, also quick fix for the wei and seconds

fixed problem with var...probably a conversion problem for fixed in size capabilities

adding fixed type tests

Removing bitshift and regrouping fixed type tests together

size capabilities functioning properly for fixed types

got exponents up and working with their inverse, changed a few of the tests....something is working that likely shouldn't be

slight changes to how to flip the rational negative around...still trying to figure it out

tests added

updated tests

odd differences in trying soltest from solc binary, let me know if you can replicate

test not working for odd reason

fixed test problem with fixed literals...still need a way to log this error

broken up the tests, added some, changed some things in types and began compiler work

moar tests and prepping for rebuilding much of the types.cpp file

further fixing

initial work for fixed types...potentially needing a constant literal type for this
2016-05-09 11:41:02 -05:00
Bob Summerwill a1ce66b304 Fixed Windows warnings 2016-03-18 01:22:15 -07:00
LianaHus 58e07151e3 - inline and assembly keywords added
- some style fixes
2016-03-11 17:49:32 +01:00
chriseth b47d593252 Do not store elements of a contract by AST node type. 2015-11-26 15:37:55 +01:00
chriseth e06768e8b5 Fix MSVC errors and warnings. 2015-11-26 14:47:28 +01:00
chriseth 20542d1623 Style. 2015-11-25 14:24:00 +01:00
chriseth 36ba7d11ca Again some why3 fixes with regards to separators in blocks. 2015-11-25 14:24:00 +01:00
chriseth 10fe0a2434 Style. 2015-11-23 16:30:51 +01:00
chriseth 806507d5c0 addmod and mulmod for why3. 2015-11-23 00:58:17 +01:00
chriseth 82a6ab486d Why3: Direct references to variables using #. 2015-11-23 00:58:17 +01:00
chriseth 12f19fa46b Formal Verification: State variables. 2015-11-19 02:04:33 +01:00
chriseth 34829ae764 Fix problems with statement blocks. 2015-11-11 15:21:01 +01:00
chriseth 56f5d58850 Rename error type. 2015-10-27 17:45:58 +01:00
chriseth a957322fd7 Preliminary why3 code output. 2015-10-27 00:49:27 +01:00