--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on April 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Internal state represented by ghost variable not provable



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