clightgen: fix the printing of annotations

The printing of EF_annot and EF_annot_val was missing the extra "kind"
parameter introduced in commit 6a010b4.

Also: the automatic translation of annotations into Coq assertions
was confusing and prevented other uses of __builtin_annot statements
in conjunction with clightgen.  I believe it was never used.
This commit removes this translation.

Closes: #360

1 files changed, 6 insertions, 0 deletions

diff --git a/test/clightgen/annotations.c b/test/clightgen/annotations.c
new file mode 100644
index 00000000..56fc1700
--- /dev/null
+++ b/test/clightgen/annotations.c
@@ -0,0 +1,6 @@
+int f(int x, long y)
+{
+  __builtin_ais_annot("x is %e1, y is %e2", x, y);
+  __builtin_annot("x is %1, y is %2", x, y);
+  return __builtin_annot_intval("x was here: %1", x);
+}