--- /dev/null
+#include <stdio.h>
+
+
+extern int __atomic_dec(volatile int* addr);
+
+int main(int argc, const char *argv[])
+{
+ int x = 5;
+
+ while (x > -20) {
+ printf("old_x=%d\n", __atomic_dec(&x));
+ printf("x=%d\n", x);
+ }
+
+ printf ("OK\n");
+ return 0;
+}