1 files changed, 13 insertions, 0 deletions
diff --git a/extern.c b/extern.c
new file mode 100644
index 0000000..186596d
--- /dev/null
+++ b/extern.c
@@ -0,0 +1,13 @@
+#include <stdio.h>
+
+unsigned i = 1;          /*@\label{line:decl-i-1}*/
+
+int main(void) {
+  unsigned i = 2;        /* A new object *//*@\label{line:decl-i-2}*/
+  if (i) {
+    extern unsigned i;   /* An existing object *//*@\label{line:decl-i-3}*/
+    printf("%u\n", i);   /* prints 1 */
+  } else {
+    printf("%u\n", i);   /* prints 2 */
+  }
+}