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] Fwd: One question to parse ACSL specification per function

  • Subject: [Frama-c-discuss] Fwd: One question to parse ACSL specification per function
  • From: Julien.Signoles at cea.fr (Julien Signoles)
  • Date: Tue, 31 May 2011 16:52:46 +0200
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