cprover
c_nondet_symbol_factory.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C Nondet Symbol Factory
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H
13 #define CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H
14 
15 #include <util/std_code.h>
16 #include <util/symbol_table.h>
17 
19  code_blockt &init_code,
20  symbol_tablet &symbol_table,
21  const irep_idt base_name,
22  const typet &type,
23  const source_locationt &,
24  bool allow_null);
25 
26 #endif // CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H
The type of an expression.
Definition: type.h:22
exprt c_nondet_symbol_factory(code_blockt &init_code, symbol_tablet &symbol_table, const irep_idt base_name, const typet &type, const source_locationt &, bool allow_null)
Creates a symbol and generates code so that it can vary over all possible values for its type...
The symbol table.
Definition: symbol_table.h:19
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Author: Diffblue Ltd.
Base class for all expressions.
Definition: expr.h:42
Sequential composition.
Definition: std_code.h:89