Fix for Clang's initialization warning

peterschrammel · peterschrammel · commit 802e0059f675 · 2017-01-12T12:22:47.000Z
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
@@ -346,8 +346,8 @@ void bmct::slice()
       }
     }
   }
-  statistics() << "Generated " << symex.total_vccs
-               << " VCC(s), " << symex.remaining_vccs
+  statistics() << "Generated " << symex().total_vccs
+               << " VCC(s), " << symex().remaining_vccs
                << " remaining after simplification" << eom;
 }
 
@@ -510,12 +510,12 @@ safety_checkert::resultt bmct::initialize()
     return ERROR;
   }
 
-  symex.set_message_handler(get_message_handler());
-  symex.options=options;
+  symex().set_message_handler(get_message_handler());
+  symex().options=options;
 
   status() << "Starting Bounded Model Checking" << eom;
 
-  symex.last_source_location.make_nil();
+  symex().last_source_location.make_nil();
 
   // get unwinding info
   setup_unwind();
@@ -540,7 +540,7 @@ safety_checkert::resultt bmct::step(const goto_functionst &goto_functions)
   try
   {
     // perform symbolic execution
-    symex(goto_functions);
+    symex()(goto_functions);
 
     // add a partial ordering, if required
     if(equation.has_threads())
@@ -575,8 +575,8 @@ safety_checkert::resultt bmct::step(const goto_functionst &goto_functions)
   slice();
 
   {
-    statistics() << "Generated " << symex.total_vccs
-                 << " VCC(s), " << symex.remaining_vccs
+    statistics() << "Generated " << symex().total_vccs
+                 << " VCC(s), " << symex().remaining_vccs
                  << " remaining after simplification" << eom;
   }
 
@@ -604,7 +604,7 @@ safety_checkert::resultt bmct::step(const goto_functionst &goto_functions)
 
   // any properties to check at all?
   if(!options.get_bool_option("program-only") &&
-     symex.remaining_vccs==0)
+     symex().remaining_vccs==0)
   {
     report_success();
     output_graphml(SAFE, goto_functions);
@@ -729,12 +729,12 @@ void bmct::setup_unwind()
       long uw=unsafe_string2int(val.substr(val.rfind(":")+1));
 
       if(thread_nr_set)
-        symex.set_unwind_thread_loop_limit(thread_nr, id, uw);
+        symex().set_unwind_thread_loop_limit(thread_nr, id, uw);
       else
-        symex.set_unwind_loop_limit(id, uw);
+        symex().set_unwind_loop_limit(id, uw);
     }
   }
 
   if(options.get_option("unwind")!="")
-    symex.set_unwind_limit(options.get_unsigned_int_option("unwind"));
+    symex().set_unwind_limit(options.get_unsigned_int_option("unwind"));
 }
diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h
@@ -42,10 +42,9 @@ class bmct:public safety_checkert
     equation(ns),
     symex_ptr(new symex_bmct(ns, new_symbol_table, equation)),
     prop_conv(_prop_conv),
-    ui(ui_message_handlert::PLAIN),
-    symex(*symex_ptr)
+    ui(ui_message_handlert::PLAIN)
   {
-    symex.constant_propagation=options.get_bool_option("propagation");
+    symex().constant_propagation=options.get_bool_option("propagation");
   }
 
   virtual ~bmct() { }
@@ -73,22 +72,20 @@ class bmct:public safety_checkert
   }
 
 protected:
+  // for initialization of derived classes
   bmct(
     const optionst &_options,
     const symbol_tablet &_symbol_table,
-    message_handlert &_message_handler,
     prop_convt& _prop_conv,
-    symex_bmct *_symex_ptr):
+    message_handlert &_message_handler):
     safety_checkert(ns, _message_handler),
     options(_options),
     ns(_symbol_table, new_symbol_table),
     equation(ns),
-    symex_ptr(_symex_ptr),
+    symex_ptr(NULL),
     prop_conv(_prop_conv),
