--- layout: fc_discuss_archives title: Message 45 from Frama-C-discuss on May 2011 ---
Hello all, Forward from one of my personal email addresses (not allowed to send mails to Frama-C discuss from it): ---------- Message transf?r? ---------- From: Julien Signoles To: haihao shen <haihaoshen at gmail.com <mailto:haihaoshen at gmail.com>> Date: Tue, 31 May 2011 16:48:07 +0200 Subject: Re: One question to parse ACSL specification per function Hello, 2011/5/31 haihao shen <haihaoshen at gmail.com <mailto: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 <http://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 <http://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 <http://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