Adding Basic Support for Function Pointers in TriCera

Sammanfattning: TriCera is a verification tool that encodes programs in a C-like language to a set of Constrained Horn Clauses.  These clauses describe the program states that can be reached when the program is executed.  A solver can then be used to check if the program is safe.  Before this project TriCera did not have any support for function pointers, which are a commonly used construct in C programs. In this report, an algorithm encoding function pointer calls is defined.  The calls are encoded in a way that is similar to how other conditional control flow is encoded.  For each possible callee the function pointer in a call could point to, the algorithm will generate a call to that function in the encoding together with a condition checking if the pointer currently points to the function.   This algorithm is implemented in TriCera together with support for basic function pointer declarations. Test cases are used to check that the implementation works for basic programs. The implementation currently includes support for: basic function pointer declarations, function pointer expressions involving indirection and address operators, and function pointer calls.  With the new additions TriCera is now able to verify basic programs using function pointers. Limitations in the method used to find the set of possible callees and the already existing method for automatic recursion detection prevents some programs from being encoded.  Future work includes: full support for function pointer declarations, a better method for finding the set of possible callees, and a better method for automatic recursion detection.