From aef560529a3322f4a50ea4d6a2c14bd7e23b212f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 28 Sep 2020 16:51:24 +0200
Subject: [PATCH] [Eva] Frama_C_show_each directives print the offsetmap on
arrays.
---
.../value/domains/cvalue/cvalue_transfer.ml | 4 +--
src/plugins/value/engine/transfer_stmt.ml | 35 +++++++++----------
tests/builtins/fam.c | 2 +-
3 files changed, 19 insertions(+), 22 deletions(-)
diff --git a/src/plugins/value/domains/cvalue/cvalue_transfer.ml b/src/plugins/value/domains/cvalue/cvalue_transfer.ml
index 94bb435e101..eca8881948b 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 d7bb71ccae0..953d273cd33 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 bd928c9b097..3d189d20aa3 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);
}
--
GitLab