Rename core?goto to symex?ready?goto

This does a rename from the term "core goto" to "symex ready goto"
to more accurately denote what this goto form is.

Renaming also updates documentation.

Author: TGWDB

doc/ADR/README.md

@@ -6,8 +6,8 @@ where taken at the time they were, so that future maintainers
 can more easily identify constraints that shaped the architecture
 of the system and the surrounding infrastructure.
 
-## Core goto form
-\subpage core-goto
+## Symex ready goto form
+\subpage symex-ready-goto
 
 ## Release & Packaging
 

doc/ADR/core_goto.md doc/ADR/symex_ready_goto.mddoc/ADR/core_goto.md renamed to doc/ADR/symex_ready_goto.md

@@ -1,13 +1,13 @@
-\page core-goto Core goto definition
+\page symex-ready-goto Symex ready goto definition
 
 During the analysis of a program CBMC transforms the input program in an intermediate language
 called extended goto. Then the tool performs a series of simplifications on the obtained goto
 program until the program is given to the solver.
 
-We say that a program is in the **core goto form** when all the extended goto features have
+We say that a program is in the **symex ready goto form** when all the extended goto features have
 been simplified.
 
-More specifically, a program that is in **core goto form** is one that can be passed to **symex** by
+More specifically, a program that is in **symex ready goto form** is one that can be passed to **symex** by
 using any solver deriving from `goto_verifiert` without requiring any lowering step.
 
 At the time of writing, verifiers extending `goto_verifiert` are:

doc/architectural/goto-program-transformations.md

@@ -5,7 +5,7 @@
 \section required-transforms Core Transformation Passes
 
 This section lists the transformation passes that must have been applied for the
-goto model to be in core goto format.
+goto model to be in symex ready goto format.
 
 Note that the passes are listed below in the order they are currently called in
 CBMC. While all dependencies on the ordering are not fully documented, the
@@ -184,11 +184,11 @@ nondet-transform if it is being used.</em>
 
 This transformation removes skip instructions. Note that this transformation is
 called in many places and may be called as part of other transformations. This
-instance here is part of the mandatory transformation to reach core goto format.
-If there is a use case where it is desirable to preserve a "no operation"
-instruction, a `LOCATION` type instruction may be used in place of a `SKIP`
-instruction. The `LOCATION` instruction has the same semantics as the `SKIP`
-instruction, but is not removed by the remove skip instructions pass.
+instance here is part of the mandatory transformation to reach symex ready goto
+format. If there is a use case where it is desirable to preserve a "no
+operation" instruction, a `LOCATION` type instruction may be used in place of a
+`SKIP` instruction. The `LOCATION` instruction has the same semantics as the
+`SKIP` instruction, but is not removed by the remove skip instructions pass.
 
 The implementation of this pass is called via \ref remove_skip(goto_modelt &)
 
@@ -215,7 +215,7 @@ coverage-transform if it is being used.</em>
 
 The sections lists the optional transformation passes that are optional and will
 modify a goto model. Note that these are documented here for consistency, but
-not required for core goto format.
+not required for symex ready goto format.
 
 Note for each optional pass there is a listed predeceesor pass. This is the pass
 currently called before the listed pass in CBMC. While the ordering may not be

regression/cbmc/export-core-goto/test-bad-usage.desc

@@ -0,0 +1,9 @@
+CORE
+test.c
+--export-symex-ready-goto ""
+^ERROR: Please provide a filename to write the goto-binary to.$
+^EXIT=6$
+^SIGNAL=0$
+--
+--
+Ensure that --export-symex-ready-goto exported.symex-ready.goto terminates with error when incorrectly used.

regression/cbmc/export-core-goto/test-correct.desc

@@ -0,0 +1,15 @@
+CORE
+test.c
+--export-symex-ready-goto exported.symex.ready.goto
+^Parsing test.c$
+^Converting$
+^Type-checking test$
+^Generating GOTO Program$
+^Removal of function pointers and virtual functions$
+^Generic Property Instrumentation$
+Exported goto-program in symex-ready-goto form at exported.symex.ready.goto
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Ensure that --export-symex-ready-goto exported.symex.ready.goto terminates successfully and logs this.

regression/cbmc/export-symex-ready-goto/test-bad-usage.desc

@@ -245,11 +245,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("trace", true);
   }
 
-  if(cmdline.isset("export-core-goto"))
+  if(cmdline.isset("export-symex-ready-goto"))
   {
     options.set_option(
-      "export-core-goto", cmdline.get_value("export-core-goto"));
-    if(options.get_option("export-core-goto").empty())
+      "export-symex-ready-goto", cmdline.get_value("export-symex-ready-goto"));
+    if(options.get_option("export-symex-ready-goto").empty())
     {
       log.error()
         << "ERROR: Please provide a filename to write the goto-binary to."
@@ -559,26 +559,27 @@ int cbmc_parse_optionst::doit()
   if(set_properties())
     return CPROVER_EXIT_SET_PROPERTIES_FAILED;
 
-  // At this point, our goto-model should be in core-goto form (all of the
+  // At this point, our goto-model should be in symex-ready-goto form (all of the
   // transformations have been run and the program is ready to be given to the
   // solver).
-  if(options.is_set("export-core-goto"))
+  if(options.is_set("export-symex-ready-goto"))
   {
-    auto core_goto_filename = options.get_option("export-core-goto");
+    auto symex_ready_goto_filename =
+      options.get_option("export-symex-ready-goto");
 
-    bool success =
-      !write_goto_binary(core_goto_filename, goto_model, ui_message_handler);
+    bool success = !write_goto_binary(
+      symex_ready_goto_filename, goto_model, ui_message_handler);
 
     if(!success)
     {
       log.error() << "ERROR: Unable to export goto-program in file "
-                  << core_goto_filename << messaget::eom;
+                  << symex_ready_goto_filename << messaget::eom;
       return CPROVER_EXIT_INTERNAL_ERROR;
     }
     else
     {
-      log.status() << "Exported goto-program in core-goto form at "
-                   << core_goto_filename << messaget::eom;
+      log.status() << "Exported goto-program in symex-ready-goto form at "
+                   << symex_ready_goto_filename << messaget::eom;
       return CPROVER_EXIT_SUCCESS;
     }
   }
@@ -967,7 +968,7 @@ void cbmc_parse_optionst::help()
     " --show-symbol-table          show loaded symbol table\n"
     HELP_SHOW_GOTO_FUNCTIONS
     HELP_VALIDATE
-    " --export-core-goto f         serialise goto-program in core-goto form in f\n" // NOLINT(*)
+    " --export-symex-ready-goto f         serialise goto-program in symex-ready-goto form in f\n" // NOLINT(*)
     "\n"
     "Program instrumentation options:\n"
     HELP_GOTO_CHECK

regression/cbmc/export-symex-ready-goto/test-correct.desc

@@ -59,7 +59,7 @@ class optionst;
   "(verbosity):(no-library)" \
   "(nondet-static)" \
   "(version)" \
-  "(export-core-goto):" \
+  "(export-symex-ready-goto):" \
   OPT_COVER \
   "(symex-coverage-report):" \
   "(mm):" \