From 1a6f581d5c9441db2d93780e0920085799a0d123 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 25 Jan 2019 10:34:06 +0000 Subject: [PATCH] Avoid default constructing code_{assert,assume}t The default constructor is deprecated. --- jbmc/src/java_bytecode/java_bytecode_convert_method.cpp | 6 ++---- src/goto-instrument/wmm/shared_buffers.cpp | 2 +- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 87055431405..f79e434f08c 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -2313,16 +2313,14 @@ void java_bytecode_convert_methodt::convert_athrow( // we translate athrow into // ASSERT false; // ASSUME false: - code_assertt assert_code; - assert_code.assertion() = false_exprt(); + code_assertt assert_code(false_exprt{}); source_locationt assert_location = location; // copy assert_location.set_comment("assertion at " + location.as_string()); assert_location.set("user-provided", true); assert_location.set_property_class(ID_assertion); assert_code.add_source_location() = assert_location; - code_assumet assume_code; - assume_code.assumption() = false_exprt(); + code_assumet assume_code(false_exprt{}); source_locationt assume_location = location; // copy assume_location.set("user-provided", true); assume_code.add_source_location() = assume_location; diff --git a/src/goto-instrument/wmm/shared_buffers.cpp b/src/goto-instrument/wmm/shared_buffers.cpp index e575f613d9c..b88201f8353 100644 --- a/src/goto-instrument/wmm/shared_buffers.cpp +++ b/src/goto-instrument/wmm/shared_buffers.cpp @@ -320,7 +320,7 @@ void shared_bufferst::write( target=goto_program.insert_before(target); target->guard=cond_expr; target->type=ASSERT; - target->code=code_assertt(); + target->code = code_assertt(cond_expr); target->code.add_source_location()=source_location; target->source_location=source_location; target++;