cprover
c_typecheck_argc_argv.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: ANSI-C Conversion / Type Checking
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "c_typecheck_base.h"
13 
14 #include <util/arith_tools.h>
15 
16 void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol)
17 {
18  const code_typet::parameterst &parameters=
19  to_code_type(main_symbol.type).parameters();
20 
21  if(parameters.empty())
22  return;
23 
24  if(parameters.size()!=2 &&
25  parameters.size()!=3)
26  {
27  error().source_location=main_symbol.location;
28  error() << "main expected to have no or two or three parameters" << eom;
29  throw 0;
30  }
31 
32  symbolt *argc_new_symbol;
33 
34  const exprt &op0=static_cast<const exprt &>(parameters[0]);
35  const exprt &op1=static_cast<const exprt &>(parameters[1]);
36 
37  {
38  symbolt argc_symbol;
39 
40  argc_symbol.base_name="argc";
41  argc_symbol.name="argc'";
42  argc_symbol.type=op0.type();
43  argc_symbol.is_static_lifetime=true;
44  argc_symbol.is_lvalue=true;
45 
46  if(argc_symbol.type.id()!=ID_signedbv &&
47  argc_symbol.type.id()!=ID_unsignedbv)
48  {
49  error().source_location=main_symbol.location;
50  error() << "argc argument expected to be integer type, but got `"
51  << to_string(argc_symbol.type) << "'" << eom;
52  throw 0;
53  }
54 
55  move_symbol(argc_symbol, argc_new_symbol);
56  }
57 
58  {
59  if(op1.type().id()!=ID_pointer ||
60  op1.type().subtype().id()!=ID_pointer)
61  {
62  error().source_location=main_symbol.location;
63  error() << "argv argument expected to be pointer-to-pointer type, "
64  "but got `"
65  << to_string(op1.type()) << '\'' << eom;
66  throw 0;
67  }
68 
69  // we make the type of this thing an array of pointers
70  // need to add one to the size -- the array is terminated
71  // with NULL
72  exprt one_expr=from_integer(1, argc_new_symbol->type);
73 
74  const plus_exprt size_expr(argc_new_symbol->symbol_expr(), one_expr);
75  const array_typet argv_type(op1.type().subtype(), size_expr);
76 
77  symbolt argv_symbol;
78 
79  argv_symbol.base_name="argv'";
80  argv_symbol.name="argv'";
81  argv_symbol.type=argv_type;
82  argv_symbol.is_static_lifetime=true;
83  argv_symbol.is_lvalue=true;
84 
85  symbolt *argv_new_symbol;
86  move_symbol(argv_symbol, argv_new_symbol);
87  }
88 
89  if(parameters.size()==3)
90  {
91  symbolt envp_symbol;
92  envp_symbol.base_name="envp'";
93  envp_symbol.name="envp'";
94  envp_symbol.type=(static_cast<const exprt&>(parameters[2])).type();
95  envp_symbol.is_static_lifetime=true;
96 
97  symbolt envp_size_symbol, *envp_new_size_symbol;
98  envp_size_symbol.base_name="envp_size";
99  envp_size_symbol.name="envp_size'";
100  envp_size_symbol.type=op0.type(); // same type as argc!
101  envp_size_symbol.is_static_lifetime=true;
102  move_symbol(envp_size_symbol, envp_new_size_symbol);
103 
104  if(envp_symbol.type.id()!=ID_pointer)
105  {
106  error().source_location=main_symbol.location;
107  error() << "envp argument expected to be pointer type, but got `"
108  << to_string(envp_symbol.type) << '\'' << eom;
109  throw 0;
110  }
111 
112  exprt size_expr = envp_new_size_symbol->symbol_expr();
113 
114  envp_symbol.type.id(ID_array);
115  envp_symbol.type.add(ID_size).swap(size_expr);
116 
117  symbolt *envp_new_symbol;
118  move_symbol(envp_symbol, envp_new_symbol);
119  }
120 }
typet::subtype
const typet & subtype() const
Definition: type.h:38
c_typecheck_baset::add_argc_argv
void add_argc_argv(const symbolt &main_symbol)
Definition: c_typecheck_argc_argv.cpp:16
arith_tools.h
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:754
c_typecheck_base.h
c_typecheck_baset::to_string
virtual std::string to_string(const exprt &expr)
Definition: c_typecheck_base.cpp:23
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:305
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
exprt
Base class for all expressions.
Definition: expr.h:54
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
c_typecheck_baset::move_symbol
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
Definition: c_typecheck_base.cpp:33
messaget::eom
static eomt eom
Definition: message.h:284
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
messaget::error
mstreamt & error() const
Definition: message.h:386
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:236
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
irept::swap
void swap(irept &irep)
Definition: irep.h:303
irept::id
const irep_idt & id() const
Definition: irep.h:259
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:893
array_typet
Arrays with given size.
Definition: std_types.h:1000
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:27
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40