Skip to content

Commit 4e5bf6e

Browse files
committed
Move "is hidden" attribute of goto functions out of type
Whether the execution of a goto function is to be hidden has nothing to do with its signature, and therefore should not be included in the type (irrespective of whether the type is stored in goto_functiont or in the symbol table). As this attribute is recomputed upon reading a goto binary, there is no need to store it in the goto binary, and thus also no need to bump the goto-binary version number.
1 parent d2abadb commit 4e5bf6e

File tree

3 files changed

+14
-9
lines changed

3 files changed

+14
-9
lines changed

src/goto-programs/goto_function.h

Lines changed: 12 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -60,19 +60,17 @@ class goto_functiont
6060
return type.get_bool(ID_C_inlined);
6161
}
6262

63-
DEPRECATED(SINCE(2019, 2, 16, "Get the type from the symbol table instead"))
6463
bool is_hidden() const
6564
{
66-
return type.get_bool(ID_C_hide);
65+
return function_is_hidden;
6766
}
6867

69-
DEPRECATED(SINCE(2019, 2, 16, "Get the type from the symbol table instead"))
7068
void make_hidden()
7169
{
72-
type.set(ID_C_hide, true);
70+
function_is_hidden = true;
7371
}
7472

75-
goto_functiont() : body(), type({}, empty_typet())
73+
goto_functiont() : body(), type({}, empty_typet()), function_is_hidden(false)
7674
{
7775
}
7876

@@ -81,20 +79,23 @@ class goto_functiont
8179
body.clear();
8280
type.clear();
8381
parameter_identifiers.clear();
82+
function_is_hidden = false;
8483
}
8584

8685
void swap(goto_functiont &other)
8786
{
8887
body.swap(other.body);
8988
type.swap(other.type);
9089
parameter_identifiers.swap(other.parameter_identifiers);
90+
std::swap(function_is_hidden, other.function_is_hidden);
9191
}
9292

9393
void copy_from(const goto_functiont &other)
9494
{
9595
body.copy_from(other.body);
9696
type = other.type;
9797
parameter_identifiers = other.parameter_identifiers;
98+
function_is_hidden = other.function_is_hidden;
9899
}
99100

100101
goto_functiont(const goto_functiont &) = delete;
@@ -103,7 +104,8 @@ class goto_functiont
103104
goto_functiont(goto_functiont &&other)
104105
: body(std::move(other.body)),
105106
type(std::move(other.type)),
106-
parameter_identifiers(std::move(other.parameter_identifiers))
107+
parameter_identifiers(std::move(other.parameter_identifiers)),
108+
function_is_hidden(other.function_is_hidden)
107109
{
108110
}
109111

@@ -112,6 +114,7 @@ class goto_functiont
112114
body = std::move(other.body);
113115
type = std::move(other.type);
114116
parameter_identifiers = std::move(other.parameter_identifiers);
117+
function_is_hidden = other.function_is_hidden;
115118
return *this;
116119
}
117120

@@ -120,6 +123,9 @@ class goto_functiont
120123
/// The validation mode indicates whether well-formedness check failures are
121124
/// reported via DATA_INVARIANT violations or exceptions.
122125
void validate(const namespacet &ns, const validation_modet vm) const;
126+
127+
protected:
128+
bool function_is_hidden;
123129
};
124130

125131
void get_local_identifiers(const goto_functiont &, std::set<irep_idt> &dest);

src/goto-programs/read_bin_goto_object.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -131,8 +131,8 @@ static bool read_bin_goto_object(
131131
instruction.labels.push_back(label);
132132
if(label == CPROVER_PREFIX "HIDE")
133133
hidden=true;
134-
// The above info is normally in the type of the goto_functiont object,
135-
// which should likely be stored in the binary.
134+
// The above info is also held in the goto_functiont object, and could
135+
// be stored in the binary.
136136
}
137137
}
138138

src/util/irep_ids.def

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -285,7 +285,6 @@ IREP_ID_ONE(signed_int128)
285285
IREP_ID_ONE(unsigned_int128)
286286
IREP_ID_ONE(case)
287287
IREP_ID_TWO(C_inlined, #inlined)
288-
IREP_ID_TWO(C_hide, #hide)
289288
IREP_ID_ONE(hide)
290289
IREP_ID_ONE(abs)
291290
IREP_ID_ONE(sign)

0 commit comments

Comments
 (0)