--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on December 2013 ---
Hello Xiao-lei, Le 12/12/2013 07:25, Xiao-lei Cui a ?crit : > I often struggle with annotating function calls in ACSL, due to my > inexperience. I am not sure if it is necessary to reference the pre and > post conditions of the callee(e.g. bar1, bar2 in the code below) in the > annotation for the caller. > For instance , given the code below, what is the proper way to > annotate function foo()? Your question is too generic to be able to give a useful answer. The generic answer would be: put in foo() contract what you need to prove about foo(). Then extend it depending on what bar1() and bar2() provide. If you use bar1() and bar2() into foo(), regarding preconditions of barX() functions two cases can occur: * foo() code ensures the preconditions are valid (e.g. through a if before calling barX()) ; * Or you put in foo() precondition enough things to ensure preconditions of barX() are satisfied. Regarding postcondition, most of the time bar1() and bar2() postconditions will help you proof foo(). But how to spread the verification effort between foo(), bar1() and bar2() really depend on the specific structure of a given code. Best regards, david