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 
17 #include <util/namespace.h>
18 #include <util/std_expr.h>
19 #include <util/cprover_prefix.h>
20 #include <util/prefix.h>
21 
23 
25  const namespacet &ns,
26  goto_functionst &goto_functions,
27  const irep_idt &fct_name)
28 {
29  goto_functionst::function_mapt::iterator
30  i_it=goto_functions.function_map.find(fct_name);
31  assert(i_it!=goto_functions.function_map.end());
32 
33  goto_programt &init=i_it->second.body;
34 
36  {
37  const goto_programt::instructiont &instruction=*i_it;
38 
39  if(instruction.is_assign())
40  {
41  const symbol_exprt &sym=to_symbol_expr(
42  to_code_assign(instruction.code).lhs());
43 
44  // is it a __CPROVER_* variable?
46  continue;
47 
48  // static lifetime?
49  if(!ns.lookup(sym.get_identifier()).is_static_lifetime)
50  continue;
51 
52  // constant?
53  if(sym.type().get_bool(ID_C_constant))
54  continue;
55 
56  i_it=init.insert_before(++i_it);
57  i_it->make_assignment();
58  i_it->code=code_assignt(sym, side_effect_expr_nondett(sym.type()));
59  i_it->source_location=instruction.source_location;
60  i_it->function=instruction.function;
61  }
62  else if(instruction.is_function_call())
63  {
64  const code_function_callt &fct=to_code_function_call(instruction.code);
65  const symbol_exprt &fsym=to_symbol_expr(fct.function());
66 
67  if(has_prefix(id2string(fsym.get_identifier()), "#ini#"))
68  nondet_static(ns, goto_functions, fsym.get_identifier());
69  }
70  }
71 }
72 
73 
75  const namespacet &ns,
76  goto_functionst &goto_functions)
77 {
78  nondet_static(ns, goto_functions, CPROVER_PREFIX "initialize");
79 
80  // update counters etc.
81  goto_functions.update();
82 }
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
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:120
Goto Programs with Functions.
typet & type()
Definition: expr.h:60
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:178
exprt & lhs()
Definition: std_code.h:157
Nondeterministic initialization of certain global scope variables.
API to expression classes.
TO_BE_DOCUMENTED.
Definition: namespace.h:62
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1037
A function call.
Definition: std_code.h:657
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
exprt & function()
Definition: std_code.h:677
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
Expression to hold a symbol (variable)
Definition: std_expr.h:82
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
Assignment.
Definition: std_code.h:144
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700