Do not accept arrays of variable size with static lifetime
Neither Clang nor GCC accept these. In addition to rejecting such declarations, also fix the off-by-one error reported in #525: type declarations are type checked before their symbols are processed, thus the symbol name needs to be set up early. A lookup via the symbol table, however, is not yet possible. Thus maintain the full symbol. Fixes: #525
This commit is contained in:
parent
40d1560702
commit
544682c934
|
@ -0,0 +1,20 @@
|
|||
typedef unsigned char u1;
|
||||
typedef unsigned short u2;
|
||||
typedef unsigned long long u4;
|
||||
|
||||
// Not resolved (as expected)
|
||||
u4 B[( (u1)( ( (u1)15 ) / ( ( (((sizeof(u4))/(sizeof(u1)))*((u1)15)) > ((u1)64)) ? (0) : (1) ) ) )];
|
||||
|
||||
// Correctly resolved
|
||||
u2 C[( (u1)( ( (u1)11 ) / ( ( (((sizeof(u2))/(sizeof(u1)))*((u1)11)) > ((u1)64)) ? (0) : (1) ) ) )];
|
||||
|
||||
int main()
|
||||
{
|
||||
// Correctly resolved
|
||||
u2 A[( (u1)( ( (u1)1 ) / ( ( (((sizeof(u2))/(sizeof(u1)))*((u1)1)) > ((u1)64)) ? (0) : (1) ) ) )];
|
||||
|
||||
// Correctly resolved
|
||||
static u4 D[( (u1)( ( (u1)4 ) / ( ( (((sizeof(u4))/(sizeof(u1)))*((u1)4)) > ((u1)64)) ? (0) : (1) ) ) )];
|
||||
|
||||
return 0;
|
||||
}
|
|
@ -0,0 +1,9 @@
|
|||
CORE
|
||||
main.c
|
||||
|
||||
^EXIT=(64|1)$
|
||||
^SIGNAL=0$
|
||||
^CONVERSION ERROR$
|
||||
array size of static symbol `B' is not constant$
|
||||
--
|
||||
^warning: ignoring
|
|
@ -45,8 +45,6 @@ void c_typecheck_baset::move_symbol(symbolt &symbol, symbolt *&new_symbol)
|
|||
|
||||
void c_typecheck_baset::typecheck_symbol(symbolt &symbol)
|
||||
{
|
||||
current_symbol_id=symbol.name;
|
||||
|
||||
bool is_function=symbol.type.id()==ID_code;
|
||||
|
||||
const typet &final_type=follow(symbol.type);
|
||||
|
@ -703,6 +701,7 @@ void c_typecheck_baset::typecheck_declaration(
|
|||
|
||||
symbolt symbol;
|
||||
declaration.to_symbol(*d_it, symbol);
|
||||
current_symbol=symbol;
|
||||
|
||||
// now check other half of type
|
||||
typecheck_type(symbol.type);
|
||||
|
|
|
@ -61,7 +61,7 @@ protected:
|
|||
symbol_tablet &symbol_table;
|
||||
const irep_idt module;
|
||||
const irep_idt mode;
|
||||
irep_idt current_symbol_id;
|
||||
symbolt current_symbol;
|
||||
|
||||
typedef std::unordered_map<irep_idt, typet, irep_id_hash> id_type_mapt;
|
||||
id_type_mapt parameter_map;
|
||||
|
|
|
@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
#include <util/c_types.h>
|
||||
#include <util/config.h>
|
||||
#include <util/invariant.h>
|
||||
#include <util/simplify_expr.h>
|
||||
#include <util/arith_tools.h>
|
||||
#include <util/std_types.h>
|
||||
|
@ -551,9 +552,15 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
|
|||
{
|
||||
// not a constant and not infinity
|
||||
|
||||
assert(!current_symbol_id.empty());
|
||||
PRECONDITION(!current_symbol.name.empty());
|
||||
|
||||
const symbolt &base_symbol=lookup(current_symbol_id);
|
||||
if(current_symbol.is_static_lifetime)
|
||||
{
|
||||
error().source_location=current_symbol.location;
|
||||
error() << "array size of static symbol `"
|
||||
<< current_symbol.base_name << "' is not constant" << eom;
|
||||
throw 0;
|
||||
}
|
||||
|
||||
// Need to pull out! We insert new symbol.
|
||||
source_locationt source_location=size.find_source_location();
|
||||
|
@ -564,7 +571,7 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
|
|||
do
|
||||
{
|
||||
suffix="$array_size"+std::to_string(count);
|
||||
temp_identifier=id2string(base_symbol.name)+suffix;
|
||||
temp_identifier=id2string(current_symbol.name)+suffix;
|
||||
count++;
|
||||
}
|
||||
while(symbol_table.symbols.find(temp_identifier)!=
|
||||
|
@ -573,13 +580,13 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
|
|||
// add the symbol to symbol table
|
||||
auxiliary_symbolt new_symbol;
|
||||
new_symbol.name=temp_identifier;
|
||||
new_symbol.pretty_name=id2string(base_symbol.pretty_name)+suffix;
|
||||
new_symbol.base_name=id2string(base_symbol.base_name)+suffix;
|
||||
new_symbol.pretty_name=id2string(current_symbol.pretty_name)+suffix;
|
||||
new_symbol.base_name=id2string(current_symbol.base_name)+suffix;
|
||||
new_symbol.type=size.type();
|
||||
new_symbol.type.set(ID_C_constant, true);
|
||||
new_symbol.is_type=false;
|
||||
new_symbol.is_static_lifetime=false;
|
||||
new_symbol.value.make_nil();
|
||||
new_symbol.value=size;
|
||||
new_symbol.location=source_location;
|
||||
|
||||
symbol_table.add(new_symbol);
|
||||
|
|
Loading…
Reference in New Issue