cprover
nondet_static.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Nondeterministic initialization of certain global scope
4  variables
5 
6 Author: Daniel Kroening, Michael Tautschnig
7 
8 Date: November 2011
9 
10 \*******************************************************************/
11 
14 
15 #include "nondet_static.h"
16 
18 
20 
22  const namespacet &ns,
23  goto_functionst &goto_functions,
24  const irep_idt &fct_name)
25 {
26  goto_functionst::function_mapt::iterator
27  i_it=goto_functions.function_map.find(fct_name);
28  assert(i_it!=goto_functions.function_map.end());
29 
30  goto_programt &init=i_it->second.body;
31 
33  {
34  const goto_programt::instructiont &instruction=*i_it;
35 
36  if(instruction.is_assign())
37  {
38  const symbol_exprt &sym=to_symbol_expr(
39  to_code_assign(instruction.code).lhs());
40 
41  // is it a __CPROVER_* variable?
43  continue;
44 
45  // any other internal variable such as Java specific?
46  if(
47  ns.lookup(sym.get_identifier())
48  .type.get_bool(ID_C_no_nondet_initialization))
49  {
50  continue;
51  }
52 
53  // static lifetime?
54  if(!ns.lookup(sym.get_identifier()).is_static_lifetime)
55  continue;
56 
57  // constant?
59  continue;
60 
61  const goto_programt::instructiont original_instruction = instruction;
62  i_it->make_assignment();
63  i_it->code = code_assignt(
64  sym,
66  sym.type(), original_instruction.source_location));
67  i_it->source_location = original_instruction.source_location;
68  i_it->function = original_instruction.function;
69  }
70  else if(instruction.is_function_call())
71  {
72  const code_function_callt &fct=to_code_function_call(instruction.code);
73  const symbol_exprt &fsym=to_symbol_expr(fct.function());
74 
75  if(has_prefix(id2string(fsym.get_identifier()), "#ini#"))
76  nondet_static(ns, goto_functions, fsym.get_identifier());
77  }
78  }
79 }
80 
82  const namespacet &ns,
83  goto_functionst &goto_functions)
84 {
85  nondet_static(ns, goto_functions, INITIALIZE_FUNCTION);
86 
87  // update counters etc.
88  goto_functions.update();
89 }
90 
91 void nondet_static(goto_modelt &goto_model)
92 {
93  const namespacet ns(goto_model.symbol_table);
94  nondet_static(ns, goto_model.goto_functions);
95 }
irep_idt function
The function this instruction belongs to.
Definition: goto_program.h:179
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:128
function_mapt function_map
typet & type()
Definition: expr.h:56
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:240
exprt & lhs()
Definition: std_code.h:209
Symbol Table + CFG.
#define INITIALIZE_FUNCTION
Nondeterministic initialization of certain global scope variables.
TO_BE_DOCUMENTED.
Definition: namespace.h:74
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1340
bool is_constant_or_has_constant_components(const typet &type, const namespacet &ns)
Identify if a given type is constant itself or contains constant components.
Definition: type.cpp:47
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
A function call.
Definition: std_code.h:858
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
exprt & function()
Definition: std_code.h:878
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:182
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
Expression to hold a symbol (variable)
Definition: std_expr.h:90
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:136
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
Assignment.
Definition: std_code.h:196
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:909