Skip to content

Commit 9066460

Browse files
committed
Use immediately invoked lambda to avoid warning
Pushing the warning exception is not a straight forward solution in this case. This is because gcc-12 still generates the warning on read of `contract` instead of on initialisation of `contract`.
1 parent 62358f5 commit 9066460

File tree

1 file changed

+9
-11
lines changed

1 file changed

+9
-11
lines changed

src/cprover/cprover_parse_options.cpp

Lines changed: 9 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -218,17 +218,15 @@ int cprover_parse_optionst::main()
218218
return CPROVER_EXIT_SUCCESS;
219219
}
220220

221-
// gcc produces a spurious warning on optionalt<irep_idt>.
222-
// This will likely go away once we use std::optional<irep_idt>.
223-
// To make clang ignore the pragma, we need to guard it with an ifdef.
224-
#pragma GCC diagnostic push
225-
#ifndef __clang__
226-
# pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
227-
#endif
228-
optionalt<irep_idt> contract = cmdline.isset("contract")
229-
? irep_idt(cmdline.get_value("contract"))
230-
: optionalt<irep_idt>{};
231-
#pragma GCC diagnostic pop
221+
// gcc produces a spurious warning for optionalt<irep_idt> if initialised
222+
// with ternary operator. Initialising with an immediately invoked lamda
223+
// avoids this.
224+
const auto contract = [&]() -> optionalt<irep_idt> {
225+
if(cmdline.isset("contract"))
226+
return {cmdline.get_value("contract")};
227+
else
228+
return {};
229+
}();
232230

233231
if(cmdline.isset("smt2") || cmdline.isset("text") || variable_encoding)
234232
{

0 commit comments

Comments
 (0)