From 356a6bd17082c07a9d38d7206b8bb300b623aeef Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 2 Oct 2020 22:39:13 +0200
Subject: [PATCH] [Kernel] add message key printer:field-offsets to print bit
ranges in fieldinfos
---
.../ast_printing/cil_printer.ml | 9 ++++++-
.../plugin_entry_points/kernel.ml | 2 ++
.../plugin_entry_points/kernel.mli | 2 ++
tests/syntax/field-offsets.c | 24 ++++++++++++++++++
tests/syntax/oracle/field-offsets.res.oracle | 25 +++++++++++++++++++
5 files changed, 61 insertions(+), 1 deletion(-)
create mode 100644 tests/syntax/field-offsets.c
create mode 100644 tests/syntax/oracle/field-offsets.res.oracle
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 7a15dce6488..6567141ad0a 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1830,7 +1830,14 @@ class cil_printer () = object (self)
(match fi.fbitfield with
| None -> ""
| Some i -> ": " ^ string_of_int i ^ " ")
- self#attributes fi.fattr
+ self#attributes fi.fattr;
+ if Kernel.(is_debug_key_enabled dkey_print_field_offsets) then
+ try
+ let (offset, size) = Cil.bitsOffset fi.ftype (Field (fi, NoOffset)) in
+ let first = offset in
+ let last = offset + size - 1 in
+ fprintf fmt " /* bits %d .. %d */" first last
+ with Cil.SizeOfError _ -> ()
method private opt_funspec fmt funspec =
if logic_printer_enabled && not (Cil.is_empty_funspec funspec) then
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 6765be0d0f3..ddf1be28132 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -105,6 +105,8 @@ let dkey_print_unspecified = register_category "printer:unspecified"
let dkey_print_vid = register_category "printer:vid"
+let dkey_print_field_offsets = register_category "printer:field-offsets"
+
let dkey_prop_status = register_category "prop-status"
let dkey_prop_status_emit = register_category "prop-status:emit"
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 33ca7c164f5..3f4ab94f353 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -99,6 +99,8 @@ val dkey_print_unspecified: category
val dkey_print_vid: category
+val dkey_print_field_offsets: category
+
val dkey_prop_status: category
val dkey_prop_status_emit: category
diff --git a/tests/syntax/field-offsets.c b/tests/syntax/field-offsets.c
new file mode 100644
index 00000000000..dd972c8418e
--- /dev/null
+++ b/tests/syntax/field-offsets.c
@@ -0,0 +1,24 @@
+/*run.config
+ STDOPT: #"-kernel-msg-key printer:field-offsets"
+ */
+
+#include <stdlib.h>
+
+struct st {
+ int a;
+ char b;
+ void *p;
+};
+
+struct fam {
+ int a;
+ char b;
+ int fam[]; // check that a SizeOfError exception does not crash the printer
+};
+
+int main() {
+ struct st st1 = { 2 };
+ struct fam *fam = malloc(sizeof(fam) + sizeof(int)*10);
+ fam->fam[9] = 0;
+ return st1.b + fam->fam[9];
+}
diff --git a/tests/syntax/oracle/field-offsets.res.oracle b/tests/syntax/oracle/field-offsets.res.oracle
new file mode 100644
index 00000000000..62a4b01b9fb
--- /dev/null
+++ b/tests/syntax/oracle/field-offsets.res.oracle
@@ -0,0 +1,25 @@
+[kernel] Parsing tests/syntax/field-offsets.c (with preprocessing)
+/* Generated by Frama-C */
+#include "stdlib.h"
+struct st {
+ int a ; /* bits 0 .. 31 */
+ char b ; /* bits 32 .. 39 */
+ void *p ; /* bits 64 .. 95 */
+};
+struct fam {
+ int a ; /* bits 0 .. 31 */
+ char b ; /* bits 32 .. 39 */
+ int fam[] ;
+};
+int main(void)
+{
+ int __retres;
+ struct fam *tmp_0;
+ struct st st1 = {.a = 2, .b = (char)0, .p = (void *)0};
+ struct fam *fam = malloc(sizeof(tmp_0) + sizeof(int) * (unsigned int)10);
+ fam->fam[9] = 0;
+ __retres = (int)st1.b + fam->fam[9];
+ return __retres;
+}
+
+
--
GitLab