Add support for uninterpreted predicates in ACSL

[zafer-esen]

Add Uninterpreted Predicates to ACSL

This PR introduces support for uninterpreted predicates in the ACSL (ANSI/ISO C Specification Language) handling pipeline of TriCera. The work is based on the thesis:

Adding Uninterpreted Predicates to the ANSI/ISO C Specification Language
Martin Nilsson — KTH Royal Institute of Technology
Full text PDF: diva2:1957907
Record link: https://kth.diva-portal.org/smash/record.jsf?pid=diva2:1957907

Abstract: Formal verification of a C programme can be done (e.g.) by specifying the components of the programme in the ANSI/ISO C Specification Language (ACSL). To ease such work, formal verification tools can provide useful additional features. One potentially-useful feature that ACSL does not have is uninterpreted predicates. In this thesis, we looked at an existing implementation of ACSL based on constrained Horn clauses (CHCs), namely TriCera. We extended this implementation to support uninterpreted predicates based on existing support for the functionality in the underlying tool. The resulting implementation is able to solve for uninterpreted predicates in ACSL contracts.

The work in this PR is contributed by Martin Nilsson [email protected], and is being committed and submitted by me on their behalf.