cprover
nondet_static.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Nondeterministically initializes global scope variables, except for
4  constants (such as string literals, final fields) and internal variables
5  (such as CPROVER and symex variables, language specific internal
6  variables).
7 
8 Author: Daniel Kroening, Michael Tautschnig
9 
10 Date: November 2011
11 
12 \*******************************************************************/
13 
19 
20 #include "nondet_static.h"
21 
23 
25 
32  const symbol_exprt &symbol_expr,
33  const namespacet &ns)
34 {
35  const irep_idt &id = symbol_expr.get_identifier();
36 
37  // is it a __CPROVER_* variable?
39  return false;
40 
41  // variable not in symbol table such as symex variable?
42  if(!ns.get_symbol_table().has_symbol(id))
43  return false;
44 
45  const symbolt &symbol = ns.lookup(id);
46 
47  // is the type explicitly marked as not to be nondet initialized?
48  if(symbol.type.get_bool(ID_C_no_nondet_initialization))
49  return false;
50 
51  // is the type explicitly marked as not to be initialized?
52  if(symbol.type.get_bool(ID_C_no_initialization_required))
53  return false;
54 
55  // static lifetime?
56  if(!symbol.is_static_lifetime)
57  return false;
58 
59  // constant?
60  return !is_constant_or_has_constant_components(symbol_expr.type(), ns) &&
62 }
63 
72  const namespacet &ns,
73  goto_functionst &goto_functions,
74  const irep_idt &fct_name)
75 {
76  goto_functionst::function_mapt::iterator fct_entry =
77  goto_functions.function_map.find(fct_name);
78  CHECK_RETURN(fct_entry != goto_functions.function_map.end());
79 
80  goto_programt &init = fct_entry->second.body;
81 
83  {
84  const goto_programt::instructiont &instruction=*i_it;
85 
86  if(instruction.is_assign())
87  {
88  const symbol_exprt &sym=to_symbol_expr(
89  to_code_assign(instruction.code).lhs());
90 
92  {
93  const goto_programt::instructiont original_instruction = instruction;
94  i_it->make_assignment();
95  i_it->code = code_assignt(
96  sym,
98  sym.type(), original_instruction.source_location));
99  i_it->source_location = original_instruction.source_location;
100  i_it->function = original_instruction.function;
101  }
102  }
103  else if(instruction.is_function_call())
104  {
105  const code_function_callt &fct=to_code_function_call(instruction.code);
106  const symbol_exprt &fsym=to_symbol_expr(fct.function());
107 
108  if(has_prefix(id2string(fsym.get_identifier()), "#ini#"))
109  nondet_static(ns, goto_functions, fsym.get_identifier());
110  }
111  }
112 }
113 
119  const namespacet &ns,
120  goto_functionst &goto_functions)
121 {
122  nondet_static(ns, goto_functions, INITIALIZE_FUNCTION);
123 
124  // update counters etc.
125  goto_functions.update();
126 }
127 
133 void nondet_static(goto_modelt &goto_model)
134 {
135  const namespacet ns(goto_model.symbol_table);
136  nondet_static(ns, goto_model.goto_functions);
137 }
irep_idt function
The function this instruction belongs to.
Definition: goto_program.h:184
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
#define CPROVER_PREFIX
const irep_idt & get_identifier() const
Definition: std_expr.h:187
function_mapt function_map
typet & type()
Return the type of the expression.
Definition: expr.h:68
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.
Definition: symbol.h:27
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:228
bool is_static_lifetime
Definition: symbol.h:65
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
exprt & lhs()
Definition: std_code.h:269
Symbol Table + CFG.
#define INITIALIZE_FUNCTION
Nondeterministically initializes global scope variables, except for constants (such as string literal...
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:126
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
codet representation of a function call statement.
Definition: std_code.h:1036
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:262
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
typet type
Type of symbol.
Definition: symbol.h:31
exprt & function()
Definition: std_code.h:1099
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:187
bool is_constant_or_has_constant_components(const typet &type, const namespacet &ns)
Identify whether a given type is constant itself or contains constant components. ...
Definition: std_types.cpp:223
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
Expression to hold a symbol (variable)
Definition: std_expr.h:154
bool is_nondet_initializable_static(const symbol_exprt &symbol_expr, const namespacet &ns)
See the return.
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:165
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
A codet representing an assignment in the program.
Definition: std_code.h:256
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173