#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;
}