Skip to content

Commit 6c368cc

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 ffb9095 commit 6c368cc

14 files changed

+94
-43
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
@@ -65,5 +65,11 @@ bool ansi_c_typecheck(
6565
ansi_c_typecheck.error() << e << messaget::eom;
6666
}
6767

68+
catch(const invalid_source_file_exceptiont &e)
69+
{
70+
ansi_c_typecheck.error().source_location = e.source_location();
71+
ansi_c_typecheck.error() << e.reason() << messaget::eom;
72+
}
73+
6874
return message_handler.get_message_count(messaget::M_ERROR)!=errors_before;
6975
}

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 14 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -2967,21 +2967,22 @@ exprt c_typecheck_baset::do_special_functions(
29672967
if(expr.arguments().size() != 1)
29682968
{
29692969
std::ostringstream error_message;
2970-
error_message << expr.source_location().as_string() << ": " << identifier
2971-
<< " takes exactly 1 argument, but "
2970+
error_message << identifier << " takes exactly 1 argument, but "
29722971
<< expr.arguments().size() << " were provided";
2973-
throw invalid_source_file_exceptiont{error_message.str()};
2972+
throw invalid_source_file_exceptiont{error_message.str(),
2973+
expr.source_location()};
29742974
}
29752975
auto arg1 = expr.arguments()[0];
29762976
typecheck_expr(arg1);
29772977
if(!can_cast_type<c_enum_tag_typet>(arg1.type()))
29782978
{
29792979
// Can't enum range check a non-enum
29802980
std::ostringstream error_message;
2981-
error_message << expr.source_location().as_string() << ": " << identifier
2982-
<< " expects enum, but (" << expr2c(arg1, *this)
2983-
<< ") has type `" << type2c(arg1.type(), *this) << '`';
2984-
throw invalid_source_file_exceptiont{error_message.str()};
2981+
error_message << identifier << " expects enum, but ("
2982+
<< expr2c(arg1, *this) << ") has type `"
2983+
<< type2c(arg1.type(), *this) << '`';
2984+
throw invalid_source_file_exceptiont{error_message.str(),
2985+
expr.source_location()};
29852986
}
29862987
else
29872988
{
@@ -2997,10 +2998,10 @@ exprt c_typecheck_baset::do_special_functions(
29972998
if(expr.arguments().size() != 3)
29982999
{
29993000
std::ostringstream error_message;
3000-
error_message << expr.source_location().as_string() << ": " << identifier
3001-
<< " takes exactly 3 arguments, but "
3001+
error_message << identifier << " takes exactly 3 arguments, but "
30023002
<< expr.arguments().size() << " were provided";
3003-
throw invalid_source_file_exceptiont{error_message.str()};
3003+
throw invalid_source_file_exceptiont{error_message.str(),
3004+
expr.source_location()};
30043005
}
30053006

30063007
auto lhs = expr.arguments()[0];
@@ -3016,13 +3017,13 @@ exprt c_typecheck_baset::do_special_functions(
30163017
[this,
30173018
identifier](const exprt &wrong_argument, std::size_t argument_number) {
30183019
std::ostringstream error_message;
3019-
error_message << wrong_argument.source_location().as_string() << ": "
3020-
<< identifier << " has signature " << identifier
3020+
error_message << identifier << " has signature " << identifier
30213021
<< "(integral, integral, integral*), "
30223022
<< "but argument " << argument_number << " ("
30233023
<< expr2c(wrong_argument, *this) << ") has type `"
30243024
<< type2c(wrong_argument.type(), *this) << '`';
3025-
throw invalid_source_file_exceptiont{error_message.str()};
3025+
throw invalid_source_file_exceptiont{
3026+
error_message.str(), wrong_argument.source_location()};
30263027
};
30273028
for(auto const arg_index : {0, 1})
30283029
{

‎src/ansi-c/c_typecheck_type.cpp

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1195,10 +1195,9 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
11951195
if(!is_signed_or_unsigned_bitvector(underlying_type))
11961196
{
11971197
std::ostringstream msg;
1198-
msg << source_location << ": non-integral type '"
1199-
<< underlying_type.get(ID_C_c_type)
1198+
msg << "non-integral type '" << underlying_type.get(ID_C_c_type)
12001199
<< "' is an invalid underlying type";
1201-
throw invalid_source_file_exceptiont{msg.str()};
1200+
throw invalid_source_file_exceptiont{msg.str(), source_location};
12021201
}
12031202
}
12041203

@@ -1257,11 +1256,9 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
12571256
if(value < tmp.smallest() || value > tmp.largest())
12581257
{
12591258
std::ostringstream msg;
1260-
msg
1261-
<< v.source_location()
1262-
<< ": 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()};
1259+
msg << "enumerator value is not representable in the underlying type '"
1260+
<< constant_type.get(ID_C_c_type) << "'";
1261+
throw invalid_source_file_exceptiont{msg.str(), v.source_location()};
12651262
}
12661263
}
12671264
else

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

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

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

@@ -59,8 +60,10 @@ exprt convert_character_literal(
5960
result=from_integer(x, type);
6061
}
6162
else
62-
throw "wide literals with "+std::to_string(value.size())+
63-
" characters are not supported";
63+
throw invalid_source_file_exceptiont{"wide literals with " +
64+
std::to_string(value.size()) +
65+
" characters are not supported",
66+
source_location};
6467
}
6568
else
6669
{
@@ -92,9 +95,12 @@ exprt convert_character_literal(
9295
result=from_integer(x, signed_int_type());
9396
}
9497
else
95-
throw "literals with "+std::to_string(value.size())+
96-
" characters are not supported";
98+
throw invalid_source_file_exceptiont{"literals with " +
99+
std::to_string(value.size()) +
100+
" characters are not supported",
101+
source_location};
97102
}
98103

104+
result.add_source_location() = source_location;
99105
return result;
100106
}

‎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
@@ -131,6 +131,12 @@ bool cpp_typecheck(
131131
cpp_typecheck.error() << e << messaget::eom;
132132
}
133133

134+
catch(const invalid_source_file_exceptiont &e)
135+
{
136+
cpp_typecheck.error().source_location = e.source_location();
137+
cpp_typecheck.error() << e.reason() << messaget::eom;
138+
}
139+
134140
return message_handler.get_message_count(messaget::M_ERROR)!=errors_before;
135141
}
136142

