Skip to content

Commit 60c9fe5

Browse files
committed
move code_declt to goto_instruction_code.h
After introducing code_frontend_declt, code_declt is now used exclusively by goto instructions, and thus belongs into goto_instruction_code.h.
1 parent 698be3d commit 60c9fe5

File tree

3 files changed

+66
-66
lines changed

3 files changed

+66
-66
lines changed

jbmc/src/java_bytecode/create_array_with_type_intrinsic.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -75,7 +75,7 @@ codet create_array_with_type_body(
7575
code_blockt code_block;
7676

7777
// Declare new_array temporary:
78-
code_block.add(code_declt(new_array_symbol_expr));
78+
code_block.add(code_frontend_declt(new_array_symbol_expr));
7979

8080
// new_array = new Object[length];
8181
side_effect_exprt new_array_expr{

src/util/goto_instruction_code.h

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -189,6 +189,71 @@ inline code_deadt &to_code_dead(codet &code)
189189
return static_cast<code_deadt &>(code);
190190
}
191191

192+
/// A `codet` representing the declaration of a local variable.
193+
/// For example, if a variable (symbol) `x` is represented as a
194+
/// \ref symbol_exprt `sym`, then the declaration of this variable can be
195+
/// represented as `code_declt(sym)`.
196+
class code_declt : public codet
197+
{
198+
public:
199+
explicit code_declt(symbol_exprt symbol) : codet(ID_decl, {std::move(symbol)})
200+
{
201+
}
202+
203+
symbol_exprt &symbol()
204+
{
205+
return static_cast<symbol_exprt &>(op0());
206+
}
207+
208+
const symbol_exprt &symbol() const
209+
{
210+
return static_cast<const symbol_exprt &>(op0());
211+
}
212+
213+
const irep_idt &get_identifier() const
214+
{
215+
return symbol().get_identifier();
216+
}
217+
218+
static void check(
219+
const codet &code,
220+
const validation_modet vm = validation_modet::INVARIANT)
221+
{
222+
DATA_CHECK(
223+
vm, code.operands().size() == 1, "declaration must have one operand");
224+
DATA_CHECK(
225+
vm,
226+
code.op0().id() == ID_symbol,
227+
"declaring a non-symbol: " +
228+
id2string(to_symbol_expr(code.op0()).get_identifier()));
229+
}
230+
};
231+
232+
template <>
233+
inline bool can_cast_expr<code_declt>(const exprt &base)
234+
{
235+
return detail::can_cast_code_impl(base, ID_decl);
236+
}
237+
238+
inline void validate_expr(const code_declt &x)
239+
{
240+
code_declt::check(x);
241+
}
242+
243+
inline const code_declt &to_code_decl(const codet &code)
244+
{
245+
PRECONDITION(code.get_statement() == ID_decl);
246+
code_declt::check(code);
247+
return static_cast<const code_declt &>(code);
248+
}
249+
250+
inline code_declt &to_code_decl(codet &code)
251+
{
252+
PRECONDITION(code.get_statement() == ID_decl);
253+
code_declt::check(code);
254+
return static_cast<code_declt &>(code);
255+
}
256+
192257
/// \ref codet representation of a function call statement.
193258
/// The function call statement has three operands.
194259
/// The first is the expression that is used to store the return value.

src/util/std_code.h

Lines changed: 0 additions & 65 deletions
Original file line numberDiff line numberDiff line change
@@ -352,71 +352,6 @@ template<> inline bool can_cast_expr<code_skipt>(const exprt &base)
352352

353353
// there is no to_code_skip, so no validate_expr is provided for code_skipt
354354

355-
/// A `codet` representing the declaration of a local variable.
356-
/// For example, if a variable (symbol) `x` is represented as a
357-
/// \ref symbol_exprt `sym`, then the declaration of this variable can be
358-
/// represented as `code_declt(sym)`.
359-
class code_declt:public codet
360-
{
361-
public:
362-
explicit code_declt(symbol_exprt symbol) : codet(ID_decl, {std::move(symbol)})
363-
{
364-
}
365-
366-
symbol_exprt &symbol()
367-
{
368-
return static_cast<symbol_exprt &>(op0());
369-
}
370-
371-
const symbol_exprt &symbol() const
372-
{
373-
return static_cast<const symbol_exprt &>(op0());
374-
}
375-
376-
const irep_idt &get_identifier() const
377-
{
378-
return symbol().get_identifier();
379-
}
380-
381-
static void check(
382-
const codet &code,
383-
const validation_modet vm = validation_modet::INVARIANT)
384-
{
385-
DATA_CHECK(
386-
vm, code.operands().size() == 1, "declaration must have one operand");
387-
DATA_CHECK(
388-
vm,
389-
code.op0().id() == ID_symbol,
390-
"declaring a non-symbol: " +
391-
id2string(to_symbol_expr(code.op0()).get_identifier()));
392-
}
393-
};
394-
395-
template <>
396-
inline bool can_cast_expr<code_declt>(const exprt &base)
397-
{
398-
return detail::can_cast_code_impl(base, ID_decl);
399-
}
400-
401-
inline void validate_expr(const code_declt &x)
402-
{
403-
code_declt::check(x);
404-
}
405-
406-
inline const code_declt &to_code_decl(const codet &code)
407-
{
408-
PRECONDITION(code.get_statement() == ID_decl);
409-
code_declt::check(code);
410-
return static_cast<const code_declt &>(code);
411-
}
412-
413-
inline code_declt &to_code_decl(codet &code)
414-
{
415-
PRECONDITION(code.get_statement() == ID_decl);
416-
code_declt::check(code);
417-
return static_cast<code_declt &>(code);
418-
}
419-
420355
/// A `codet` representing the declaration of a local variable.
421356
/// For example, if a variable (symbol) `x` is represented as a
422357
/// \ref symbol_exprt `sym`, then the declaration of this variable can be

0 commit comments

Comments
 (0)