[Eva] Frama_C_show_each directives print the offsetmap on arrays.

src/plugins/value/domains/cvalue/cvalue_transfer.ml

@@ -224,13 +224,13 @@ let finalize_call stmt call ~pre:_ ~post:state =
 
 let show_expr valuation state fmt expr =
   match expr.enode with
-  | Lval lval ->
+  | Lval lval | StartOf lval ->
     let record = match valuation.Abstract_domain.find_loc lval with
       | `Value record -> record
       | `Top -> assert false
     in
     let offsm = Cvalue_offsetmap.offsetmap_of_lval state lval record.loc in
-    let typ = Cil.typeOf expr in
+    let typ = Cil.typeOfLval lval in
     Eval_op.pretty_offsetmap typ fmt offsm
   | _ -> Format.fprintf fmt "%s" (Unicode.top_string ())
 

src/plugins/value/engine/transfer_stmt.ml

@@ -621,22 +621,17 @@ module Make (Abstract: Abstractions.Eva) = struct
     | None, _ | _, None ->
       fun fmt _ _ _ -> Format.fprintf fmt "%s" (Unicode.top_string ())
     | Some get_cvalue, Some get_ploc ->
-      fun fmt subdivnb expr state ->
-        match expr.enode with
-        | Lval lval ->
-          begin
-            try
-              let offsm =
-                fst (Eval.lvaluate ~for_writing:false ~subdivnb state lval)
-                >>- fun (_, loc, _) ->
-                Eval_op.offsetmap_of_loc (get_ploc loc) (get_cvalue state)
-              in
-              let typ = Cil.typeOf expr in
-              (Bottom.pretty (Eval_op.pretty_offsetmap typ)) fmt offsm
-            with Abstract_interp.Error_Top ->
-              Format.fprintf fmt "%s" (Unicode.top_string ())
-          end
-        | _ -> assert false
+      fun fmt subdivnb lval state ->
+        try
+          let offsm =
+            fst (Eval.lvaluate ~for_writing:false ~subdivnb state lval)
+            >>- fun (_, loc, _) ->
+            Eval_op.offsetmap_of_loc (get_ploc loc) (get_cvalue state)
+          in
+          let typ = Cil.typeOfLval lval in
+          (Bottom.pretty (Eval_op.pretty_offsetmap typ)) fmt offsm
+        with Abstract_interp.Error_Top ->
+          Format.fprintf fmt "%s" (Unicode.top_string ())
 
   (* For scalar expressions, prints the cvalue component of their values. *)
   let show_value =
@@ -650,10 +645,12 @@ module Make (Abstract: Abstractions.Eva) = struct
         (Bottom.pretty Cvalue.V.pretty) fmt value
 
   let pretty_arguments ~subdivnb state arguments =
+    let is_scalar lval = Cil.isArithmeticOrPointerType (Cil.typeOfLval lval) in
     let pretty fmt expr =
-      if Cil.isArithmeticOrPointerType (Cil.typeOf expr)
-      then show_value fmt subdivnb expr state
-      else show_offsm fmt subdivnb expr state
+      match expr.enode with
+      | Lval lval | StartOf lval when not (is_scalar lval) ->
+        show_offsm fmt subdivnb lval state
+      | _ -> show_value fmt subdivnb expr state
     in
     Pretty_utils.pp_list ~pre:"@[<hv>" ~sep:",@ " ~suf:"@]" pretty arguments
 

tests/builtins/fam.c

@@ -12,6 +12,6 @@ void main (void) {
  buf[0] = 42;
  TcpOption * option = buf + 10;
  option->length = 5;
- Frama_C_show_each(option->value);
+ Frama_C_show_each(&(option->value));
  memcpy(option->value, value, 2);
 }