Skip to content

Commit 6d2a0f0

Browse files
tautschnigtautschnig
committed
Add source location to invalid_source_file_exceptiont
This enables proper use in the C front-end in a way that is compatible with the compiler-specific message handlers in goto-cc: those message handlers generate source-location output that mimics that of the compiler being emulated. As future work it is thus possible to remove all "throw 0" instances from the C front-end.
1 parent d65b90b commit 6d2a0f0

17 files changed

+116
-69
lines changed

‎regression/ansi-c/enum_is_in_range/enum_test10.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
CORE
22
enum_test10.c
33

4-
^EXIT=(6|70)$
4+
^EXIT=(1|64)$
55
^SIGNAL=0$
6-
^file enum_test10.c line \d+ function main: __CPROVER_enum_is_in_range expects enum, but \(i\) has type `signed int`$
6+
__CPROVER_enum_is_in_range expects enum, but \(i\) has type `signed int`$
77
--
88
^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(i\): SUCCESS$
99
^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(i\): FAILURE$

‎regression/ansi-c/enum_is_in_range/enum_test12.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
CORE
22
enum_test12.c
33

4-
^EXIT=(6|70)$
4+
^EXIT=(1|64)$
55
^SIGNAL=0$
6-
^file enum_test12.c line \d+ function main: __CPROVER_enum_is_in_range takes exactly 1 argument, but 2 were provided$
6+
__CPROVER_enum_is_in_range takes exactly 1 argument, but 2 were provided$
77
--
88
^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(.*\): SUCCESS$
99
^\[main.assertion.1\] line \d+ assertion __CPROVER_enum_is_in_range\(.*\): FAILURE$

‎src/ansi-c/ansi_c_typecheck.cpp

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -67,5 +67,11 @@ bool ansi_c_typecheck(
6767
ansi_c_typecheck.error() << e << messaget::eom;
6868
}
6969

70+
catch(const invalid_source_file_exceptiont &e)
71+
{
72+
ansi_c_typecheck.error().source_location = e.get_source_location();
73+
ansi_c_typecheck.error() << e.get_reason() << messaget::eom;
74+
}
75+
7076
return message_handler.get_message_count(messaget::M_ERROR)!=errors_before;
7177
}

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 14 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -3151,21 +3151,22 @@ exprt c_typecheck_baset::do_special_functions(
31513151
if(expr.arguments().size() != 1)
31523152
{
31533153
std::ostringstream error_message;
3154-
error_message << expr.source_location().as_string() << ": " << identifier
3155-
<< " takes exactly 1 argument, but "
3154+
error_message << identifier << " takes exactly 1 argument, but "
31563155
<< expr.arguments().size() << " were provided";
3157-
throw invalid_source_file_exceptiont{error_message.str()};
3156+
throw invalid_source_file_exceptiont{
3157+
error_message.str(), expr.source_location()};
31583158
}
31593159
auto arg1 = expr.arguments()[0];
31603160
typecheck_expr(arg1);
31613161
if(!can_cast_type<c_enum_tag_typet>(arg1.type()))
31623162
{
31633163
// Can't enum range check a non-enum
31643164
std::ostringstream error_message;
3165-
error_message << expr.source_location().as_string() << ": " << identifier
3166-
<< " expects enum, but (" << expr2c(arg1, *this)
3167-
<< ") has type `" << type2c(arg1.type(), *this) << '`';
3168-
throw invalid_source_file_exceptiont{error_message.str()};
3165+
error_message << identifier << " expects enum, but ("
3166+
<< expr2c(arg1, *this) << ") has type `"
3167+
<< type2c(arg1.type(), *this) << '`';
3168+
throw invalid_source_file_exceptiont{
3169+
error_message.str(), expr.source_location()};
31693170
}
31703171
else
31713172
{
@@ -3218,9 +3219,9 @@ exprt c_typecheck_baset::do_special_functions(
32183219
if(expr.arguments().size() != 1)
32193220
{
32203221
std::ostringstream error_message;
3221-
error_message << expr.source_location().as_string()
3222-
<< ": error: " << identifier << " expects one operand";
3223-
throw invalid_source_file_exceptiont{error_message.str()};
3222+
error_message << "error: " << identifier << " expects one operand";
3223+
throw invalid_source_file_exceptiont{
3224+
error_message.str(), expr.source_location()};
32243225
}
32253226

32263227
typecheck_function_call_arguments(expr);
@@ -3245,10 +3246,10 @@ exprt c_typecheck_baset::typecheck_builtin_overflow(
32453246
if(expr.arguments().size() != 3)
32463247
{
32473248
std::ostringstream error_message;
3248-
error_message << expr.source_location().as_string() << ": " << identifier
3249-
<< " takes exactly 3 arguments, but "
3249+
error_message << identifier << " takes exactly 3 arguments, but "
32503250
<< expr.arguments().size() << " were provided";
3251-
throw invalid_source_file_exceptiont{error_message.str()};
3251+
throw invalid_source_file_exceptiont{
3252+
error_message.str(), expr.source_location()};
32523253
}
32533254

32543255
typecheck_function_call_arguments(expr);

‎src/ansi-c/c_typecheck_type.cpp

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1198,10 +1198,9 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
11981198
if(!is_signed_or_unsigned_bitvector(underlying_type))
11991199
{
12001200
std::ostringstream msg;
1201-
msg << source_location << ": non-integral type '"
1202-
<< underlying_type.get(ID_C_c_type)
1201+
msg << "non-integral type '" << underlying_type.get(ID_C_c_type)
12031202
<< "' is an invalid underlying type";
1204-
throw invalid_source_file_exceptiont{msg.str()};
1203+
throw invalid_source_file_exceptiont{msg.str(), source_location};
12051204
}
12061205
}
12071206

@@ -1260,11 +1259,9 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
12601259
if(value < tmp.smallest() || value > tmp.largest())
12611260
{
12621261
std::ostringstream msg;
1263-
msg
1264-
<< v.source_location()
1265-
<< ": enumerator value is not representable in the underlying type '"
1266-
<< constant_type.get(ID_C_c_type) << "'";
1267-
throw invalid_source_file_exceptiont{msg.str()};
1262+
msg << "enumerator value is not representable in the underlying type '"
1263+
<< constant_type.get(ID_C_c_type) << "'";
1264+
throw invalid_source_file_exceptiont{msg.str(), v.source_location()};
12681265
}
12691266
}
12701267
else

‎src/ansi-c/literals/convert_character_literal.cpp

Lines changed: 11 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,8 @@ Author: Daniel Kroening, [email protected]
2020

2121
exprt convert_character_literal(
2222
const std::string &src,
23-
bool force_integer_type)
23+
bool force_integer_type,
24+
const source_locationt &source_location)
2425
{
2526
assert(src.size()>=2);
2627

@@ -60,8 +61,10 @@ exprt convert_character_literal(
6061
result=from_integer(x, type);
6162
}
6263
else
63-
throw "wide literals with "+std::to_string(value.size())+
64-
" characters are not supported";
64+
throw invalid_source_file_exceptiont{
65+
"wide literals with " + std::to_string(value.size()) +
66+
" characters are not supported",
67+
source_location};
6568
}
6669
else
6770
{
@@ -93,9 +96,12 @@ exprt convert_character_literal(
9396
result=from_integer(x, signed_int_type());
9497
}
9598
else
96-
throw "literals with "+std::to_string(value.size())+
97-
" characters are not supported";
99+
throw invalid_source_file_exceptiont{
100+
"literals with " + std::to_string(value.size()) +
101+
" characters are not supported",
102+
source_location};
98103
}
99104

105+
result.add_source_location() = source_location;
100106
return result;
101107
}

