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

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



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