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  // static lifetime?
46  if(!ns.lookup(sym.get_identifier()).is_static_lifetime)
47  continue;
48 
49  // constant?
51  continue;
52 
53  i_it=init.insert_before(++i_it);
54  i_it->make_assignment();
55  i_it->code=code_assignt(sym, side_effect_expr_nondett(sym.type()));
56  i_it->source_location=instruction.source_location;
57  i_it->function=instruction.function;
58  }
59  else if(instruction.is_function_call())
60  {
61  const code_function_callt &fct=to_code_function_call(instruction.code);
62  const symbol_exprt &fsym=to_symbol_expr(fct.function());
63 
64  if(has_prefix(id2string(fsym.get_identifier()), "#ini#"))
65  nondet_static(ns, goto_functions, fsym.get_identifier());
66  }
67  }
68 }
69 
71  const namespacet &ns,
72  goto_functionst &goto_functions)
73 {
74  nondet_static(ns, goto_functions, INITIALIZE_FUNCTION);
75 
76  // update counters etc.
77  goto_functions.update();
78 }
79 
80 void nondet_static(goto_modelt &goto_model)
81 {
82  const namespacet ns(goto_model.symbol_table);
83  nondet_static(ns, goto_model.goto_functions);
84 }
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:43
#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:239
exprt & lhs()
Definition: std_code.h:208
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:1301
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:828
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
exprt & function()
Definition: std_code.h:848
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:130
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
Assignment.
Definition: std_code.h:195
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:879