-    ui(ui_message_handlert::PLAIN),
-    symex(dynamic_cast<symex_bmct &>(*symex_ptr))
+    ui(ui_message_handlert::PLAIN)
   {
-    symex.constant_propagation=options.get_bool_option("propagation");
   }
 
   const optionst &options;
@@ -149,7 +146,12 @@ class bmct:public safety_checkert
   friend class fault_localizationt;
 
 private:
-  symex_bmct &symex;
+  // We cannot use a reference member here
+  // because the initialization sequence would not be clean (Clang complains)
+  symex_bmct &symex()
+  {
+    return dynamic_cast<symex_bmct &>(*symex_ptr);
+  }
 };
 
 #endif // CPROVER_CBMC_BMC_H
diff --git a/src/cbmc/bmc_incremental.cpp b/src/cbmc/bmc_incremental.cpp
@@ -30,13 +30,14 @@ safety_checkert::resultt bmc_incrementalt::step(
   try
   {
     // We count only new assertions.
-    symex.total_vccs=0;
-    symex.remaining_vccs=0;
+    symex().total_vccs=0;
+    symex().remaining_vccs=0;
 
     // perform symbolic execution
     bool symex_done=
-      symex(
-        symex_state,goto_functions,
+      symex()(
+        symex_state,
+        goto_functions,
         goto_functions.function_map.at(goto_functions.entry_point()).body);
 
     // add a partial ordering, if required
@@ -59,7 +60,7 @@ safety_checkert::resultt bmc_incrementalt::step(
       return result;
 
     // any properties to check at all?
-    if(symex.remaining_vccs==0)
+    if(symex().remaining_vccs==0)
     {
       report_success();
       result=safety_checkert::SAFE;
@@ -121,16 +122,16 @@ safety_checkert::resultt bmc_incrementalt::run(
 
     // check unwinding assertions
     if(result==safety_checkert::UNKNOWN &&
-       symex.add_loop_check())
+       symex().add_loop_check())
     {
       resultt loop_check_result=
         stop_on_fail(goto_functions, prop_conv);
       bool earliest_loop_exit=
         options.get_bool_option("earliest-loop-exit");
       if(loop_check_result==SAFE)
-        symex.update_loop_info(earliest_loop_exit ? false : true);
+        symex().update_loop_info(earliest_loop_exit ? false : true);
       else if(loop_check_result==UNSAFE)
-        symex.update_loop_info(earliest_loop_exit ? true : false);
+        symex().update_loop_info(earliest_loop_exit ? true : false);
     }
   }
 
@@ -154,11 +155,11 @@ void bmc_incrementalt::setup_unwind()
   bmct::setup_unwind();
 
   if(options.get_option("unwind-min")!="")
-    symex.incr_min_unwind=options.get_unsigned_int_option("unwind-min");
+    symex().incr_min_unwind=options.get_unsigned_int_option("unwind-min");
   if(options.get_option("unwind-max")!="")
-    symex.incr_max_unwind=options.get_unsigned_int_option("unwind-max");
+    symex().incr_max_unwind=options.get_unsigned_int_option("unwind-max");
   else
-    symex.incr_max_unwind=std::numeric_limits<unsigned>::max();
+    symex().incr_max_unwind=std::numeric_limits<unsigned>::max();
 
   status() << "Using incremental mode" << eom;
   prop_conv.set_all_frozen();
diff --git a/src/cbmc/bmc_incremental.h b/src/cbmc/bmc_incremental.h
@@ -33,12 +33,13 @@ class bmc_incrementalt:public bmct
     bmct(
       _options,
       _symbol_table,
-      _message_handler,
       _prop_conv,
-      new symex_bmc_incrementalt(ns, new_symbol_table, equation)),
-    goto_functions(_goto_functions),
-    symex(dynamic_cast<symex_bmc_incrementalt &>(*symex_ptr))  
-  {}
+      _message_handler),
+    goto_functions(_goto_functions)
+  {
+    symex_ptr=new symex_bmc_incrementalt(ns, new_symbol_table, equation);
+    symex().constant_propagation=options.get_bool_option("propagation");
+  }
 
   virtual ~bmc_incrementalt() { }
 
@@ -61,7 +62,10 @@ class bmc_incrementalt:public bmct
   virtual void setup_unwind();
 
  private:
-  symex_bmc_incrementalt &symex;
+  symex_bmc_incrementalt &symex()
+  {
+    return dynamic_cast<symex_bmc_incrementalt &>(*symex_ptr);
+  }
 };
 
 #endif
diff --git a/src/cbmc/bmc_incremental_one_loop.cpp b/src/cbmc/bmc_incremental_one_loop.cpp
@@ -28,12 +28,12 @@ safety_checkert::resultt bmc_incremental_one_loopt::step(
   try
   {
     // We count only new assertions.
-    symex.total_vccs=0;
-    symex.remaining_vccs=0;
+    symex().total_vccs=0;
+    symex().remaining_vccs=0;
 
     // perform symbolic execution
     bool symex_done=
-      symex(
+      symex()(
         symex_state,goto_functions,
         goto_functions.function_map.at(goto_functions.entry_point()).body);
 
@@ -63,7 +63,7 @@ safety_checkert::resultt bmc_incremental_one_loopt::step(
     resultt result=safety_checkert::UNKNOWN;
 
     // any properties to check at all?
-    if(symex.remaining_vccs==0)
+    if(symex().remaining_vccs==0)
     {
       report_success();
       result=safety_checkert::SAFE;
@@ -144,12 +144,12 @@ void bmc_incremental_one_loopt::setup_unwind()
   bmct::setup_unwind();
 
   if(options.get_option("unwind-min")!="")
-    symex.incr_min_unwind=options.get_unsigned_int_option("unwind-min");
+    symex().incr_min_unwind=options.get_unsigned_int_option("unwind-min");
   if(options.get_option("unwind-max")!="")
-    symex.incr_max_unwind=options.get_unsigned_int_option("unwind-max");
-  symex.ignore_assertions=(symex.incr_min_unwind>=2) &&
+    symex().incr_max_unwind=options.get_unsigned_int_option("unwind-max");
+  symex().ignore_assertions=(symex().incr_min_unwind>=2) &&
     options.get_bool_option("ignore-assertions-before-unwind-min");
-  symex.incr_loop_id=options.get_option("incremental-check");
+  symex().incr_loop_id=options.get_option("incremental-check");
 
   status() << "Using incremental mode" << eom;
   prop_conv.set_all_frozen();
diff --git a/src/cbmc/bmc_incremental_one_loop.h b/src/cbmc/bmc_incremental_one_loop.h
@@ -34,13 +34,14 @@ class bmc_incremental_one_loopt:public bmct
     bmct(
       _options,
       _symbol_table,
-      _message_handler,
       _prop_conv,
-      new symex_bmc_incremental_one_loopt(
-        ns, new_symbol_table, equation, prop_conv)),
-    goto_functions(_goto_functions),
-    symex(dynamic_cast<symex_bmc_incremental_one_loopt &>(*symex_ptr))
-  {}
+      _message_handler),
+    goto_functions(_goto_functions)
+  {
+    symex_ptr=new symex_bmc_incremental_one_loopt(
+      ns, new_symbol_table, equation, prop_conv);
+    symex().constant_propagation=options.get_bool_option("propagation");
+  }
 
   virtual ~bmc_incremental_one_loopt() {}
 
@@ -63,7 +64,10 @@ class bmc_incremental_one_loopt:public bmct
   virtual void setup_unwind();
 
 private:
-  symex_bmc_incremental_one_loopt &symex;
+  symex_bmc_incremental_one_loopt &symex()
+  {
+    return dynamic_cast<symex_bmc_incremental_one_loopt &>(*symex_ptr);
+  }
 };
 
 #endif

Original file line number	Diff line number	Diff line change
`@@ -346,8 +346,8 @@ void bmct::slice()`
`346`	`346`	`}`
`347`	`347`	`}`
`348`	`348`	`}`
`349`		`- statistics() << "Generated " << symex.total_vccs`
`350`		`- << " VCC(s), " << symex.remaining_vccs`
	`349`	`+ statistics() << "Generated " << symex().total_vccs`
	`350`	`+ << " VCC(s), " << symex().remaining_vccs`
`351`	`351`	`<< " remaining after simplification" << eom;`
`352`	`352`	`}`
`353`	`353`
`@@ -510,12 +510,12 @@ safety_checkert::resultt bmct::initialize()`
`510`	`510`	`return ERROR;`
`511`	`511`	`}`
`512`	`512`
`513`		`- symex.set_message_handler(get_message_handler());`
`514`		`- symex.options=options;`
	`513`	`+ symex().set_message_handler(get_message_handler());`
	`514`	`+ symex().options=options;`
`515`	`515`
`516`	`516`	`status() << "Starting Bounded Model Checking" << eom;`
`517`	`517`
`518`		`- symex.last_source_location.make_nil();`
	`518`	`+ symex().last_source_location.make_nil();`
`519`	`519`
`520`	`520`	`// get unwinding info`
`521`	`521`	`setup_unwind();`
`@@ -540,7 +540,7 @@ safety_checkert::resultt bmct::step(const goto_functionst &goto_functions)`
`540`	`540`	`try`
`541`	`541`	`{`
`542`	`542`	`// perform symbolic execution`
`543`		`- symex(goto_functions);`
	`543`	`+ symex()(goto_functions);`
`544`	`544`
`545`	`545`	`// add a partial ordering, if required`
`546`	`546`	`if(equation.has_threads())`
`@@ -575,8 +575,8 @@ safety_checkert::resultt bmct::step(const goto_functionst &goto_functions)`
`575`	`575`	`slice();`
`576`	`576`
`577`	`577`	`{`
`578`		`- statistics() << "Generated " << symex.total_vccs`
`579`		`- << " VCC(s), " << symex.remaining_vccs`
	`578`	`+ statistics() << "Generated " << symex().total_vccs`
	`579`	`+ << " VCC(s), " << symex().remaining_vccs`
`580`	`580`	`<< " remaining after simplification" << eom;`
`581`	`581`	`}`
`582`	`582`
`@@ -604,7 +604,7 @@ safety_checkert::resultt bmct::step(const goto_functionst &goto_functions)`
`604`	`604`
`605`	`605`	`// any properties to check at all?`
`606`	`606`	`if(!options.get_bool_option("program-only") &&`
`607`		`- symex.remaining_vccs==0)`
	`607`	`+ symex().remaining_vccs==0)`
`608`	`608`	`{`
`609`	`609`	`report_success();`
`610`	`610`	`output_graphml(SAFE, goto_functions);`
`@@ -729,12 +729,12 @@ void bmct::setup_unwind()`
`729`	`729`	`long uw=unsafe_string2int(val.substr(val.rfind(":")+1));`
`730`	`730`
`731`	`731`	`if(thread_nr_set)`
`732`		`- symex.set_unwind_thread_loop_limit(thread_nr, id, uw);`
	`732`	`+ symex().set_unwind_thread_loop_limit(thread_nr, id, uw);`
`733`	`733`	`else`
`734`		`- symex.set_unwind_loop_limit(id, uw);`
	`734`	`+ symex().set_unwind_loop_limit(id, uw);`
`735`	`735`	`}`
`736`	`736`	`}`
`737`	`737`
`738`	`738`	`if(options.get_option("unwind")!="")`
`739`		`- symex.set_unwind_limit(options.get_unsigned_int_option("unwind"));`
	`739`	`+ symex().set_unwind_limit(options.get_unsigned_int_option("unwind"));`
`740`	`740`	`}`