0

I want to develop a Frama-C-Plugin, where I get the values of the current statement.

With the help of this post Frama-C Plugin development: Getting result of value-analysis I was able to print the values of the statements, but Pointers were not shown the way I need it.

With the help of the comments, I was able to print the whole state (not only the variables of the statement).

Can I combine these two: Get the variables of the statement, but also with pointers dereferenced (the value)?

For example, printing a non-pointer after statement x=1 results in x -> {{ NULL -> {1} }}, while printing a pointer, after a statement like *x=3, results in x -> {{ y -> {0} }} because the 0 is the offset of the variable, but I want to get the value where the pointer points to, in the example 3. The way I want it, would be to get something like that: x -> 3.

Even better would be to get a tuple of (String varname, int value), so I can print it myself.

Community
  • 1
  • 1
Thomas Böhm
  • 1,456
  • 1
  • 15
  • 27
  • What do you mean by "Pointers were not shown correctly"? Maybe you should edit your question to add an example of what you get and what you want to see. – Anne Mar 29 '16 at 06:18
  • So what you want to get is the value of `(*x)`, not the value of `(x)`. To know if a variable is a pointer, you can test its type (`Cil.isPointerType vi.vtype`), and then, you have to build the lvalue `*x` (with something like `Lval (Mem ...,NoOffset)`) and use it to ask for its value. – Anne Mar 29 '16 at 06:48
  • What is the ... part? Simply the varinfo-field? How do I get the offset from the varinfo? When dereferencing a pointer, this will be needed(or didn't I get what you want to say)? – Thomas Böhm Mar 29 '16 at 07:19
  • You should have a look at the `cil_types.mli` file where you can find the definitions of all those data, and some explanations about how to build them. You need to dereference because you want to get the value of `*x`. As you've seen, if you ask the value of `x`, you get that it points to `y` (in your example) which is indeed the value of the pointer. – Anne Mar 29 '16 at 07:40
  • I've looked at the definitions in cil_types.mli: Mem needs an expression. Where do I get this from? I get varinfos by Kernel_function.get_locals, but I cannot see a similar function to get the expressions? Are there any example-codes around showing what i want? I cannot find good documenations or tutorials. – Thomas Böhm Mar 29 '16 at 08:21
  • Why can't I see the functions "Locations.Location_Bytes.pretty or Cvalue.Model.pretty? I think they get the data I want from the state, but they are not visible in the framework (newest version, but no function pretty in the source files?) – Thomas Böhm Mar 29 '16 at 08:24
  • I don't undertand what you mean by "I can't see the functions ... Cvalue.Model.pretty", "they are not visible in the framework". What does that mean? If you grep `cvalue.ml` directly you will not see it because there is a module inclusion from `Lmap` (`src/kernel_services/abstract_interp/lmap.ml`), but using a tool such as Merlin, the auto-completion does propose it. Otherwise, you also have `Db.Value.pretty_state` which exports exactly that function. – anol Mar 30 '16 at 15:39
  • I am using Eclipse for my development, and my auto-completion shows every function (or at least no other was missing when I used them until now) except for this one. Maybe I should try to set up that Merlin-thing :) – Thomas Böhm Mar 31 '16 at 06:19

1 Answers1

3

The value of a variable depend on its type. So if the variable has type int, its value is an integer, but if the variable has the type int*, its value is the address of an int variable. The variable may have many other types such as structure, array, etc.

From you example, it seems that you want to get the value of the variable pointed by the pointer. Notice that in some cases, this is not a valid operation...

Anyway, I suppose that you can extract this function to print a lvalue from the previous answer in Frama-C Plugin development: Getting result of value-analysis:

let pretty_lval fmt stmt lval =
  let kinstr = Kstmt stmt in (* make a kinstr from a stmt *)
  let loc = (* make a location from a kinstr + an lval *)
    !Db.Value.lval_to_loc kinstr ~with_alarms:CilE.warn_none_mode lval
  in
  Db.Value.fold_state_callstack
    (fun state () ->
       (* for each state in the callstack *)
       let value = Db.Value.find state loc in (* obtain value for location *)
       Format.fprintf fmt "%a -> %a@." Printer.pp_lval lval
         Locations.Location_Bytes.pretty value (* print mapping *)
    ) () ~after:false kinstr

You can then print the information you are looking for with:

if Cil.isPointerType vi.vtype then
  let lval = (Mem (Cil.evar vi), NoOffset) in
  pretty_lval fmt stmt lval
Community
  • 1
  • 1
Anne
  • 1,270
  • 6
  • 15
  • Thanks, that answered my question regarding the pointers. Is there now a way to get the value and store it in an ocaml-variable, instead of printing it? Somehow by calling a function with value (from the solution) as parameter? – Thomas Böhm Mar 29 '16 at 10:11
  • 1
    What do you mean? `value` above **is** an ocaml variable. Perhaps you mean a string variable? If this is the case, you can use `Format.asprintf`, but this is rather an ocaml question. – Anne Mar 29 '16 at 11:14
  • What I meant was: I want to get the value that is stored at the variable. For example: if I have {{ NULL -> {0} }}, I want to store 0 in an Ocaml int-variable (or add it to a list or something like that). With asprintf, I get the string (with brackets, ->, NULL...). Is there a way to get the value by a Frama-C-function or do I have to split the String? – Thomas Böhm Mar 29 '16 at 11:56
  • 1
    Try `Db.Value.pretty` instead of `Locations.Location_Bytes.pretty`. I think that for your case, it will be simpler. – Anne Mar 29 '16 at 13:00
  • Thanks, exactly what I needed :) – Thomas Böhm Mar 29 '16 at 13:14