From ec133099c04d6d0170dcffd8ef8ce4ccbdf859f8 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Thu, 23 Feb 2023 12:14:42 -0800 Subject: [PATCH 1/2] Minor formatting fix to contracts help --- src/goto-instrument/contracts/dynamic-frames/dfcc.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc.h b/src/goto-instrument/contracts/dynamic-frames/dfcc.h index 7ef25c5b287..ae0e58160e4 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc.h @@ -58,8 +58,8 @@ class optionst; // clang-format off #define HELP_DFCC \ - "--dfcc activate dynamic frame condition checking for function\n"\ - " contracts using the given harness as entry point" + " --dfcc activate dynamic frame condition checking for function\n"\ + " contracts using the given harness as entry point\n" #define FLAG_ENFORCE_CONTRACT_REC "enforce-contract-rec" #define OPT_ENFORCE_CONTRACT_REC "(" FLAG_ENFORCE_CONTRACT_REC "):" @@ -67,7 +67,7 @@ class optionst; " --enforce-contract-rec [/]" \ " wrap fun with an assertion of the contract\n"\ " and assume recursive calls to fun satisfy \n"\ - " the contract" + " the contract\n" // clang-format on /// Exception thrown for bad function/contract specification pairs passed on From e663f8af973ce799e1cd575022e81b7c6974498f Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Thu, 23 Feb 2023 17:49:31 -0800 Subject: [PATCH 2/2] Align and reformat long lines --- src/goto-instrument/contracts/dynamic-frames/dfcc.h | 5 +++-- src/goto-instrument/goto_instrument_parse_options.cpp | 4 ++-- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc.h b/src/goto-instrument/contracts/dynamic-frames/dfcc.h index ae0e58160e4..93c45dcb1b3 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc.h @@ -58,8 +58,9 @@ class optionst; // clang-format off #define HELP_DFCC \ - " --dfcc activate dynamic frame condition checking for function\n"\ - " contracts using the given harness as entry point\n" + " --dfcc activate dynamic frame condition checking\n"\ + " for function contracts using the given\n"\ + " harness as entry point\n" #define FLAG_ENFORCE_CONTRACT_REC "enforce-contract-rec" #define OPT_ENFORCE_CONTRACT_REC "(" FLAG_ENFORCE_CONTRACT_REC "):" diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 7d94927ae32..13903597f8d 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1980,11 +1980,11 @@ void goto_instrument_parse_optionst::help() " used with aggressive-slice, preserves all functions within function calls\n" // NOLINT(*) " of the functions on the shortest path\n" " --aggressive-slice-preserve-function \n" - " force the aggressive slicer to preserve function \n" // NOLINT(*) + " force the aggressive slicer to preserve function \n" // NOLINT(*) " --aggressive-slice-preserve-functions-containing \n" " force the aggressive slicer to preserve all functions with names containing \n" // NOLINT(*) " --aggressive-slice-preserve-all-direct-paths \n" - " force aggressive slicer to preserve all direct paths\n" // NOLINT(*) + " force aggressive slicer to preserve all direct paths\n" // NOLINT(*) "\n" "Code contracts:\n" HELP_DFCC