cprover
java_enum_static_init_unwind_handler.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Unwind loops in static initializers
4 
5 Author: Chris Smowton, chris.smowton@diffblue.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <util/invariant.h>
15 #include <util/suffix.h>
16 
32  const irep_idt &function_id,
33  unsigned loop_number,
34  unsigned unwind_count,
35  unsigned &unwind_max,
36  const symbol_tablet &symbol_table)
37 {
38  const std::string &function_str = id2string(function_id);
39  if(!has_suffix(function_str, ".<clinit>:()V"))
40  return tvt::unknown();
41 
42  const symbolt &function_symbol = symbol_table.lookup_ref(function_str);
43  irep_idt class_id = function_symbol.type.get(ID_C_class);
44  INVARIANT(
45  !class_id.empty(), "functions should have their defining class annotated");
46 
47  const typet &class_type = symbol_table.lookup_ref(class_id).type;
48  size_t unwinds = class_type.get_size_t(ID_java_enum_static_unwind);
49  if(unwinds != 0 && unwind_count < unwinds)
50  {
51  unwind_max = unwinds;
52  return tvt(false); // Must unwind
53  }
54  else
55  {
56  return tvt::unknown(); // Defer to other unwind handlers
57  }
58 }
The type of an expression.
Definition: type.h:22
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
static tvt unknown()
Definition: threeval.h:33
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
tvt java_enum_static_init_unwind_handler(const irep_idt &function_id, unsigned loop_number, unsigned unwind_count, unsigned &unwind_max, const symbol_tablet &symbol_table)
Unwind handler that special-cases the clinit (static initializer) functions of enumeration classes...
Definition: threeval.h:19
The symbol table.
Definition: symbol_table.h:19
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
typet type
Type of symbol.
Definition: symbol.h:34
Unwind loops in static initializers.
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:15
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:255
bool empty() const
Definition: dstring.h:61