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
- Prev by Date: [Frama-c-discuss] Behavior specification with ghost variables
- Next by Date: [Frama-c-discuss] Error on using pp-annot
- Previous by thread: [Frama-c-discuss] Behavior specification with ghost variables
- Next by thread: [Frama-c-discuss] alignment assumptions?