--- layout: fc_discuss_archives title: Message 122 from Frama-C-discuss on November 2013 ---
Hi Xiao-lei, 2013/11/27 Xiao-lei Cui <x_cui at hotmail.com>: > extern void g(void); > extern int h(void); > > int f(void){ > //@ asserts pre-condition-of (g) ? > g(); > //@ asserts post-condition-of (g) ? > return (h()); /*how to specify the return value here?*/ > } > I see no other way than using a temporary variable: int res_tmp; [...] res_tmp = h(); //@ assert something on res_tmp; return res_tmp; Best regards, david