Skip to content

Commit 46de172

Browse files
author
Daniel Kroening
committed
extend goto_programt::instructiont API
This adds get_X() methods that make the use of goto program instructions more type safe.
1 parent 2b87abd commit 46de172

File tree

1 file changed

+78
-0
lines changed

1 file changed

+78
-0
lines changed

src/goto-programs/goto_program.h

+78
Original file line numberDiff line numberDiff line change
@@ -180,6 +180,76 @@ class goto_programt
180180
public:
181181
codet code;
182182

183+
/// Get the assignment for ASSIGN
184+
const code_assignt &get_assign() const
185+
{
186+
PRECONDITION(is_assign());
187+
return to_code_assign(code);
188+
}
189+
190+
/// Get the assignment for ASSIGN
191+
code_assignt &get_assign()
192+
{
193+
PRECONDITION(is_assign());
194+
return to_code_assign(code);
195+
}
196+
197+
/// Get the declaration for DECL
198+
const code_declt &get_decl() const
199+
{
200+
PRECONDITION(is_decl());
201+
return to_code_decl(code);
202+
}
203+
204+
/// Get the declaration for DECL
205+
code_declt &get_decl()
206+
{
207+
PRECONDITION(is_decl());
208+
return to_code_decl(code);
209+
}
210+
211+
/// Get the dead statement for DEAD
212+
const code_deadt &get_dead() const
213+
{
214+
PRECONDITION(is_dead());
215+
return to_code_dead(code);
216+
}
217+
218+
/// Get the dead statement for DEAD
219+
code_deadt &get_dead()
220+
{
221+
PRECONDITION(is_dead());
222+
return to_code_dead(code);
223+
}
224+
225+
/// Get the return statement for READ
226+
const code_returnt &get_return() const
227+
{
228+
PRECONDITION(is_return());
229+
return to_code_return(code);
230+
}
231+
232+
/// Get the return statement for READ
233+
code_returnt &get_return()
234+
{
235+
PRECONDITION(is_return());
236+
return to_code_return(code);
237+
}
238+
239+
/// Get the function call for FUNCTION_CALL
240+
const code_function_callt &get_function_call() const
241+
{
242+
PRECONDITION(is_function_call());
243+
return to_code_function_call(code);
244+
}
245+
246+
/// Get the function call for FUNCTION_CALL
247+
code_function_callt &get_function_call()
248+
{
249+
PRECONDITION(is_function_call());
250+
return to_code_function_call(code);
251+
}
252+
183253
/// The function this instruction belongs to
184254
irep_idt function;
185255

@@ -190,8 +260,16 @@ class goto_programt
190260
goto_program_instruction_typet type;
191261

192262
/// Guard for gotos, assume, assert
263+
/// Use get_condition() to read
193264
exprt guard;
194265

266+
/// Get the condition of gotos, assume, assert
267+
const exprt &get_condition() const
268+
{
269+
PRECONDITION(is_goto() || is_assume() || is_assert());
270+
return guard;
271+
}
272+
195273
// The below will eventually become a single target only.
196274
/// The target for gotos and for start_thread nodes
197275
typedef std::list<instructiont>::iterator targett;

0 commit comments

Comments
 (0)