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] Frama-c-discuss Digest, Vol 34, Issue 12

  • Subject: [Frama-c-discuss] Frama-c-discuss Digest, Vol 34, Issue 12
  • From: Julien.Signoles at cea.fr (Julien Signoles)
  • Date: Fri, 18 Mar 2011 11:49:26 +0100
  • In-reply-to: <AANLkTinFA=3g2KBza3Uo+2VMRcT3i4BBXhsm9Pv0prGQ@mail.gmail.com>
  • References: <mailman.69.1300273245.28543.frama-c-discuss@lists.gforge.inria.fr> <AANLkTinFA=3g2KBza3Uo+2VMRcT3i4BBXhsm9Pv0prGQ@mail.gmail.com>
Hello Xavier,

Le 16/03/2011 16:56, xavier kauffmann a ?crit :
> On Wed, Mar 16, 2011 at 12:00 PM,
> <frama-c-discuss-request at lists.gforge.inria.fr
> <mailto:frama-c-discuss-request at lists.gforge.inria.fr>> wrote:
>
>     When replying, please edit your Subject line so it is more specific
>     than "Re: Contents of Frama-c-discuss digest..."

Please follow this statement and do not include all the digest in your 
message, but the part you are talking about.

>     Regarding the "if it is not related to it, shouldn't the value
>     analysis be able to provide a value or range for this expression?"
>     part of your question: of course, it can provide the value of an
>     unrelated expression. If your program has a thousand globals, the
>     value of each global at each statement is saved just in case you later
>     want to inspect the value of that variable at that program point.
>
> Would an ocaml script be able to get this information?

Yes it would be. This information is available for any user through the 
Frama-C GUI anyway.

> If so how much knowledge of ocaml would it require?

More OCaml knowledge you have, more quickly you will develop your 
plug-in and more robust/bug free/... your plug-in will be. That is not 
specific to OCaml and Frama-C though ;-).

I think you have to become quite fluent in OCaml for writing a 
"real-world" plug-in, but there was at least one person who learns OCaml 
by writing a Frama-C plug-in.

> Could you please give some hint about which FramaC api should be used?

The API of the value analysis is the module Db.Value.

>      > when I was hoping for something like
>      > bar ? [--..--] - {1234}
>      > based on the evaluation of bar at the toto = 1 and toto = 3 lines
>      > Is there a way to get these exclusions from the value analysis?
>
>     Well, you may have noticed that "[--..--] - {1234}" is not in the
>     documented list of formats in which the value analysis can display
>     sets of values. However, you may get the sets [-2^31 .. 1233] and
>     [1235 .. 2^31-1] programmatically, provided you are willing to insert
>     an annotation to guide the value analysis.
>
> Could you please provide an example?

Consider the program a.c below (your initial example):

=== a.c ===
int main(int bar)
{
   int toto;

   // see value analysis manual, section 7.1.2
   /*@ assert bar <= 1234 || bar > 1234; */
   if (bar == 1234)
   {
     toto = 0;
   }
   else
   {
     toto = 1;
     toto = 2; /* statement 7 */
     toto = 3;
   }
   return toto;
}
===========

You can write the following OCaml script. It is compatible with Frama-C 
Carbon-20110201. It is quite hackish since it uses the internal id of 
statements for finding one of interest (toto = 2;) and the fact that the 
main function has only one formal 'bar'.

=== a.ml ===
(* See plug-in Dev Guide for details about this functor application *)
module L =
   Plugin.Register
     (struct
       let name = "AAA"
       let shortname = "AAA"
       let help = "print formal `bar' at stmt with id 7"
      end)

let print_superposed_states states =
   (* statement 7 is [toto = 2]; shown by frama-c -kernel-debug 1.
      Usually one finds the right statement(s) in an other way depending 
on what
      is your case study *)
   let stmt, kf = Kernel_function.find_from_sid 7 in
   let bar = match Globals.Functions.get_params kf with
     | [ v ] -> v
     | [] | _ :: _ :: _ ->
       assert false (* only the formal 'bar' in the example *)
   in
   let set = Cil_datatype.Kinstr.Hashtbl.find states (Cil_types.Kstmt 
stmt) in
   State_set.iter
     (fun m ->
       let v =
	Relations_type.Model.find
	  ~conflate_bottom:true ~with_alarms:CilE.warn_all_mode
	  m
	  (Locations.loc_of_varinfo bar)
       in
       L.result "in one state, values of bar at stmt 7 are: %a"
	Cvalue_type.V.pretty v)
     set

let () =
   Db.Value.Record_Value_Superposition_Callbacks.extend
     (fun (_callstack, states) -> print_superposed_states states)
========

> Will it require some additional command line options?

$ frama-c -load-script a.ml -val -slevel 2 a.c
<...>
[AAA] in one state, possible values of bar at stmt 7 are: [1235..2147483647]
[AAA] in one state, possible values of bar at stmt 7 are: 
[-2147483648..1233]
<...>

Hope this helps,
Julien