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: haihaoshen at gmail.com (haihao shen)
  • Date: Tue, 31 May 2011 23:13:59 +0800
  • In-reply-to: <BANLkTi=8Gx4aa-xAt9YkyqoPcdRp_FPjJQ@mail.gmail.com>
  • References: <BANLkTikWHFYdUiCqN5B+Ec2EjQCtQyEFUw@mail.gmail.com> <BANLkTi=8Gx4aa-xAt9YkyqoPcdRp_FPjJQ@mail.gmail.com>
Hi Julien,

Thanks for your quick reply. Yeah, I would like to construct a plugin to get
ACSL specification per function (extract ACSL specification separately).
Your sample code really helped me out and I configured it as a standalone
plugin. Thanks again!

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). Also,
I would like to know whether there are other utility function to handle
predicate or logic.

==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)>)

Best,
Haihao
On Tue, May 31, 2011 at 10:48 PM, Julien Signoles <julien.signoles at gmail.com
> wrote:

> Hello,
>
>  2011/5/31 haihao shen <haihaoshen at gmail.com>
>
>>
>> This is Haihao and I am a newer to OCaml and Frama-C.
>>
>
> You're welcome!
>
>
>> I would like to get the ACSL specification per function. Say you have such
>> an example:
>>
>> /*@
>>   @ require (x >0 && y>0);
>>   @ ensure (\result >= x || \result >=y);
>>   @*/
>>
>> int max(int x, int y)
>> {
>>     if(x>=y) return x;
>>     else return y;
>> }
>>
>>  /*@
>>   @ require (x >0 && y>0);
>>   @ ensure (\result >= x || \result >=y);
>>   @*/
>>
>> int min(int x, int y)
>> {
>>     if(x>=y) return y;
>>     else return x;
>> }
>>
>> For funciton max and min, I would like to extract ACSL
>> specification seperately. I constructed a skeleton according to
>> http://forge.ocamlcore.org/docman/view.php/77/132/framac2011.pdf, but I
>> cannot find a way for my purpose. You are also the developer for Frama-C,
>> and I am wondering whether you could give me some suggestion.
>>
>
> Thanks to the link above, I guess you send me this mail directly from
> forge.ocamlcore.org. Actually there is a public mailing list dedicated to
> Frama-C (in Cc) and you should use it in order to have more answers more
> quickly.
>
> About your question:
>
> 1) Your ACSL specification is incorrect since the keywords are "requires"
> and "ensures" (and not "require" and "ensure"). You could see that by
> running frama-c on your C file:
> =====
> frama-c minmax.c
> [kernel] preprocessing with "gcc -C -E -I.  minmax.c"
> b.c:2:[kernel] user error: unsupported clause of name 'require' in
> annotation.
> [kernel] user error: skipping file "minmax.c" that has errors.
> [kernel] error occurring when exiting Frama-C: stopping exit procedure.
>          Frama-C aborted because of invalid user input.
> =====
>
> 2) I don't really understand what you mean by "extract ACSL specification
> separately". As you follow the slides I present at the OCaml Users Meeting,
> I guess you would like to write an OCaml plug-in.
>
> For instance, the following plug-in pretty prints the specification of the
> function "max":
> ==== spec.ml ====
> include Plugin.Register
>   (struct
>     let name = "Specification printer"
>     let shortname = "spec"
>     let help = "Pretty print the specification of the function `max'"
>    end)
>
> let main () =
>   Ast.compute ();
>   result "%a" !Ast_printer.d_funspec
>     (Kernel_function.get_spec (Globals.Functions.find_by_name "max"))
>
> let () = Db.Main.extend main
> ==========
>
> $ frama-c -load-script spec.ml minmax.c
> [kernel] preprocessing with "gcc -C -E -I.  minmax.c"
> [spec] requires x > 0 ? y > 0;
>        ensures \result ? \old(x) ? \result ? \old(y);
>
> Do not hesitate to precise your need,
> hope this helps,
> Julien
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110531/69ecaad1/attachment.htm>