diff --git a/src/plugins/value/domains/cvalue/cvalue_transfer.ml b/src/plugins/value/domains/cvalue/cvalue_transfer.ml index 94bb435e1011082f6a365b22399e8612f0b2355b..eca8881948b1a38333e25cf6f95779ba8cd2d0b5 100644 --- a/src/plugins/value/domains/cvalue/cvalue_transfer.ml +++ b/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 ()) diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml index d7bb71ccae05b325d7b83953d4f3af716a8b3f6b..953d273cd33cae2924f0fdfe75dee013a2491739 100644 --- a/src/plugins/value/engine/transfer_stmt.ml +++ b/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 diff --git a/tests/builtins/fam.c b/tests/builtins/fam.c index bd928c9b0970dfe79e209dce95868f10eb3e29fa..3d189d20aa307a45e4174694d97d7da54acdee99 100644 --- a/tests/builtins/fam.c +++ b/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); }