--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on May 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] question about a simple example and jessie



> you can always
> add to the program a ghost variable and ghost statements to make the
> logic of the loop clearer.

A didactic example taking advantage of ghost code can be found pages
74-77 of the library/tutorial "ACSL by Example", for function
remove_copy:

http://www.first.fraunhofer.de/owx_download/acsl-by-example-4_2_1.pdf

Pascal