From 95fb9335846db350cf78689df60bdb1a697bc033 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Tue, 5 May 2015 15:47:57 +0200 Subject: [PATCH] [mc] Knowledge about the size of pointer types in DWARF Some compilers do not emit DW_AT_byte_size for DW_TAG_pointer_type, so we fill this. We currently assume that the model-checked process is in the same architecture. This fixes the model-checker in clang. --- src/mc/mc_dwarf.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/mc/mc_dwarf.cpp b/src/mc/mc_dwarf.cpp index c68e14bcb6..1133efac84 100644 --- a/src/mc/mc_dwarf.cpp +++ b/src/mc/mc_dwarf.cpp @@ -678,6 +678,12 @@ static dw_type_t MC_dwarf_die_to_type(mc_object_info_t info, Dwarf_Die * die, type->dw_type_id = MC_dwarf_at_type(die); + // Some compiler do not emit DW_AT_byte_size for pointer_type, + // so we fill this. We currently assume that the model-checked process is in + // the same architecture.. + if (type->type == DW_TAG_pointer_type) + type->byte_size = sizeof(void*); + // Computation of the byte_size; if (dwarf_hasattr_integrate(die, DW_AT_byte_size)) type->byte_size = MC_dwarf_attr_integrate_uint(die, DW_AT_byte_size, 0); -- 2.20.1