16 Commits

Author	SHA1	Message	Date
Rhett Aultman	89b60ffbd4	Refactor error reporting ... This commit introduces ErrorReporter, a utility class which consolidates all of the error logging functionality into a common set of functions. It also replaces all direct interactions with an ErrorList with calls to an ErrorReporter. This commit resolves issue #2209	2017-05-30 07:28:31 -07:00
VoR0220	3f9f725737	Fix licensing headers ... Signed-off-by: VoR0220 <rj@erisindustries.com>	2016-11-23 12:22:33 +01:00
Yoichi Hirai	092e5829d8	formal: ignore pragmas during Why3 code generation ... Fixes #1177	2016-10-11 00:01:29 +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
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	26e5faa038	Handle external effects.	2016-07-13 11:16:00 +02: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	36ba7d11ca	Again some why3 fixes with regards to separators in blocks.	2015-11-25 14:24:00 +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	a957322fd7	Preliminary why3 code output.	2015-10-27 00:49:27 +01:00