Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] ACSL annotation for making function calls

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