Skip to content

Commit 1a6f581

Browse files
committed
Avoid default constructing code_{assert,assume}t
The default constructor is deprecated.
1 parent ab81ffc commit 1a6f581

File tree

2 files changed

+3
-5
lines changed

2 files changed

+3
-5
lines changed

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2313,16 +2313,14 @@ void java_bytecode_convert_methodt::convert_athrow(
23132313
// we translate athrow into
23142314
// ASSERT false;
23152315
// ASSUME false:
2316-
code_assertt assert_code;
2317-
assert_code.assertion() = false_exprt();
2316+
code_assertt assert_code(false_exprt{});
23182317
source_locationt assert_location = location; // copy
23192318
assert_location.set_comment("assertion at " + location.as_string());
23202319
assert_location.set("user-provided", true);
23212320
assert_location.set_property_class(ID_assertion);
23222321
assert_code.add_source_location() = assert_location;
23232322

2324-
code_assumet assume_code;
2325-
assume_code.assumption() = false_exprt();
2323+
code_assumet assume_code(false_exprt{});
23262324
source_locationt assume_location = location; // copy
23272325
assume_location.set("user-provided", true);
23282326
assume_code.add_source_location() = assume_location;

src/goto-instrument/wmm/shared_buffers.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -320,7 +320,7 @@ void shared_bufferst::write(
320320
target=goto_program.insert_before(target);
321321
target->guard=cond_expr;
322322
target->type=ASSERT;
323-
target->code=code_assertt();
323+
target->code = code_assertt(cond_expr);
324324
target->code.add_source_location()=source_location;
325325
target->source_location=source_location;
326326
target++;

0 commit comments

Comments
 (0)