--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on May 2011 ---
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>