Skip to content

Commit 0470384

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 d7342aa commit 0470384

File tree

19 files changed

+127
-79
lines changed

19 files changed

+127
-79
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$

‎regression/cbmc/gcc_builtin_add_overflow/type-conflict.desc‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
type-conflict.c
33
-DCONFLICT1
4-
line 12 function main: __builtin_add_overflow has signature __builtin_add_overflow\(integral, integral, integral\*\), but argument 3 \(r\) has type `signed int`$
4+
line 12 function main: error: __builtin_add_overflow has signature __builtin_add_overflow\(integral, integral, integral\*\), but argument 3 \(r\) has type `signed int`$
55
^EXIT=6$
66
^SIGNAL=0$

‎regression/cbmc/saturating_arithmetric/typeconflict.desc‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
typeconflict.c
3-
file typeconflict.c line 3 function main: __CPROVER_saturating_minus takes exactly two arguments, but 1 were provided
3+
file typeconflict.c line 3 function main: error: __CPROVER_saturating_minus takes exactly two arguments, but 1 were provided
44
^EXIT=6$
55
^SIGNAL=0$
66
--

‎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: 22 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -3170,21 +3170,22 @@ exprt c_typecheck_baset::do_special_functions(
31703170
if(expr.arguments().size() != 1)
31713171
{
31723172
std::ostringstream error_message;
3173-
error_message << expr.source_location().as_string() << ": " << identifier
3174-
<< " takes exactly 1 argument, but "
3173+
error_message << identifier << " takes exactly 1 argument, but "
31753174
<< expr.arguments().size() << " were provided";
3176-
throw invalid_source_file_exceptiont{error_message.str()};
3175+
throw invalid_source_file_exceptiont{
3176+
error_message.str(), expr.source_location()};
31773177
}
31783178
auto arg1 = expr.arguments()[0];
31793179
typecheck_expr(arg1);
31803180
if(!can_cast_type<c_enum_tag_typet>(arg1.type()))
31813181
{
31823182
// Can't enum range check a non-enum
31833183
std::ostringstream error_message;
3184-
error_message << expr.source_location().as_string() << ": " << identifier
3185-
<< " expects enum, but (" << expr2c(arg1, *this)
3186-
<< ") has type `" << type2c(arg1.type(), *this) << '`';
3187-
throw invalid_source_file_exceptiont{error_message.str()};
3184+
error_message << identifier << " expects enum, but ("
3185+
<< expr2c(arg1, *this) << ") has type `"
3186+
<< type2c(arg1.type(), *this) << '`';
3187+
throw invalid_source_file_exceptiont{
3188+
error_message.str(), expr.source_location()};
31883189
}
31893190
else
31903191
{
@@ -3237,9 +3238,9 @@ exprt c_typecheck_baset::do_special_functions(
32373238
if(expr.arguments().size() != 1)
32383239
{
32393240
std::ostringstream error_message;
3240-
error_message << expr.source_location().as_string()
3241-
<< ": error: " << identifier << " expects one operand";
3242-
throw invalid_source_file_exceptiont{error_message.str()};
3241+
error_message << "error: " << identifier << " expects one operand";
3242+
throw invalid_source_file_exceptiont{
3243+
error_message.str(), expr.source_location()};
32433244
}
32443245

32453246
typecheck_function_call_arguments(expr);
@@ -3264,10 +3265,10 @@ exprt c_typecheck_baset::typecheck_builtin_overflow(
32643265
if(expr.arguments().size() != 3)
32653266
{
32663267
std::ostringstream error_message;
3267-
error_message << expr.source_location().as_string() << ": " << identifier
3268-
<< " takes exactly 3 arguments, but "
3268+
error_message << identifier << " takes exactly 3 arguments, but "
32693269
<< expr.arguments().size() << " were provided";
3270-
throw invalid_source_file_exceptiont{error_message.str()};
3270+
throw invalid_source_file_exceptiont{
3271+
error_message.str(), expr.source_location()};
32713272
}
32723273

32733274
typecheck_function_call_arguments(expr);
@@ -3283,14 +3284,14 @@ exprt c_typecheck_baset::typecheck_builtin_overflow(
32833284
[this, identifier](
32843285
const exprt &wrong_argument, std::size_t argument_number, bool _p) {
32853286
std::ostringstream error_message;
3286-
error_message << wrong_argument.source_location().as_string() << ": "
3287-
<< identifier << " has signature " << identifier
3288-
<< "(integral, integral, integral" << (_p ? "" : "*")
3289-
<< "), "
3287+
error_message << "error: " << identifier << " has signature "
3288+
<< identifier << "(integral, integral, integral"
3289+
<< (_p ? "" : "*") << "), "
32903290
<< "but argument " << argument_number << " ("
32913291
<< expr2c(wrong_argument, *this) << ") has type `"
32923292
<< type2c(wrong_argument.type(), *this) << '`';
3293-
throw invalid_source_file_exceptiont{error_message.str()};
3293+
throw invalid_source_file_exceptiont{
3294+
error_message.str(), wrong_argument.source_location()};
32943295
};
32953296
for(int arg_index = 0; arg_index <= (!is__p_variant ? 1 : 2); ++arg_index)
32963297
{
@@ -3326,10 +3327,11 @@ exprt c_typecheck_baset::typecheck_saturating_arithmetic(
33263327
if(expr.arguments().size() != 2)
33273328
{
33283329
std::ostringstream error_message;
3329-
error_message << expr.source_location().as_string() << ": " << identifier
3330+
error_message << "error: " << identifier
33303331
<< " takes exactly two arguments, but "
33313332
<< expr.arguments().size() << " were provided";
3332-
throw invalid_source_file_exceptiont{error_message.str()};
3333+
throw invalid_source_file_exceptiont{
3334+
error_message.str(), expr.source_location()};
33333335
}
33343336

33353337
exprt result;

‎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, kroening@kroening.com
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, kroening@kroening.com
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: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -307,9 +307,9 @@ void ansi_c_scanner_init()
307307
}
308308

309309
<GRAMMAR>{char_lit} {
310-
newstack(yyansi_clval);
311-
parser_stack(yyansi_clval)=convert_character_literal(yytext, true);
312-
PARSER.set_source_location(parser_stack(yyansi_clval));
310+
loc();
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

0 commit comments

Comments
 (0)