Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.


[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Silicon] Is it possible to make frama-c return non-zero on timeout/failure?


  • Subject: [Frama-c-discuss] [Silicon] Is it possible to make frama-c return non-zero on timeout/failure?
  • From: tjoppen at acc.umu.se (Tomas Härdin)
  • Date: Sun, 11 Nov 2018 21:24:17 +0100

Hi

Is it possible to make frama-c return a non-zero exit code if it fails
to prove every goal? This would be very useful in a build system. Maybe
it's already possible in recent versions? I'm stuck on Silicon
currently (due to Debian). Searching the manual didn't yield much

The reason is of course the sometimes huge proving times, in my case
when dealing with string concatenation. I get the feeling that putting
each function into its own compilation unit may save some headache. But
of course, this is only useful if it's possible to have a sane build
system!

/Tomas