hello You could take (and improve/refactor) some obsolete code from https://github.com/bstarynk/bismon and read the below draft report http://www.starynkevitch.net/Basile/bismon-chariot-doc.pdf
I am no more working on that code base. My current open source project is https://github.com/RefPerSys/RefPerSys/ (an inference engine project, GPL licensed) which you could use to test/improve your static analysis part. Be of course aware of https://frama-c.com/ (I was part of that team at www- list.cea.fr before my retirement in nov 2023) regards Regards. -- Basile STARYNKEVITCH <bas...@starynkevitch.net> 8 rue de la Faïencerie 92340 Bourg-la-Reine, France http://starynkevitch.net/Basile & https://github.com/bstarynk