Skip to content

Commit 5323702

Browse files
author
Joel Allred
committed
Fix bad return type of char pointer func
We cast the return type of ID_cprover_string_array_of_char_pointer_func so that it matches its expected return type. This addresses: diffblue/platform#975
1 parent ce83039 commit 5323702

File tree

1 file changed

+6
-1
lines changed

1 file changed

+6
-1
lines changed

src/solvers/refinement/string_constraint_generator_main.cpp

+6-1
Original file line numberDiff line numberDiff line change
@@ -684,7 +684,12 @@ exprt string_constraint_generatort::add_axioms_for_char_pointer(
684684
{
685685
exprt char_pointer=args(fun, 1)[0];
686686
if(char_pointer.id()==ID_index)
687-
return char_pointer.op0();
687+
return typecast_exprt(char_pointer.op0(), fun.type());
688+
// TODO: It seems reasonable that the result of the function application
689+
// should match the return type of the function. However it is not
690+
// clear whether this typecast is properly handled in the string
691+
// refinement. We need regression tests that use that function.
692+
688693
// TODO: we do not know what to do in the other cases
689694
assert(false);
690695
return exprt();

0 commit comments

Comments
 (0)