Fixed type mismatch in generated CEGIS danger_execute calls.

Author: pkesseli

src/ansi-c/library/cegis.c

@@ -1,6 +1,4 @@
-#ifndef __CPROVER_CEGIS_H_
-#define __CPROVER_CEGIS_H_
-#endif
+/* FUNCTION: __CPROVER_danger_execute */
 
 #ifndef __CPROVER_cegis_number_of_vars
 #define __CPROVER_cegis_number_of_vars 2
@@ -15,8 +13,6 @@
 #define __CPROVER_cegis_max_solution_size 1
 #endif
 
-/* FUNCTION: __CPROVER_danger_execute */
-
 const void *__CPROVER_cegis_OPS[__CPROVER_cegis_number_of_ops];
 void *__CPROVER_cegis_RESULT_OPS[__CPROVER_cegis_max_solution_size];
 

src/cegis/danger/symex/learn/danger_learn_config.cpp

@@ -16,8 +16,6 @@
 #include <cegis/danger/symex/learn/solution_factory.h>
 #include <cegis/danger/symex/learn/danger_learn_config.h>
 
-#include <util/ui_message.h> // XXX: Debug
-
 danger_learn_configt::danger_learn_configt(const danger_programt &program) :
     original_program(program), num_consts(0u)
 {
@@ -34,8 +32,7 @@ void danger_learn_configt::process(const counterexamplest &ces,
   var_ids.clear();
   num_consts=get_invariant_variable_ids(program.st, var_ids);
   const size_t num_vars=var_ids.size();
-  //null_message_handlert msg;
-  ui_message_handlert msg(ui_message_handlert::PLAIN, ""); // XXX: Debug
+  null_message_handlert msg;
   const std::string name(DANGER_EXECUTE);
   symbol_tablet &st=program.st;
   goto_functionst &gf=program.gf;

src/cegis/instrument/cegis_library.cpp

@@ -61,21 +61,6 @@ void add_execute_placeholder(symbol_tablet &symbol_table,
   symbol_table.add(symbol);
 }
 
-void set_loop_id(goto_functionst &gf, const std::string &func_name)
-{
-  goto_functionst::function_mapt &fm=gf.function_map;
-  goto_functionst::function_mapt::iterator execute=fm.find(func_name);
-  assert(fm.end() != execute);
-  goto_programt &body=execute->second.body;
-  goto_programt::instructionst &instrs=body.instructions;
-  unsigned loop_number=0;
-  for (goto_programt::targett it=instrs.begin(); it != instrs.end(); ++it)
-  {
-    goto_programt::instructiont &instr=*it;
-    if (instr.is_backwards_goto()) instr.loop_number=loop_number++;
-  }
-}
-
 goto_programt::targett init_array(const symbol_tablet &st, goto_programt &body,
     const char * const name, goto_programt::targett pos)
 {
@@ -120,22 +105,10 @@ void add_cegis_library(symbol_tablet &st, goto_functionst &gf,
       get_cegis_library_text(num_vars, num_consts, max_solution_size,
           func_name));
 
-  //if(cmdline.isset("gcc"))
-  /*{
-    // There are gcc versions that target Windows (MinGW for example),
-    // and we support that.
-    config.ansi_c.preprocessor=configt::ansi_ct::preprocessort::PP_GCC;
-    config.ansi_c.mode=configt::ansi_ct::flavourt::MODE_GCC_C;
-
-    // enable Cygwin
-    #ifdef _WIN32
-    config.ansi_c.defines.push_back("__CYGWIN__");
-    #endif
-  }*/
-
   add_library(library_src, st, msg);
   goto_convert(func_name, st, gf, msg);
-  set_loop_id(gf, func_name);
+  gf.compute_loop_numbers();
+  gf.update();
   set_init_values(st, gf);
 }
 

src/cegis/invariant/symex/learn/add_invariant_programs_to_learn.cpp

@@ -42,7 +42,8 @@ void execute_inv_prog(const symbol_tablet &st, goto_functionst &gf,
   const constant_exprt index(from_integer(0u, size_type));
   const index_exprt first_elem(prog_symbol, index);
   call.arguments().push_back(address_of_exprt(first_elem));
-  const constant_exprt size(from_integer(max_solution_size, size_type));
+  const typet size_arg_type(unsigned_char_type());
+  const constant_exprt size(from_integer(max_solution_size, size_arg_type));
   call.arguments().push_back(size);
   execution->code=call;
 }