Skip to content

Commit f85650c

Browse files
committed
Add check on alloca being declared as expected when called
Note that `throw 0;` is used for error handling in order to match the code pattern used in the rest of the file, despite not being best practice.
1 parent 5af3b3a commit f85650c

File tree

1 file changed

+17
-0
lines changed

1 file changed

+17
-0
lines changed

src/goto-programs/builtin_functions.cpp

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -706,6 +706,23 @@ void goto_convertt::do_alloca(
706706
const source_locationt &source_location = function.source_location();
707707
const auto alloca_type = to_code_type(function.type());
708708

709+
if(alloca_type.return_type() != pointer_type(void_type()))
710+
{
711+
error().source_location = source_location;
712+
error() << "'alloca' function called, but 'alloca' has not been declared "
713+
<< "with expected 'void *' return type." << eom;
714+
throw 0;
715+
}
716+
if(
717+
alloca_type.parameters().size() != 1 ||
718+
alloca_type.parameters()[0].type() != size_type())
719+
{
720+
error().source_location = source_location;
721+
error() << "'alloca' function called, but 'alloca' has not been declared "
722+
<< "with expected single 'size_t' parameter." << eom;
723+
throw 0;
724+
}
725+
709726
exprt new_lhs = lhs;
710727

711728
// make sure we have a left-hand side to track the allocation even when the

0 commit comments

Comments
 (0)