Skip to content

Commit 0a6a600

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 7e5f1ac commit 0a6a600

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()

‎src/goto-cc/goto_cc_mode.cpp

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -111,6 +111,15 @@ int goto_cc_modet::main(int argc, const char **argv)
111111
log.error() << "Out of memory" << messaget::eom;
112112
return EX_SOFTWARE;
113113
}
114+
115+
catch(const invalid_source_file_exceptiont &e)
116+
{
117+
messaget log{message_handler};
118+
log.error().source_location = e.get_source_location();
119+
log.error() << e.get_reason() << messaget::eom;
120+
return EX_SOFTWARE;
121+
}
122+
114123
catch(const cprover_exception_baset &e)
115124
{
116125
messaget log{message_handler};

‎src/goto-programs/string_instrumentation.cpp

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -266,7 +266,7 @@ void string_instrumentationt::do_sprintf(
266266
{
267267
if(arguments.size()<2)
268268
{
269-
throw incorrect_source_program_exceptiont(
269+
throw invalid_source_file_exceptiont(
270270
"sprintf expected to have two or more arguments",
271271
target->source_location());
272272
}
@@ -302,7 +302,7 @@ void string_instrumentationt::do_snprintf(
302302
{
303303
if(arguments.size()<3)
304304
{
305-
throw incorrect_source_program_exceptiont(
305+
throw invalid_source_file_exceptiont(
306306
"snprintf expected to have three or more arguments",
307307
target->source_location());
308308
}
@@ -339,7 +339,7 @@ void string_instrumentationt::do_fscanf(
339339
{
340340
if(arguments.size()<2)
341341
{
342-
throw incorrect_source_program_exceptiont(
342+
throw invalid_source_file_exceptiont(
343343
"fscanf expected to have two or more arguments",
344344
target->source_location());
345345
}
@@ -615,7 +615,7 @@ void string_instrumentationt::do_strchr(
615615
{
616616
if(arguments.size()!=2)
617617
{
618-
throw incorrect_source_program_exceptiont(
618+
throw invalid_source_file_exceptiont(
619619
"strchr expected to have two arguments", target->source_location());
620620
}
621621

@@ -639,7 +639,7 @@ void string_instrumentationt::do_strrchr(
639639
{
640640
if(arguments.size()!=2)
641641
{
642-
throw incorrect_source_program_exceptiont(
642+
throw invalid_source_file_exceptiont(
643643
"strrchr expected to have two arguments", target->source_location());
644644
}
645645

@@ -663,7 +663,7 @@ void string_instrumentationt::do_strstr(
663663
{
664664
if(arguments.size()!=2)
665665
{
666-
throw incorrect_source_program_exceptiont(
666+
throw invalid_source_file_exceptiont(
667667
"strstr expected to have two arguments", target->source_location());
668668
}
669669

@@ -693,7 +693,7 @@ void string_instrumentationt::do_strtok(
693693
{
694694
if(arguments.size()!=2)
695695
{
696-
throw incorrect_source_program_exceptiont(
696+
throw invalid_source_file_exceptiont(
697697
"strtok expected to have two arguments", target->source_location());
698698
}
699699

‎src/goto-programs/string_instrumentation.h

Lines changed: 0 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -12,33 +12,12 @@ Author: Daniel Kroening, [email protected]
1212
#ifndef CPROVER_GOTO_PROGRAMS_STRING_INSTRUMENTATION_H
1313
#define CPROVER_GOTO_PROGRAMS_STRING_INSTRUMENTATION_H
1414

15-
#include <util/exception_utils.h>
16-
1715
class exprt;
1816
class goto_functionst;
1917
class goto_modelt;
2018
class goto_programt;
2119
class symbol_tablet;
2220

23-
class incorrect_source_program_exceptiont : public cprover_exception_baset
24-
{
25-
public:
26-
incorrect_source_program_exceptiont(
27-
std::string message,
28-
source_locationt source_location)
29-
: cprover_exception_baset(std::move(message)),
30-
source_location(std::move(source_location))
31-
{
32-
}
33-
std::string what() const override
34-
{
35-
return reason + " (at: " + source_location.as_string() + ")";
36-
}
37-
38-
private:
39-
source_locationt source_location;
40-
};
41-
4221
void string_instrumentation(
4322
symbol_tablet &,
4423
goto_programt &);

‎src/symtab2gb/symtab2gb_parse_options.cpp

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -77,14 +77,18 @@ static void run_symtab2gb(
7777
auto &symtab_file = symtab_files[ix];
7878
if(failed(symtab_language->parse(symtab_file, symtab_filename)))
7979
{
80+
source_locationt source_location;
81+
source_location.set_file(symtab_filename);
8082
throw invalid_source_file_exceptiont{
81-
"failed to parse symbol table from file '" + symtab_filename + "'"};
83+
"failed to parse symbol table", source_location};
8284
}
8385
symbol_tablet symtab{};
8486
if(failed(symtab_language->typecheck(symtab, "<unused>")))
8587
{
88+
source_locationt source_location;
89+
source_location.set_file(symtab_filename);
8690
throw invalid_source_file_exceptiont{
87-
"failed to typecheck symbol table from file '" + symtab_filename + "'"};
91+
"failed to typecheck symbol table", source_location};
8892
}
8993
config.set_from_symbol_table(symtab);
9094

‎src/util/exception_utils.cpp

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -91,7 +91,14 @@ std::string invalid_input_exceptiont::what() const
9191
}
9292

9393
invalid_source_file_exceptiont::invalid_source_file_exceptiont(
94-
std::string reason)
95-
: cprover_exception_baset(std::move(reason))
94+
std::string reason,
95+
source_locationt source_location)
96+
: invalid_input_exceptiont(std::move(reason)),
97+
source_location(std::move(source_location))
98+
{
99+
}
100+
101+
std::string invalid_source_file_exceptiont::what() const
96102
{
103+
return source_location.as_string() + ": " + reason;
97104
}

‎src/util/exception_utils.h

Lines changed: 18 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -172,10 +172,26 @@ class invalid_input_exceptiont : public cprover_exception_baset
172172
/// Thrown when we can't handle something in an input source file.
173173
/// For example, if we get C source code that is not syntactically valid
174174
/// or that has type errors.
175-
class invalid_source_file_exceptiont : public cprover_exception_baset
175+
class invalid_source_file_exceptiont : public invalid_input_exceptiont
176176
{
177177
public:
178-
explicit invalid_source_file_exceptiont(std::string reason);
178+
invalid_source_file_exceptiont(
179+
std::string reason,
180+
source_locationt source_location);
181+
std::string what() const override;
182+
183+
const std::string &get_reason() const
184+
{
185+
return reason;
186+
}
187+
188+
const source_locationt &get_source_location() const
189+
{
190+
return source_location;
191+
}
192+
193+
private:
194+
source_locationt source_location;
179195
};
180196

181197
#endif // CPROVER_UTIL_EXCEPTION_UTILS_H

0 commit comments

Comments
 (0)