Skip to content

Commit d657a5d

Browse files
committed
Make componentt::{base,pretty}_name comments
The only semantically relevant name information is the ID_name entry. Two components should not be considered different when they only differ in their base_name or pretty_name. Thus, use ID_C_base_name and ID_C_pretty_name, respectively, to store these. The goto binary version is incremented as goto binaries compiled before this patch are incompatible with the changes introduced here. Fixes: #5818
1 parent c41ce2b commit d657a5d

File tree

12 files changed

+22
-16
lines changed

12 files changed

+22
-16
lines changed
709 Bytes
Binary file not shown.

regression/ansi-c/arch_flags_mcpu_bad/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ This tests the -mcpu=cortex=a15 flag that should activate ARM-32 mode.
1111
The object file 'object.intel' was compiled from 'source.c' with goto-cc
1212
on a 64-bit platform:
1313

14-
goto-cc -c source.c
14+
goto-cc -c source.c -o object.intel
1515

1616
preproc.i is already pre-processed so that it can be linked in without
1717
needing to invoke a pre-processor from a cross-compile toolchain on your
703 Bytes
Binary file not shown.
Binary file not shown.

regression/ansi-c/arch_flags_mthumb_bad/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ This tests the -mthumb flag that should activate ARM-32 mode. The object
1111
file 'object.intel' was compiled from 'source.c' with goto-cc on a
1212
64-bit platform:
1313

14-
goto-cc -c source.c
14+
goto-cc -c source.c -o object.intel
1515

1616
preproc.i is already pre-processed so that it can be linked in without
1717
needing to invoke a pre-processor from a cross-compile toolchain on your
702 Bytes
Binary file not shown.

src/ansi-c/expr2c.cpp

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1551,13 +1551,13 @@ std::string expr2ct::convert_member(
15511551

15521552
if(!component_name.empty())
15531553
{
1554-
const exprt &comp_expr = struct_union_type.get_component(component_name);
1554+
const auto &comp_expr = struct_union_type.get_component(component_name);
15551555

15561556
if(comp_expr.is_nil())
15571557
return convert_norep(src, precedence);
15581558

1559-
if(!comp_expr.get(ID_pretty_name).empty())
1560-
dest+=comp_expr.get_string(ID_pretty_name);
1559+
if(!comp_expr.get_pretty_name().empty())
1560+
dest += id2string(comp_expr.get_pretty_name());
15611561
else
15621562
dest+=id2string(component_name);
15631563

@@ -1569,9 +1569,12 @@ std::string expr2ct::convert_member(
15691569
if(n>=struct_union_type.components().size())
15701570
return convert_norep(src, precedence);
15711571

1572-
const exprt &comp_expr = struct_union_type.components()[n];
1572+
const auto &comp_expr = struct_union_type.components()[n];
15731573

1574-
dest+=comp_expr.get_string(ID_pretty_name);
1574+
if(!comp_expr.get_pretty_name().empty())
1575+
dest += id2string(comp_expr.get_pretty_name());
1576+
else
1577+
dest += id2string(comp_expr.get_name());
15751578

15761579
return dest;
15771580
}

src/cpp/expr2cpp.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -95,7 +95,10 @@ std::string expr2cppt::convert_struct(
9595

9696
dest+=sep;
9797
dest+='.';
98-
dest += c.get_string(ID_pretty_name);
98+
if(!c.get_pretty_name().empty())
99+
dest += id2string(c.get_pretty_name());
100+
else
101+
dest += id2string(c.get_name());
99102
dest+='=';
100103
dest+=tmp;
101104
}

src/goto-instrument/alignment_checks.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -80,8 +80,8 @@ void print_struct_alignment_problems(
8080
<< symbol_pair.second.location << '\n';
8181
}
8282

83-
out << "members " << it_mem->get_pretty_name() << " and "
84-
<< it_next->get_pretty_name() << " might interfere\n";
83+
out << "members " << it_mem->get_name() << " and "
84+
<< it_next->get_name() << " might interfere\n";
8585
}
8686
}
8787
}

src/goto-programs/write_goto_binary.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ Author: CM Wintersteiger
1212
#ifndef CPROVER_GOTO_PROGRAMS_WRITE_GOTO_BINARY_H
1313
#define CPROVER_GOTO_PROGRAMS_WRITE_GOTO_BINARY_H
1414

15-
#define GOTO_BINARY_VERSION 5
15+
#define GOTO_BINARY_VERSION 6
1616

1717
#include <iosfwd>
1818
#include <string>

src/util/irep_ids.def

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -347,7 +347,7 @@ IREP_ID_TWO(mult, *)
347347
IREP_ID_TWO(div, /)
348348
IREP_ID_TWO(power, **)
349349
IREP_ID_ONE(factorial_power)
350-
IREP_ID_ONE(pretty_name)
350+
IREP_ID_TWO(C_pretty_name, #pretty_name)
351351
IREP_ID_TWO(C_class, #class)
352352
IREP_ID_TWO(C_field, #field)
353353
IREP_ID_TWO(C_interface, #interface)

src/util/std_types.h

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -82,12 +82,12 @@ class struct_union_typet:public typet
8282

8383
const irep_idt &get_base_name() const
8484
{
85-
return get(ID_base_name);
85+
return get(ID_C_base_name);
8686
}
8787

8888
void set_base_name(const irep_idt &base_name)
8989
{
90-
return set(ID_base_name, base_name);
90+
return set(ID_C_base_name, base_name);
9191
}
9292

9393
const irep_idt &get_access() const
@@ -102,12 +102,12 @@ class struct_union_typet:public typet
102102

103103
const irep_idt &get_pretty_name() const
104104
{
105-
return get(ID_pretty_name);
105+
return get(ID_C_pretty_name);
106106
}
107107

108108
void set_pretty_name(const irep_idt &name)
109109
{
110-
return set(ID_pretty_name, name);
110+
return set(ID_C_pretty_name, name);
111111
}
112112

113113
bool get_anonymous() const

0 commit comments

Comments
 (0)