--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on October 2011 ---
Hi everybody, Yes, WP and Jessie have not exactly the same capabilities. We are currently writing a tutorial on WP using exactly the algorithms of "ACSL By Example", with work-arounds and hints when necessary. Previous work ? Fraunhoffer FIRST already reveal precious hints for improving WP there and there. As a first hint list of 'hints' to validate "ACSL By Example" with WP: - fullfill all missing "assigns" clauses, eg. by including local variables modified during loop steps (1) - use option -wp-rte to generate proof obligations against runtime errors (default in Jessie, not in WP) - increase Alt-Ergo's timeout in presence of user-defined precidates, or use Z3 (2) - using -wp-split sometimes help You should then manage to validate most of algorithms from "ACSL By Example" with these hints. Regards, Loic Correnson. (1) Actually, assigns clause must completely refer *all* assigned location, not only those allocated on the heap. The memory model of Jessie is sometimes able to reason with incomplete assigns clause that do not mention local variables, provided their address is not taken (probably). This a convenient extension, but not correct in ACSL sense. In Frama-C we are developping a plug-in to infer those missing assigns clause, but it is not distributed yet. (2) This problem is due to non-optimal triggers for Alt-Ergo. It is already corrected for next release.