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

[Frama-c-discuss] Frama-c-discuss Digest, Vol 34, Issue 12



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