Merge branch 'master' of https://www.github.com/diffblue/cbmc

Author: Daniel Kroening

src/goto-cc/compile.cpp

@@ -25,7 +25,6 @@ Date: June 2006
 
 #include <ansi-c/ansi_c_language.h>
 
-#include <linking/linking_class.h>
 #include <linking/entry_point.h>
 
 #include <goto-programs/goto_convert.h>

src/goto-instrument/full_slicer.cpp

@@ -473,6 +473,27 @@ void full_slicer(
 
 /*******************************************************************\
 
+Function: property_slicer
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void property_slicer(
+  goto_functionst &goto_functions,
+  const namespacet &ns,
+  const std::list<std::string> &properties)
+{
+  properties_criteriont p(properties);
+  full_slicert()(goto_functions, ns, p);
+}
+
+/*******************************************************************\
+
 Function: slicing_criteriont::~slicing_criteriont
 
   Inputs:

src/goto-instrument/full_slicer.h

@@ -15,6 +15,11 @@ void full_slicer(
   goto_functionst &goto_functions,
   const namespacet &ns);
 
+void property_slicer(
+  goto_functionst &goto_functions,
+  const namespacet &ns,
+  const std::list<std::string> &properties);
+
 class slicing_criteriont
 {
 public:

src/goto-instrument/full_slicer_class.h

@@ -118,4 +118,35 @@ class assert_criteriont:public slicing_criteriont
   }
 };
 
+class properties_criteriont:public slicing_criteriont
+{
+public:
+  explicit properties_criteriont(
+    const std::list<std::string> &properties):
+    property_ids(properties)
+  {
+  }
+
+  virtual bool operator()(goto_programt::const_targett target)
+  {
+    if(!target->is_assert())
+      return false;
+
+    const std::string &p_id=
+      id2string(target->source_location.get_property_id());
+
+    for(std::list<std::string>::const_iterator
+        it=property_ids.begin();
+        it!=property_ids.end();
+        ++it)
+      if(p_id==*it)
+        return true;
+
+    return false;
+  }
+
+protected:
+  const std::list<std::string> &property_ids;
+};
+
 #endif

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1224,6 +1224,9 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   // add loop ids
   goto_functions.compute_loop_numbers();
 
+  // label the assertions
+  label_properties(goto_functions);
+
   // nondet volatile?
   if(cmdline.isset("nondet-volatile"))
   {
@@ -1246,7 +1249,10 @@ void goto_instrument_parse_optionst::instrument_goto_program()
       symbol_table, goto_functions, cmdline.isset("pointer-check"));
 
     status() << "Performing a full slice" << eom;
-    full_slicer(goto_functions, ns);
+    if(cmdline.isset("property"))
+      property_slicer(goto_functions, ns, cmdline.get_values("property"));
+    else
+      full_slicer(goto_functions, ns);
   }
 
   // label the assertions
@@ -1347,6 +1353,7 @@ void goto_instrument_parse_optionst::help()
     "Slicing:\n"
     " --reachability-slice         slice away instructions that can't reach assertions\n"
     " --full-slice                 slice away instructions that don't affect assertions\n"
+    " --property id                slice with respect to specific property only\n"
     "\n"
     "Further transformations:\n"
     " --constant-propagator        propagate constants and simplify expressions\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -49,7 +49,7 @@ Author: Daniel Kroening, [email protected]
   "(show-uninitialized)(show-locations)" \
   "(full-slice)(reachability-slice)" \
   "(inline)" \
-  "(show-claims)(show-properties)" \
+  "(show-claims)(show-properties)(property):" \
   "(show-symbol-table)(show-points-to)(show-rw-set)" \
   "(cav11)" \
   "(show-natural-loops)(accelerate)(havoc-loops)" \

src/linking/linking.cpp

@@ -64,6 +64,34 @@ std::string linkingt::type_to_string(
 
 /*******************************************************************\
 
+Function: follow_tags_symbols
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static const typet &follow_tags_symbols(
+  const namespacet &ns,
+  const typet &type)
+{
+  if(type.id()==ID_symbol)
+    return ns.follow(type);
+  else if(type.id()==ID_c_enum_tag)
+    return ns.follow_tag(to_c_enum_tag_type(type));
+  else if(type.id()==ID_struct_tag)
+    return ns.follow_tag(to_struct_tag_type(type));
+  else if(type.id()==ID_union_tag)
+    return ns.follow_tag(to_union_tag_type(type));
+  else
+    return type;
+}
+
+/*******************************************************************\
+
 Function: linkingt::type_to_string_verbose
 
   Inputs:
@@ -79,7 +107,7 @@ std::string linkingt::type_to_string_verbose(
   const symbolt &symbol,
   const typet &type) const
 { 
-  const typet &followed=ns.follow(type);
+  const typet &followed=follow_tags_symbols(ns, type);
 
   if(followed.id()==ID_struct || followed.id()==ID_union)
   {
@@ -149,13 +177,13 @@ void linkingt::detailed_conflict_report_rec(
 {
   #ifdef DEBUG
   str << "<BEGIN DEPTH " << depth << ">";
-  debug();
+  debug_msg();
   #endif
 
   std::string msg;
 
-  const typet &t1=ns.follow(type1);
-  const typet &t2=ns.follow(type2);
+  const typet &t1=follow_tags_symbols(ns, type1);
+  const typet &t2=follow_tags_symbols(ns, type2);
 
   if(t1.id()!=t2.id())
     msg="type classes differ";
@@ -231,6 +259,49 @@ void linkingt::detailed_conflict_report_rec(
         }
       }
   }
+  else if(t1.id()==ID_c_enum)
+  {
+    const c_enum_typet::memberst &members1=
+      to_c_enum_type(t1).members();
+
+    const c_enum_typet::memberst &members2=
+      to_c_enum_type(t2).members();
+
+    if(t1.subtype()!=t2.subtype())
+    {
+      msg="enum value types are different (";
+      msg+=type_to_string(ns, old_symbol.name, t1.subtype())+'/';
+      msg+=type_to_string(ns, new_symbol.name, t2.subtype())+')';
+    }
+    else if(members1.size()!=members2.size())
+    {
+      msg="number of enum members is different (";
+      msg+=i2string(members1.size())+'/';
+      msg+=i2string(members2.size())+')';
+    }
+    else
+      for(std::size_t i=0; i<members1.size(); ++i)
+      {
+        if(members1[i].get_base_name()!=members2[i].get_base_name())
+        {
+          msg="names of member "+i2string(i)+" differ (";
+          msg+=id2string(members1[i].get_base_name())+'/';
+          msg+=id2string(members2[i].get_base_name())+')';
+          break;
+        }
+        else if(members1[i].get_value()!=members2[i].get_value())
+        {
+          msg="values of member "+i2string(i)+" differ (";
+          msg+=id2string(members1[i].get_value())+'/';
+          msg+=id2string(members2[i].get_value())+')';
+          break;
+        }
+      }
+
+    msg+="\nenum declarations at\n";
+    msg+=t1.source_location().as_string()+" and\n";
+    msg+=t1.source_location().as_string();
+  }
   else if(t1.id()==ID_code)
   {
     const code_typet::parameterst &parameters1=
@@ -309,7 +380,7 @@ void linkingt::detailed_conflict_report_rec(
 
   #ifdef DEBUG
   str << "<END DEPTH " << depth << ">";
-  debug();
+  debug_msg();
   #endif
 }
 
@@ -527,8 +598,8 @@ void linkingt::duplicate_code_symbol(
 
       while(!conflicts.empty())
       {
-        const typet &t1=ns.follow(conflicts.front().first);
-        const typet &t2=ns.follow(conflicts.front().second);
+        const typet &t1=follow_tags_symbols(ns, conflicts.front().first);
+        const typet &t2=follow_tags_symbols(ns, conflicts.front().second);
 
         // void vs. non-void return type may be acceptable if the
         // return value is never used
@@ -555,7 +626,8 @@ void linkingt::duplicate_code_symbol(
                 old_symbol.value.is_nil()!=new_symbol.value.is_nil())
         {
           if(warn_msg.empty())
-            warn_msg="different pointer types in function";
+            warn_msg="pointer parameter types differ between "
+                     "declaration and definition";
           replace=new_symbol.value.is_not_nil();
         }
         // transparent union with (or entirely without) implementation is
@@ -736,10 +808,12 @@ void linkingt::duplicate_object_symbol(
     }
     else
     {
-      // provide additional diagnostic output for struct/union/array
+      // provide additional diagnostic output for
+      // struct/union/array/enum
       if(old_type.id()==ID_struct ||
          old_type.id()==ID_union ||
-         old_type.id()==ID_array)
+         old_type.id()==ID_array ||
+         old_type.id()==ID_c_enum)
         detailed_conflict_report(
           old_symbol,
           new_symbol,
@@ -1040,8 +1114,8 @@ void linkingt::do_type_dependencies(id_sett &needs_to_be_renamed)
       {
         queue.push(*d_it);
         #ifdef DEBUG
-        str << "LINKING: needs to be renamed (dependency): " << s_it->first;
-        debug();
+        str << "LINKING: needs to be renamed (dependency): " << *d_it;
+        debug_msg();
         #endif
       }
   }
@@ -1061,20 +1135,28 @@ Function: linkingt::rename_symbols
 
 void linkingt::rename_symbols(const id_sett &needs_to_be_renamed)
 {
+  namespacet src_ns(src_symbol_table);
+
   for(id_sett::const_iterator
       it=needs_to_be_renamed.begin();
       it!=needs_to_be_renamed.end();
       it++)
   {
     symbolt &new_symbol=src_symbol_table.symbols[*it];
 
-    irep_idt new_identifier=rename(*it);
+    irep_idt new_identifier;
+
+    if(new_symbol.is_type)
+      new_identifier=type_to_name(src_ns, *it, new_symbol.type);
+    else
+      new_identifier=rename(*it);
+
     new_symbol.name=new_identifier;
 
     #ifdef DEBUG
     str << "LINKING: renaming " << *it << " to "
         << new_identifier;
-    debug();
+    debug_msg();
     #endif
 
     if(new_symbol.is_type)
@@ -1182,7 +1264,7 @@ void linkingt::typecheck()
       needs_to_be_renamed.insert(s_it->first);
       #ifdef DEBUG
       str << "LINKING: needs to be renamed: " << s_it->first;
-      debug();
+      debug_msg();
       #endif
     }
   }

src/util/merge_irep.cpp

@@ -200,6 +200,17 @@ const irept& merge_irept::merged(const irept &irep)
     dest_named_sub[it->first]=merged(it->second); // recursive call
     #endif
 
+  const irept::named_subt &src_comments=irep.get_comments();
+  irept::named_subt &dest_comments=new_irep.get_comments();
+
+  forall_named_irep(it, src_comments)
+    #ifdef SUB_IS_LIST
+    dest_comments.push_back(
+      std::make_pair(it->first, merged(it->second))); // recursive call
+    #else
+    dest_comments[it->first]=merged(it->second); // recursive call
+    #endif
+
   return *irep_store.insert(new_irep).first;
 }
 

src/util/message_stream.h

@@ -86,6 +86,13 @@ class message_streamt:public message_clientt
     sequence_number++;
   }
 
+  void debug_msg()
+  {
+    send_msg(9, str.str());
+    clear_err();
+    sequence_number++;
+  }
+
   std::ostringstream str;
 
   bool get_error_found() const