Homework 6: File Property Simulation

Problem

We wish to design an analysis that can check that close is only called if the file is currently open, that open is only called if the file is currently closed, and that the file is definitely closed at the program exit.

In this homework, you are expected to implement a pass to perform an intraprocedural path-sensitive property checking(i.e. file state) for a C program.

• example.c

We assume that

• There is no loop now in the function.
• There is no pointer and function parameter in the source code.

You can generate the bc code by the following command or use the bc code provided in the benchmark section.

• Command: clang -O0 -g -emit-llvm example.c -c -o example.bc (This command applies the existing optimization in LLVM on the final IR so that it may look slightly different from the original program.)

Sample Output

The output of the example.cc is as follows. You should output the file name, final state, and its paths at exit point of program.

• file_example.txt

Benchmark

• Source code
  • testcase_1.c
• BC code
  • Find it on Skeleton.zip

Skeleton