Skip to content

Commit 94dacc5

Browse files
committed
Revert "Revert "Use get_fresh_aux_symbol to create $array_size and fix its type""
This reverts commit 9e204fd.
1 parent bc9233e commit 94dacc5

File tree

2 files changed

+23
-27
lines changed

2 files changed

+23
-27
lines changed
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--program-only
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
--
9+
\(__CPROVER_size_t\)x\$array_size
10+
--
11+
There should not be any type cast of x$array_size to __CPROVER_size_t, because
12+
it already is of that type.

src/ansi-c/c_typecheck_type.cpp

Lines changed: 11 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
1616
#include <util/arith_tools.h>
1717
#include <util/c_types.h>
1818
#include <util/config.h>
19+
#include <util/fresh_symbol.h>
1920
#include <util/mathematical_types.h>
2021
#include <util/pointer_offset_size.h>
2122
#include <util/simplify_expr.h>
@@ -614,42 +615,25 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
614615
throw 0;
615616
}
616617

617-
// Need to pull out! We insert new symbol.
618-
unsigned count=0;
619-
irep_idt temp_identifier;
620-
std::string suffix;
621-
622-
do
623-
{
624-
suffix="$array_size"+std::to_string(count);
625-
temp_identifier=id2string(current_symbol.name)+suffix;
626-
count++;
627-
}
628-
while(symbol_table.symbols.find(temp_identifier)!=
629-
symbol_table.symbols.end());
630-
631-
// add the symbol to symbol table
632-
auxiliary_symbolt new_symbol;
633-
new_symbol.name=temp_identifier;
634-
new_symbol.pretty_name=id2string(current_symbol.pretty_name)+suffix;
635-
new_symbol.base_name=id2string(current_symbol.base_name)+suffix;
636-
new_symbol.type=size.type();
618+
symbolt &new_symbol = get_fresh_aux_symbol(
619+
size_type(),
620+
id2string(current_symbol.name) + "$array_size",
621+
id2string(current_symbol.base_name) + "$array_size",
622+
size_source_location,
623+
mode,
624+
symbol_table);
637625
new_symbol.type.set(ID_C_constant, true);
638-
new_symbol.value=size;
639-
new_symbol.location = size_source_location;
640-
new_symbol.mode = mode;
641-
642-
symbol_table.add(new_symbol);
626+
new_symbol.value = typecast_exprt::conditional_cast(size, size_type());
643627

644628
// produce the code that declares and initializes the symbol
645-
symbol_exprt symbol_expr(temp_identifier, new_symbol.type);
629+
symbol_exprt symbol_expr = new_symbol.symbol_expr();
646630

647631
code_declt declaration(symbol_expr);
648632
declaration.add_source_location() = size_source_location;
649633

650634
code_assignt assignment;
651635
assignment.lhs()=symbol_expr;
652-
assignment.rhs()=size;
636+
assignment.rhs() = new_symbol.value;
653637
assignment.add_source_location() = size_source_location;
654638

655639
// store the code

0 commit comments

Comments
 (0)