--- layout: fc_discuss_archives title: Message 43 from Frama-C-discuss on April 2014 ---
On Wed, 30 Apr 2014, Virgile Prevosto wrote: You are absolutely right, the new specification is different, and on purpose. I could not prove the orignial specification because inp is changed during execution of foo() due to a call to a lower level function not visible at specification level. So it is intended. Frank > Hello, > > 2014-04-29 21:27 GMT+02:00 Frank Dordowsky <frank at dordowsky.de>: > > Your new specification is very different from your original one: > /*@ assumes inp < 0; > ensures \result == 'n'; */ > is equivalent to > /*@ ensures \at(inp,Old) < 0 ==> \result == 'n'; */ > > Unless inp is not modified by the call to foo (which is not the case > here since you want inp to reflect an internal state which is modified > at each call if I recall correctly), > in the post state (the one in which the ensures clause is evaluated), > inp != \at(inp, Old). > >> I also tried model variables because they are advocated in the ACSL >> specification 1.7 as means to "...provide abstract specifications to >> functions whose concrete implementation must remain private". >> Unfortunately, it seems that model variables are not yet implemented in >> Fluorine. > > Yes, at the moment only model fields (for types) are implemented in > the kernel, and I'm not completely sure of their level of support in > WP and Jessie. > > Best regards, > -- > E tutto per oggi, a la prossima volta > Virgile > Frank Dordowsky S?ntisstr. 37 81825 M?nchen E-Mail: frank at dordowsky.de