Why does the dependence graph of this scanf()-using program by Frama-C look like this?

Question

I use the Frama-C tool to generate the dependence graph of this program(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;
    }

The command is:

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

The result is My question is why the statments "m=m*i;"，"m=m%10000" do not map to nodes. The result does not seem right,because there are three loops in the code.

Answer 1

A slicer for C programs only works in practice if its defined goal is to preserve defined executions, and the slicer is allowed to change undefined executions.

Otherwise, the slicer would be unable to remove a statement such as x = *p; as soon as it is unable to determine that p is a valid pointer at that point, even if it knows that it does not need x, just because if the statement is removed, executions where p is NULL at that point are changed.

Frama-C does not handle complex library functions such as scanf(). Because of this, it thinks that local variable n is used without being initialized.

Type frama-c -val main.c You should get a warning like:

main.c:10:[kernel] warning: accessing uninitialized left-value:
               assert \initialized(&n);
...
[value] Values for function main:
      NON TERMINATING FUNCTION

The word assert means that Frama-C's option -val is unable to determine that all executions are defined, and "NON TERMINATING FUNCTION" means that it is unable to find a single defined execution of the program to continue from.

The undefined use of an uninitialized variable is the reason the PDG removes most statements. The PDG algorithm thinks it can remove them because they come after what it thinks is an undefined behavior, the first access to variable n.

I modified your program slightly to replace the scanf() call with a simpler statement:

#define EOF (-1)
int unknown_int();

int scan_unknown_int(int *p)
{
  *p = unknown_int();
  return unknown_int();
}

int main()
{
  int n,i,m,j;
  while(scan_unknown_int(&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;
}

and I got the PDG below. It looks complete as far as I can tell. If you know better layout programs than dot but that accept the dot format, this is a good chance to use them.

Note that the condition of the outmost while became tmp != -1. The nodes of the graph are the statements of an internal normalized representation of the program. The condition tmp != -1 has a data dependency to the node for the statement tmp = unknown_int();. You can display the internal representation with frama-c -print main.c, and it will show that the outmost loop condition has been broken into:

  while (1) {
    int tmp;
    tmp = scan_unknown_int(& n);
    if (! (tmp != -1)) { break; }

This helps, among other things, the slicing to remove only the parts of a complex statement that can be removed instead of having to keep the entire complex statement.