Add support to clightgen for generating Csyntax AST as .v files

As proposed in #404.

This is presented as a new option `-clight` to the existing `clightgen` tool.

Revise clightgen testing to test the Csyntax output in addition to
the Clight output.

1 files changed, 8 insertions, 0 deletions

diff --git a/test/export/annotations.c b/test/export/annotations.c
new file mode 100644
index 00000000..993fa7d0
--- /dev/null
+++ b/test/export/annotations.c
@@ -0,0 +1,8 @@
+int f(int x, long y)
+{
+#if !defined(SYSTEM_macos) && !defined(SYSTEM_cygwin)
+  __builtin_ais_annot("x is %e1, y is %e2", x, y);
+#endif
+  __builtin_annot("x is %1, y is %2", x, y);
+  return __builtin_annot_intval("x was here: %1", x);
+}