‎src/ansi-c/literals/convert_character_literal.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
2121

2222
exprt convert_character_literal(
2323
const std::string &src,
24-
bool force_integer_type);
24+
bool force_integer_type,
25+
const source_locationt &source_location);
2526

2627
#endif // CPROVER_ANSI_C_LITERALS_CONVERT_CHARACTER_LITERAL_H

‎src/ansi-c/scanner.l

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -308,8 +308,8 @@ void ansi_c_scanner_init()
308308

309309
<GRAMMAR>{char_lit} {
310310
newstack(yyansi_clval);
311-
parser_stack(yyansi_clval)=convert_character_literal(yytext, true);
312-
PARSER.set_source_location(parser_stack(yyansi_clval));
311+
source_locationt l=parser_stack(yyansi_clval).source_location();
312+
parser_stack(yyansi_clval)=convert_character_literal(yytext, true, l);
313313
return TOK_CHARACTER;
314314
}
315315

‎src/cpp/cpp_typecheck.cpp

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -129,6 +129,12 @@ bool cpp_typecheck(
129129
cpp_typecheck.error() << e << messaget::eom;
130130
}
131131

132+
catch(const invalid_source_file_exceptiont &e)
133+
{
134+
cpp_typecheck.error().source_location = e.get_source_location();
135+
cpp_typecheck.error() << e.get_reason() << messaget::eom;
136+
}
137+
132138
return message_handler.get_message_count(messaget::M_ERROR)!=errors_before;
133139
}
134140

‎src/crangler/mini_c_parser.cpp

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -236,8 +236,12 @@ mini_c_parsert::tokenst mini_c_parsert::parse_pre_declarator()
236236
else if(token == '(') // function type, part of declarator
237237
return result;
238238
else
239+
{
240+
source_locationt loc;
241+
loc.set_line(token.line_number);
239242
throw invalid_source_file_exceptiont(
240-
"expected a declaration but got '" + token.text + "'");
243+
"expected a declaration but got '" + token.text + "'", loc);
244+
}
241245
}
242246
}
243247

@@ -263,7 +267,11 @@ mini_c_parsert::tokenst mini_c_parsert::parse_declarator()
263267
return {consume_token()};
264268
}
265269
else
266-
throw invalid_source_file_exceptiont("expected an identifier");
270+
{
271+
source_locationt loc;
272+
loc.set_line(peek().line_number);
273+
throw invalid_source_file_exceptiont("expected an identifier", loc);
274+
}
267275
}
268276

269277
mini_c_parsert::tokenst mini_c_parsert::parse_post_declarator()

0 commit comments

Comments
 (0)