CBMC
loop_ids.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Loop IDs
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_PROGRAMS_LOOP_IDS_H
13 #define CPROVER_GOTO_PROGRAMS_LOOP_IDS_H
14 
15 #include <util/ui_message.h>
16 
17 class goto_functionst;
18 class goto_modelt;
19 class goto_programt;
20 
27 struct loop_idt
28 {
29  loop_idt(const irep_idt &function_id, const unsigned int loop_number)
31  {
32  }
33 
34  loop_idt(const loop_idt &other) = default;
35 
37  unsigned int loop_number;
38 
39  bool operator==(const loop_idt &o) const
40  {
41  return function_id == o.function_id && loop_number == o.loop_number;
42  }
43 
44  bool operator!=(const loop_idt &o) const
45  {
46  return !operator==(o);
47  }
48 
49  bool operator<(const loop_idt &o) const
50  {
51  return function_id < o.function_id ||
53  }
54 };
55 
56 void show_loop_ids(
58  const goto_modelt &);
59 
60 void show_loop_ids(
62  const goto_functionst &);
63 
64 void show_loop_ids(
66  const irep_idt &function_id,
67  const goto_programt &);
68 
69 #endif // CPROVER_GOTO_PROGRAMS_LOOP_IDS_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
void show_loop_ids(ui_message_handlert::uit, const goto_modelt &)
Definition: loop_ids.cpp:21
Loop id used to identify loops.
Definition: loop_ids.h:28
bool operator<(const loop_idt &o) const
Definition: loop_ids.h:49
loop_idt(const loop_idt &other)=default
irep_idt function_id
Definition: loop_ids.h:36
loop_idt(const irep_idt &function_id, const unsigned int loop_number)
Definition: loop_ids.h:29
unsigned int loop_number
Definition: loop_ids.h:37
bool operator!=(const loop_idt &o) const
Definition: loop_ids.h:44
bool operator==(const loop_idt &o) const
Definition: loop_ids.h:39