--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on May 2010 ---
> 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