More string abstraction to be common processing of goto-programs

In the case of goto-analyzer and goto-diff this should be dead code.
In CBMC it reverses the order of string abstraction and non-det statics.
It is conceivable that these two interact but this way around is probably
better.

Author: martin

src/cbmc/cbmc_parse_options.cpp

@@ -957,6 +957,12 @@ bool cbmc_parse_optionst::process_goto_program(
   // checks don't know about adjusted float expressions
   adjust_float_expressions(goto_model);
 
+  if(options.get_bool_option("string-abstraction"))
+  {
+    log.status() << "String Abstraction" << messaget::eom;
+    string_abstraction(goto_model, log.get_message_handler());
+  }
+
   // ignore default/user-specified initialization
   // of variables with static lifetime
   if(options.get_bool_option("nondet-static"))
@@ -967,12 +973,6 @@ bool cbmc_parse_optionst::process_goto_program(
     nondet_static(goto_model);
   }
 
-  if(options.get_bool_option("string-abstraction"))
-  {
-    log.status() << "String Abstraction" << messaget::eom;
-    string_abstraction(goto_model, log.get_message_handler());
-  }
-
   // add failed symbols
   // needs to be done before pointer analysis
   add_failed_symbols(goto_model.symbol_table);

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -913,6 +913,12 @@ bool goto_analyzer_parse_optionst::process_goto_program(
     // checks don't know about adjusted float expressions
     adjust_float_expressions(goto_model);
 
+    if(options.get_bool_option("string-abstraction"))
+    {
+      log.status() << "String Abstraction" << messaget::eom;
+      string_abstraction(goto_model, log.get_message_handler());
+    }
+
     // recalculate numbers, etc.
     goto_model.goto_functions.update();
 

src/goto-diff/goto_diff_parse_options.cpp

@@ -310,6 +310,12 @@ bool goto_diff_parse_optionst::process_goto_program(
     // checks don't know about adjusted float expressions
     adjust_float_expressions(goto_model);
 
+    if(options.get_bool_option("string-abstraction"))
+    {
+      log.status() << "String Abstraction" << messaget::eom;
+      string_abstraction(goto_model, log.get_message_handler());
+    }
+
     // recalculate numbers, etc.
     goto_model.goto_functions.update();