diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml index 7a15dce648818142cd98813462572deb20d9728f..6567141ad0a51d2dbd1cff12ccae4751edb12368 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 6765be0d0f303e6cb94c3370a44cacd398c151ff..ddf1be28132cef2717a63e266d47e895fac8cb6b 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 33ca7c164f58687e2d998762d3b0108f4ea5f14f..3f4ab94f35323b73bda4e9933cdf48fd3afc665e 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 0000000000000000000000000000000000000000..dd972c8418ed4e042d4e2912312e7c538ea9599c --- /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 0000000000000000000000000000000000000000..62a4b01b9fb855630e67033bd10a1a209ec595ba --- /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; +} + +