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] Internal state represented by ghost variable not provable

  • Subject: [Frama-c-discuss] Internal state represented by ghost variable not provable
  • From: frank at dordowsky.de (Frank Dordowsky)
  • Date: Mon, 28 Apr 2014 20:58:59 +0200 (CEST)
Hello Virgile,
thanks for this interesting hint. I have seen a similar approach in this 
report, however, without using an automaton:

Burghardt, J.; Carben, A.; Gerlach, J.; Pohl, H. & Voellinger, K.
ACSL By Example. Towards a Verified C Standard Library
Fraunhofer FIRST, 2013

I think it is a rather elaborate way to specify a seemingly simple
behaviour. Moreover, in my real example I am working at, this
behaviour is only part of a more complex specification: an erroneous
situtation must occur three times in a row before an error code is
returned, otherwise a default value is given back, or the proper value
calculated and returned.

I will first stick with Anne's proposal. When I have my specification
got proper and there is still time left I will have a closer look at the
Aorai manual.

Frank