Skip to content

Commit f0a7f1f

Browse files
committed
Add source location parameter to get_nondet_bool()
1 parent 493fcda commit f0a7f1f

File tree

2 files changed

+7
-4
lines changed

2 files changed

+7
-4
lines changed

jbmc/src/java_bytecode/java_object_factory.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1212,7 +1212,7 @@ void java_object_factoryt::gen_nondet_init(
12121212
{
12131213
// types different from pointer or structure:
12141214
// bool, int, float, byte, char, ...
1215-
exprt rhs = type.id() == ID_c_bool ? get_nondet_bool(type)
1215+
exprt rhs = type.id() == ID_c_bool ? get_nondet_bool(type, loc)
12161216
: side_effect_expr_nondett(type, loc);
12171217
code_assignt assign(expr, rhs);
12181218
assign.add_source_location()=loc;

src/util/nondet_bool.h

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,14 +15,17 @@ Author: Chris Smowton, [email protected]
1515
#include "std_expr.h"
1616
#include "std_types.h"
1717

18-
/// \par parameters: Desired type (C_bool or plain bool)
18+
/// \param type desired type (C_bool or plain bool)
19+
/// \param source_location source location
1920
/// \return nondet expr of that type
20-
inline exprt get_nondet_bool(const typet &type)
21+
inline exprt get_nondet_bool(
22+
const typet &type,
23+
const source_locationt &source_location)
2124
{
2225
// We force this to 0 and 1 and won't consider
2326
// other values.
2427
return typecast_exprt(
25-
side_effect_expr_nondett(bool_typet(), source_locationt()), type);
28+
side_effect_expr_nondett(bool_typet(), source_location), type);
2629
}
2730

2831
#endif // CPROVER_UTIL_NONDET_BOOL_H

0 commit comments

Comments
 (0)