ESBMC is a SMT-based context-bounded bounded model checker that aims toprovide bit-precise verification of both ANSI-C and C++ programs. Thepresentation will briefly introduce the tool and then show the usage oflibtooling as a frontend for the tool, including the problems we had duringthe development and what we hope for the future. On the first half of the talk, I'll describe the tool and present someexamples of its usage, including the verification of concurrent programs. I'll then focus on the tool's new frontend, which generates the AST of theprogram using clang's libtooling and converts it to an internal format that'sused for the verification. This second half of the presentation will befocused on the development of the C frontend and the yet to be C++ frontend,including how we had to adjust to the libtooling API. The aim of the talk is to present the difficulties that we faced when movingaway from our frontend to clang, including limitations we found during thedevelopment. I'll end the talk with what we hope for the future, as users ofclang, which translates to easier access to some of clang's internals(specially the static analyser).