From 8f750f2d4d68192d92b6363490e8a8e577f55584 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 5 Jun 2020 16:43:43 +0200 Subject: 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 --- test/clightgen/annotations.c | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 test/clightgen/annotations.c (limited to 'test') 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); +} -- cgit