Merge pull request #292 from peterschrammel/do-not-instrument-built-ins

Do not instrument built-ins

Author: Daniel Kroening

regression/cbmc-cover/built-ins1/main.c

@@ -0,0 +1,17 @@
+int main()
+{
+  char a[10];
+  __CPROVER_input("a[3]", a[3]);
+
+  int len = strlen(a);
+
+  if(len==3)
+  {
+    return 0;
+  }
+  else if(len==4)
+  {
+    return -1;
+  }
+  return 1;
+}

regression/cbmc-cover/built-ins1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--cover location --unwind 1
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 4 of 7 covered
+--
+^warning: ignoring
+^\[.*<builtin-library-

regression/cbmc-cover/built-ins2/main.c

@@ -0,0 +1,19 @@
+struct mystruct {
+  int x;
+  char y;
+};
+
+int main()
+{
+  struct mystruct s;
+  char c;
+  __CPROVER_input("c", c);
+
+  memset(&s,c,sizeof(struct mystruct));
+
+  if(s.y=='A')
+  {
+    return 0;
+  }
+  return 1;
+}

regression/cbmc-cover/built-ins2/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--cover location --unwind 10
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 4 of 4 covered
+--
+^warning: ignoring
+^\[.*<builtin-library-

regression/cbmc-cover/built-ins3/main.c

@@ -0,0 +1,14 @@
+#include <stdio.h>
+
+int main()
+{
+  const char *s="test";
+  int ret=puts(s); //return value is nondet (internal to built-in, thus non-controllable)
+
+  if(ret<0)
+  {
+    return 1;
+  }
+
+  return 0;
+}

regression/cbmc-cover/built-ins3/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--cover location --unwind 10
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 4 of 4 covered
+--
+^warning: ignoring
+^\[.*<builtin-library-

regression/cbmc-cover/built-ins4/main.c

@@ -0,0 +1,17 @@
+int main()
+{
+  char a[10];
+  __CPROVER_input("a[3]", a[3]);
+
+  int len = strlen(a);
+
+  if(len==3)
+  {
+    return 0;
+  }
+  else if(len==4)
+  {
+    return -1;
+  }
+  return 1;
+}

regression/cbmc-cover/built-ins4/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--cover branch --unwind 5
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 5 of 5 covered
+--
+^warning: ignoring
+^\[.*<builtin-library-

regression/cbmc-cover/built-ins5/main.c

@@ -0,0 +1,17 @@
+int main()
+{
+  char a[10];
+  __CPROVER_input("a[3]", a[3]);
+
+  int len = strlen(a);
+
+  if(len==3)
+  {
+    return 0;
+  }
+  else if(len==4)
+  {
+    return -1;
+  }
+  return 1;
+}

regression/cbmc-cover/built-ins5/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--cover condition --unwind 5
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 4 of 4 covered
+--
+^warning: ignoring
+^\[.*<builtin-library-

regression/cbmc-cover/built-ins6/main.c

@@ -0,0 +1,17 @@
+int main()
+{
+  char a[10];
+  __CPROVER_input("a[3]", a[3]);
+
+  int len = strlen(a);
+
+  if(len==3)
+  {
+    return 0;
+  }
+  else if(len==4)
+  {
+    return -1;
+  }
+  return 1;
+}

regression/cbmc-cover/built-ins6/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--cover decision --unwind 5
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 4 of 4 covered
+--
+^warning: ignoring
+^\[.*<builtin-library-

regression/cbmc-cover/built-ins7/main.c

@@ -0,0 +1,17 @@
+int main()
+{
+  char a[10];
+  __CPROVER_input("a[3]", a[3]);
+
+  int len = strlen(a);
+
+  if(len==3)
+  {
+    return 0;
+  }
+  else if(len==4)
+  {
+    return -1;
+  }
+  return 1;
+}

regression/cbmc-cover/built-ins7/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--cover mcdc --unwind 5
+^EXIT=0$
+^SIGNAL=0$
+^\*\* 4 of 4 covered
+--
+^warning: ignoring
+^\[.*<builtin-library-

src/goto-instrument/cover.cpp

@@ -685,6 +685,7 @@ Function: eval_expr
           the atomic expr values
 
 \*******************************************************************/
+
 bool eval_expr(
   const std::map<exprt, signed> &atomic_exprs,
   const exprt &src)
@@ -1142,7 +1143,7 @@ void instrument_cover_goals(
             basic_blocks.source_location_map[block_nr];
 
           if(!source_location.get_file().empty() &&
-             source_location.get_file()[0]!='<')
+             !source_location.is_built_in())
           {
             std::string comment="block "+b;
             goto_program.insert_before_swap(i_it);
@@ -1180,7 +1181,8 @@ void instrument_cover_goals(
         t->source_location.set_property_class(property_class);
       }
 
-      if(i_it->is_goto() && !i_it->guard.is_true())
+      if(i_it->is_goto() && !i_it->guard.is_true() &&
+         !i_it->source_location.is_built_in())
       {
         std::string b=std::to_string(basic_blocks[i_it]);
         std::string true_comment=
@@ -1215,6 +1217,7 @@ void instrument_cover_goals(
         i_it->make_skip();
 
       // Conditions are all atomic predicates in the programs.
+      if(!i_it->source_location.is_built_in())
       {
         const std::set<exprt> conditions=collect_conditions(i_it);
 
@@ -1251,6 +1254,7 @@ void instrument_cover_goals(
         i_it->make_skip();
 
       // Decisions are maximal Boolean combinations of conditions.
+      if(!i_it->source_location.is_built_in())
       {
         const std::set<exprt> decisions=collect_decisions(i_it);
 
@@ -1291,6 +1295,7 @@ void instrument_cover_goals(
       // 3. Each condition in a decision takes every possible outcome
       // 4. Each condition in a decision is shown to independently
       //    affect the outcome of the decision.
+      if(!i_it->source_location.is_built_in())
       {
         const std::set<exprt> conditions=collect_conditions(i_it);
         const std::set<exprt> decisions=collect_decisions(i_it);
@@ -1393,7 +1398,8 @@ void instrument_cover_goals(
   Forall_goto_functions(f_it, goto_functions)
   {
     if(f_it->first==goto_functions.entry_point() ||
-       f_it->first=="__CPROVER_initialize")
+       f_it->first=="__CPROVER_initialize" ||
+       f_it->second.is_hidden())
       continue;
 
     instrument_cover_goals(symbol_table, f_it->second.body, criterion);