‎src/goto-cc/goto_cc_mode.cpp

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

‎src/symtab2gb/symtab2gb_parse_options.cpp

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -72,14 +72,18 @@ static void run_symtab2gb(
7272
auto &symtab_file = symtab_files[ix];
7373
if(failed(symtab_language->parse(symtab_file, symtab_filename)))
7474
{
75-
throw invalid_source_file_exceptiont{
76-
"failed to parse symbol table from file '" + symtab_filename + "'"};
75+
source_locationt source_location;
76+
source_location.set_file(symtab_filename);
77+
throw invalid_source_file_exceptiont{"failed to parse symbol table",
78+
source_location};
7779
}
7880
symbol_tablet symtab{};
7981
if(failed(symtab_language->typecheck(symtab, "<unused>")))
8082
{
81-
throw invalid_source_file_exceptiont{
82-
"failed to typecheck symbol table from file '" + symtab_filename + "'"};
83+
source_locationt source_location;
84+
source_location.set_file(symtab_filename);
85+
throw invalid_source_file_exceptiont{"failed to typecheck symbol table",
86+
source_location};
8387
}
8488
goto_modelt goto_model{};
8589
goto_model.symbol_table = symtab;

‎src/util/exception_utils.cpp

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -106,12 +106,14 @@ std::string invalid_input_exceptiont::what() const
106106
}
107107

108108
invalid_source_file_exceptiont::invalid_source_file_exceptiont(
109-
std::string reason)
110-
: reason(std::move(reason))
109+
std::string reason,
110+
source_locationt source_location)
111+
: invalid_input_exceptiont(std::move(reason)),
112+
m_source_location(std::move(source_location))
111113
{
112114
}
113115

114116
std::string invalid_source_file_exceptiont::what() const
115117
{
116-
return reason;
118+
return m_source_location.as_string() + ": " + m_reason;
117119
}

‎src/util/exception_utils.h

Lines changed: 15 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -180,14 +180,26 @@ class invalid_input_exceptiont : public cprover_exception_baset
180180
/// Thrown when we can't handle something in an input source file.
181181
/// For example, if we get C source code that is not syntactically valid
182182
/// or that has type errors.
183-
class invalid_source_file_exceptiont : public cprover_exception_baset
183+
class invalid_source_file_exceptiont : public invalid_input_exceptiont
184184
{
185185
public:
186-
explicit invalid_source_file_exceptiont(std::string reason);
186+
invalid_source_file_exceptiont(
187+
std::string reason,
188+
source_locationt source_location);
187189
std::string what() const override;
188190

191+
const std::string &reason() const
192+
{
193+
return m_reason;
194+
}
195+
196+
const source_locationt &source_location() const
197+
{
198+
return m_source_location;
199+
}
200+
189201
private:
190-
std::string reason;
202+
source_locationt m_source_location;
191203
};
192204

193205
#endif // CPROVER_UTIL_EXCEPTION_UTILS_H

‎src/util/typecheck.cpp

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]
88

99
#include "typecheck.h"
1010

11+
#include "exception_utils.h"
1112
#include "invariant.h"
1213

1314
bool typecheckt::typecheck_main()
@@ -37,5 +38,11 @@ bool typecheckt::typecheck_main()
3738
error() << e << eom;
3839
}
3940

41+
catch(const invalid_source_file_exceptiont &e)
42+
{
43+
error().source_location = e.source_location();
44+
error() << e.reason() << messaget::eom;
45+
}
46+
4047
return message_handler->get_message_count(messaget::M_ERROR)!=errors_before;
4148
}

0 commit comments

Comments
 (0)