--- layout: fc_discuss_archives title: Message 44 from Frama-C-discuss on March 2011 ---
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