--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on May 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] One question to parse ACSL specification per function



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>