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] counterexamples through Frama-C WP

  • Subject: [Frama-c-discuss] counterexamples through Frama-C WP
  • From: dcok at grammatech.com (David Cok)
  • Date: Mon, 11 Nov 2013 11:14:26 -0500
I've been successfully using Frama-C WP with alt-ergo, but I do not see 
a mechanism for retrieving concrete counterexample information from the 
back-end SMT solvers (either alt-ergo, or others through Why).

Just in  case I'm missing something, can someone more familiar with WP 
point me to the appropriate options or confirm that reporting 
counterexample information is a feature yet to be implemented?

If the latter, would such a contribution be welcome?

- David