Skip to content

Commit 2ff58a9

Browse files
authored
Merge pull request #3934 from tautschnig/deprecation-assert-assume
Avoid default constructing code_{assert,assume}t [blocks: #3800]
2 parents 71bdebf + 1a6f581 commit 2ff58a9

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
@@ -2312,16 +2312,14 @@ void java_bytecode_convert_methodt::convert_athrow(
23122312
// we translate athrow into
23132313
// ASSERT false;
23142314
// ASSUME false:
2315-
code_assertt assert_code;
2316-
assert_code.assertion() = false_exprt();
2315+
code_assertt assert_code(false_exprt{});
23172316
source_locationt assert_location = location; // copy
23182317
assert_location.set_comment("assertion at " + location.as_string());
23192318
assert_location.set("user-provided", true);
23202319
assert_location.set_property_class(ID_assertion);
23212320
assert_code.add_source_location() = assert_location;
23222321

2323-
code_assumet assume_code;
2324-
assume_code.assumption() = false_exprt();
2322+
code_assumet assume_code(false_exprt{});
23252323
source_locationt assume_location = location; // copy
23262324
assume_location.set("user-provided", true);
23272325
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
@@ -322,7 +322,7 @@ void shared_bufferst::write(
322322
target=goto_program.insert_before(target);
323323
target->guard=cond_expr;
324324
target->type=ASSERT;
325-
target->code=code_assertt();
325+
target->code = code_assertt(cond_expr);
326326
target->code.add_source_location()=source_location;
327327
target->source_location=source_location;
328328
target++;

0 commit comments

Comments
 (0)