Added Duet5LC configuration

1 files changed, 217 insertions, 0 deletions

diff --git a/src/ecv.h b/src/ecv.h
new file mode 100644
index 00000000..efb6f7bf
--- /dev/null
+++ b/src/ecv.h
@@ -0,0 +1,217 @@
+/* Header file for supporting Escher C Verifier annotations in C and C++ files
+ * Copyright(c) 2016 Escher Technologies Limited
+ * Escher Technologies Limited permits free use and distribution of this file for the purpose of annotating C and C++ programs
+ * in a manner compatible with Escher C Verifier, subject to the following conditions:
+ * 1. If you make any alterations to this file, you must make this clear by adding additional comments,
+ *    and you must reproduce these conditions and copyright notice in full.
+ * 2. No warranty or support is provided except in accordance with the terms of a paid-up support & maintenance agreement
+ *    between the user and Escher Technologies Limited.
+ *
+ * For documentation of the eCv keywords, see the eCv Reference Manual at http://eschertech.com/support/perfect_developer_self_help.php
+ * For examples of their use, see http://eschertech.com/articles/index.php
+ */
+
+#if !defined(__ECV_H_INCLUDED__)
+
+#define __ECV_H_INCLUDED__
+
+#ifdef __ECV__
+#pragma ECV noverify
+#endif
+
+/* Define the "normal" versions of the eCv keywords.
+ * If any of these clash with identifiers in the user program, you can #undef them after including this file. */
+
+#define any				_ecv_any
+#define array			_ecv_array
+#define assert			_ecv_assert
+#define assume			_ecv_assume
+#define decrease		_ecv_decrease
+#define disjoint		_ecv_disjoint
+#define exists			_ecv_exists
+#define forall			_ecv_forall
+#define ghost  			_ecv_ghost
+#define holds			_ecv_holds
+#define idiv			_ecv_idiv
+#define imod			_ecv_imod
+#define in				_ecv_in
+#define integer			_ecv_integer
+#define invariant		_ecv_invariant
+#define keep			_ecv_keep
+#define let				_ecv_let
+#define maxof			_ecv_maxof
+#define minof			_ecv_minof
+#define min_sizeof		_ecv_min_sizeof
+#define not_null		_ecv_not_null
+#define null			_ecv_null
+#define old				_ecv_old
+#define out				_ecv_out
+#define over			_ecv_over
+#define post			_ecv_post
+#define pre				_ecv_pre
+#define result			_ecv_result
+#define returns			_ecv_returns
+#define some			_ecv_some
+#define spec			_ecv_spec
+#define that			_ecv_that
+#define those			_ecv_those
+#define value			_ecv_value
+#define writes			_ecv_writes
+#define yield			_ecv_yield
+#define zero_init		_ecv_zero_init
+
+#if defined(__ECV__) || !defined(__STDC_VERSION__) || (__STDC_VERSION__ < 19901L)
+# define restrict		_ecv_restrict
+#endif
+
+#if defined(__cplusplus)
+# define early			_ecv_early
+# define from			_ecv_from
+# if defined(__ECV__) || (__cplusplus < 201103L)
+// The C++'11 final, nullptr and override keywords are available whenever processing C++ with eCv
+#  define final			_ecv_final
+#  define nullptr		_ecv_nullptr
+#  define override		_ecv_override
+# endif
+#endif
+
+#if defined(__ECV__)
+
+/************************ The following definitions are only active when running eCv **********************/
+
+#if defined(_MSC_VER)
+
+/******************** Definitions for Microsoft compilers *********************/
+
+/* Define Microsoft compiler-specific keywords as expanding to nothing */
+#define __declspec(_x)
+#define __w64
+#define __inline		inline
+#define __cdecl
+#define __fastcall
+#define __stdcall
+
+#if _MSC_VER >= 1400
+
+/ * Microsoft file crtdefs.h (which is included by nearly everything else) contains some references to types not defined there.
+ * To avoid problems, we include crtdefs.h here along with the files that define the missing types. */
+#define __STDC_WANT_SECURE_LIB__	(0)	/* need this to undo some inline declarations that don't compile in eCv */
+#define _CRT_SECURE_NO_WARNINGS		(1)
+#include "crtdefs.h"
+#include "locale.h"						/* defines "struct lconv" */
+struct __lc_time_data { int _x; };		/* this is defined only in the CRT source */
+struct threadmbcinfostruct { int _x; };	/* this is defined only in the CRT source */
+#endif
+
+#endif		/* end Microsoft compiler specific */
+
+#if defined(__GNUC__)
+
+/*********************** Definitions for Gnu Compiler Collection C and C++ compilers ********************/
+
+#define __inline__		inline
+#define __restrict__	_ecv_restrict
+
+/* Hide gcc __attribute__ keyword from eCv.
+ * WARNING: some header files (e.g. _mingw.h) may "#undef __attribute__", which undoes this. */
+#define __attribute__(_x)
+
+/* The following are needed to handle gcc's implementation of variable argument lists */
+typedef struct __builtin_va_list__ { int x; } __builtin_va_list;
+extern void __builtin_va_start(__builtin_va_list, const char*);
+extern void __builtin_va_end(__builtin_va_list);
+
+#endif		/* end gcc specific */
+
+#if defined HI_TECH_C
+
+/****************************** Definitions for HiTech C compilers ********************************/
+
+#define bit bool			/* define HiTech bit type as equivalent to bool */
+
+/* Define the HiTech C extra type qualifiers */
+#define interrupt		_ecv_interrupt	/* functions may be flagged as interrupt routines */
+#define persistent
+#define near
+#define bank0
+#define bank1
+#define bank2
+#define bank3
+#define eeprom
+#define __interrupt		_ecv_interrupt	/* functions may be flagged as interrupt routines */
+#define __persistent
+#define __near
+#define __bank0
+#define __bank1
+#define __bank2
+#define __bank3
+#define __eeprom
+
+#define asm(_x)				/* hide assembler from eCv */
+
+#endif		/* end HiTech compiler specific */
+
+#if defined __IAR_SYSTEMS_ICC__
+
+/****************************** Definitions for IAR C/C++ compilers ********************************/
+
+/* Define the IAR extra keywords */
+#define __cc_version1
+#define __cc_version2
+#define __data16
+#define __data20
+#define __interrupt		_ecv_interrupt	/* functions may be flagged as interrupt routines */
+#define __intrinsic
+#define __monitor
+#define __no_init
+#define __no_pic
+#define __noreturn
+#define __persistent
+#define __ramfunc
+#define __raw
+#define __regvar
+#define __root
+#define __ro_placement
+#define __save_reg20
+#define __task
+
+#endif		/* end IAR compiler specific */
+
+/**************************** End of compiler-specific definitions ***************************/
+
+#else		/* not running eCv */
+
+/* Define eCv macros as expanding to nothing */
+#define _ecv_array
+#define _ecv_assert(_x)		((void)0)
+#define _ecv_assume(_x)
+#define _ecv_change(_x)
+#define _ecv_decrease(_x)
+#define _ecv_ghost(_x)
+#define _ecv_interrupt
+#define _ecv_invariant(_x)
+#define _ecv_keep(_x)
+#define _ecv_not_null(_x)	(_x)
+#define _ecv_null
+#define _ecv_out
+#define _ecv_pass			((void)0)
+#define _ecv_post(_x)
+#define _ecv_pre(_x)
+#define _ecv_restrict
+#define _ecv_returns(_x)
+#define _ecv_spec
+#define _ecv_writes(_x)
+
+#if defined(__cplusplus)
+#define _ecv_early
+#define _ecv_final
+#define _ecv_from
+#define _ecv_nullptr		(0)
+#define _ecv_override
+#endif
+
+#endif		/* end "if defined(__ECV__) ... else ..." */
+
+#endif		/* end header guard */
+
+/* End of file */