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] One question to parse ACSL specification per function

  • Subject: [Frama-c-discuss] One question to parse ACSL specification per function
  • From: Julien.Signoles at cea.fr (Julien Signoles)
  • Date: Wed, 01 Jun 2011 10:12:05 +0200
  • In-reply-to: <BANLkTikbDRzFe4xcAX1NWHnR+yeFiTEdWw@mail.gmail.com>
  • References: <BANLkTikWHFYdUiCqN5B+Ec2EjQCtQyEFUw@mail.gmail.com> <BANLkTi=8Gx4aa-xAt9YkyqoPcdRp_FPjJQ@mail.gmail.com> <BANLkTikbDRzFe4xcAX1NWHnR+yeFiTEdWw@mail.gmail.com>
Hello,

Le 31/05/2011 17:13, haihao shen a ?crit :
> I have another question on kernel_function (kf) and normal function (f).
> I searched some utility functions in module kernel_function and found
> that for kernel function, the module provides several functions to
> handle detailed specification per function preconditions and
> postconditions. I would like to know whether there is similar function
> to handle normal function (f).

Not directly. Kernel function groups in a single type function 
declarations and function definitions, as well as it provides an easy 
access to its specification. That is not the case of what you call 
"normal" function.

But it is still possible to get the kernel function corresponding to a 
"normal" function and conversely, for instance via their shared varinfo.

Also, I would like to know whether there
> are other utility function to handle predicate or logic.

The Plug-in Development Guide 
(http://frama-c.com/download/frama-c-plugin-development-guide.pdf), even 
if partially out-of-date, explains how Frama-C sources are organized. 
For instance, have a look at Section 5.1.

The full API documentation is also available in html format here: 
http://frama-c.com/download/frama-c-Carbon-20110201_api.tar.gz.

> ==utility function in module kernel_function ==
> let postcondition <javascript:void(0)> kf <javascript:void(0)> =
> Logic_const <javascript:void(0)>.pands <javascript:void(0)>
>      (List <javascript:void(0)>.map <javascript:void(0)> Ast_info
> <javascript:void(0)>.behavior_postcondition <javascript:void(0)>
> (get_spec <javascript:void(0)> kf <javascript:void(0)>).spec_behavior
> <javascript:void(0)>)

Usually, when looking for a function, it is easier to look at the module 
interface than at the module implementation, even if you can improve 
your OCaml skill this last way (only if the implementation is clear 
enough: that is arguably and unfortunately not always the case in Frama-C).

Hope this helps,
Julien