Почему граф зависимостей этой программы, использующей scanf() от Frama-C, выглядит так?

Я использую инструмент Frama-C для создания графа зависимостей этой программы (main.c).

    #include<stdio.h>
    int main()
    {
        int n,i,m,j;
        while(scanf("%d",&n)!=EOF)
        { 
            m=n;
            for(i=n-1;i>=1;i--)
            {   
                m=m*i;
                while(m%10==0)
                {
                     m=m/10;
                }
                m=m%10000;
            }  
            m=m%10;
            printf("%5d -> %d\n",n,m);
        }
       return 0;
    }

Команда:

    frama-c -pdg -dot-pdg main main.c 
    dot -Tpdf main.main.dot -o main.pdf

Результат: Мой вопрос в том, почему статусы «m = m * i;», «m = m% 10000» не сопоставляются с узлами. Результат не кажется правильным, потому что в коде три цикла.