Merge pull request #660 from peterschrammel/pull-from-master

Update test-gen-support from master

Author: forejtv

.gitignore

@@ -1,5 +1,16 @@
 # Local files generated by IDEs
+.vs/*
 .vscode/*
+~AutoRecover.*
+*.sln
+*.vcxproj*
+scripts/__pycache__/*
+src/goto-analyzer/taint_driver_scripts/.idea/*
+/*.config
+/*.creator
+/*.creator.user
+/*.files
+/*.includes
 
 # compilation files
 *.lo

COMPILING

@@ -10,10 +10,10 @@ environments:
 
 - Solaris 11
 
-- FreeBSD 10 or 11
+- FreeBSD 11
 
 - Cygwin
-  (We recommend the i686-pc-mingw32-g++ cross compiler, version 4.7 or above.)
+  (We recommend the i686-pc-mingw32-g++ cross compiler, version 5.4 or above.)
 
 - Microsoft's Visual Studio version 12 (2013), version 14 (2015),
   or version 15 (older versions won't work)
@@ -29,16 +29,16 @@ COMPILATION ON LINUX
 We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
 
 0) You need a C/C++ compiler, Flex and Bison, and GNU make.
-   The GNU Make needs to be version 3.81 or higher. On Debian-like
-   distributions, do
+   The GNU Make needs to be version 3.81 or higher.
+   On Debian-like distributions, do
 
-   apt-get install g++ gcc flex bison make git libz-dev libwww-perl patch libzip-dev
+   apt-get install g++-6 gcc flex bison make git libwww-perl patch
 
    On Red Hat/Fedora or derivates, do
 
    yum install gcc gcc-c++ flex bison perl-libwww-perl patch
 
-   Note that you need g++ version 4.9 or newer.
+   Note that you need g++ version 5.2 or newer.
 
 1) As a user, get the CBMC source via
 
@@ -57,7 +57,7 @@ COMPILATION ON SOLARIS 11
 1) As root, get the necessary development tools:
 
    pkg install system/header developer/lexer/flex developer/parser/bison developer/versioning/git
-   pkg install --accept developer/gcc-49
+   pkg install --accept developer/gcc-5
 
 2) As a user, get the CBMC source via
 
@@ -83,8 +83,8 @@ COMPILATION ON SOLARIS 11
    It will mis-optimize MiniSat2.
 
 
-COMPILATION ON FREEBSD 10/11
-----------------------------
+COMPILATION ON FREEBSD 11
+-------------------------
 
 1) As root, get the necessary tools:
 

regression/cbmc-java/VarLengthArrayTrace1/test.desc

@@ -3,7 +3,7 @@ VarLengthArrayTrace1.class
 --trace
 ^EXIT=10$
 ^SIGNAL=0$
-dynamic_3_array\[1l\]=10
+dynamic_3_array\[1.*\]=10
 --
 ^warning: ignoring
 assignment removed

regression/cbmc-java/classtest1/classtest1.class

@@ -0,0 +1,11 @@
+public class classtest1
+{
+  static void main(String[] args)
+  {
+    g(classtest1.class);
+  }
+  static void g(Object c)
+  {
+    assert true;
+  }
+}

regression/cbmc-java/classtest1/classtest1.java

@@ -0,0 +1,8 @@
+CORE
+classtest1.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/classtest1/test.desc

@@ -5,8 +5,8 @@ main.c
 ^SIGNAL=0$
 pointer outside dynamic object bounds in \*p: FAILURE
 pointer outside dynamic object bounds in \*p: FAILURE
-pointer outside dynamic object bounds in p2\[\(signed long int\)1\]: FAILURE
-pointer outside dynamic object bounds in p2\[\(signed long int\)0\]: FAILURE
+pointer outside dynamic object bounds in p2\[.*1\]: FAILURE
+pointer outside dynamic object bounds in p2\[.*0\]: FAILURE
 \*\* 4 of 36 failed \(3 iterations\)
 --
 ^warning: ignoring

regression/cbmc/Malloc23/test.desc

@@ -6,7 +6,7 @@ int main(int argc, char** argv) {
   if(argc != 2)
     return 0;
 
-  unsigned long x[argc];
+  unsigned long long x[argc];
   x[0]=0x0102030405060708;
   x[1]=0x1112131415161718;
 

regression/cbmc/byte_update2/main.c

@@ -13,7 +13,7 @@ int main(int argc, char** argv) {
   x[3]=0x0708;
   x[4]=0x090a;
 
-  unsigned long* alias=(unsigned long*)(((char*)x)+0);
+  unsigned long long* alias=(unsigned long long*)(((char*)x)+0);
   *alias=0xf1f2f3f4f5f6f7f8;
 
   unsigned char* alias2=(unsigned char*)x;

regression/cbmc/byte_update3/main.c

@@ -18,7 +18,7 @@ int main(int argc, char** argv) {
   x[8]=0x09;
   x[9]=0x0a;
 
-  unsigned long* alias=(unsigned long*)(((char*)x)+1);
+  unsigned long long* alias=(unsigned long long*)(((char*)x)+1);
   *alias=0xf1f2f3f4f5f6f7f8;
 
   unsigned char* alias2=(unsigned char*)x;

regression/cbmc/byte_update4/main.c

@@ -13,7 +13,7 @@ int main(int argc, char** argv) {
   x[3]=0x0708;
   x[4]=0x090a;
 
-  unsigned long* alias=(unsigned long*)(((char*)x)+1);
+  unsigned long long* alias=(unsigned long long*)(((char*)x)+1);
   *alias=0xf1f2f3f4f5f6f7f8;
 
   unsigned char* alias2=(unsigned char*)x;

regression/cbmc/byte_update5/main.c

@@ -6,7 +6,7 @@ int main(int argc, char** argv) {
   if(argc != 2)
     return 0;
 
-  unsigned long x[argc];
+  unsigned long long x[argc];
   x[0]=0x0102030405060708;
   x[1]=0x1112131415161718;
 

regression/cbmc/byte_update6/main.c

@@ -6,7 +6,7 @@ int main(int argc, char** argv) {
   if(argc != 2)
     return 0;
 
-  unsigned long x[argc];
+  unsigned long long x[argc];
   x[0]=0x0102030405060708;
   x[1]=0x1112131415161718;
 

regression/cbmc/byte_update7/main.c

@@ -0,0 +1,18 @@
+
+int x;
+
+void g()
+{
+  x = 1;
+}
+
+void f()
+{
+  g();
+}
+
+int main()
+{
+  f();
+}
+

regression/goto-instrument/inline_13/main.c

@@ -0,0 +1,8 @@
+CORE
+main.c
+--function-inline main --log -
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument/inline_13/test.desc

@@ -0,0 +1,23 @@
+
+int x;
+
+void h()
+{
+  x = 1;
+}
+
+void g()
+{
+  h();
+}
+
+void f()
+{
+  g();
+}
+
+int main()
+{
+  f();
+}
+

regression/goto-instrument/inline_14/main.c

@@ -0,0 +1,8 @@
+CORE
+main.c
+--function-inline main --log - --no-caching
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument/inline_14/test.desc

@@ -0,0 +1,23 @@
+
+int x;
+
+void h()
+{
+  x = 1;
+}
+
+void g()
+{
+  h();
+}
+
+void f()
+{
+  g();
+}
+
+int main()
+{
+  f();
+}
+

regression/goto-instrument/inline_15/main.c

@@ -0,0 +1,8 @@
+CORE
+main.c
+--function-inline main --log - --no-caching --verbosity 9
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument/inline_15/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --full-slice
 ^EXIT=0$

regression/goto-instrument/slice02/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --full-slice
 ^EXIT=10$

regression/goto-instrument/slice14/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --full-slice --unwind 2
 ^EXIT=0$

regression/goto-instrument/slice16/test.desc

@@ -11,20 +11,19 @@
 added_lines = set()
 repository_root = sys.argv[2]
 
-with open(sys.argv[1], "r") as f:
-  diff = unidiff.PatchSet(f)
-  for diff_file in diff:
-    filename = diff_file.target_file
-    # Skip files deleted in the tip (b side of the diff):
-    if filename == "/dev/null":
-      continue
-    assert filename.startswith("b/")
-    filename = os.path.join(repository_root, filename[2:])
-    added_lines.add((filename, 0))
-    for diff_hunk in diff_file:
-      for diff_line in diff_hunk:
-        if diff_line.line_type == "+":
-          added_lines.add((filename, diff_line.target_line_no))
+diff = unidiff.PatchSet.from_filename(sys.argv[1])
+for diff_file in diff:
+  filename = diff_file.target_file
+  # Skip files deleted in the tip (b side of the diff):
+  if filename == "/dev/null":
+    continue
+  assert filename.startswith("b/")
+  filename = os.path.join(repository_root, filename[2:])
+  added_lines.add((filename, 0))
+  for diff_hunk in diff_file:
+    for diff_line in diff_hunk:
+      if diff_line.line_type == "+":
+        added_lines.add((filename, diff_line.target_line_no))
 
 for l in sys.stdin:
   bits = l.split(":")

scripts/filter_lint_by_diff.py

@@ -94,6 +94,9 @@ void dep_graph_domaint::control_dependencies(
      from->is_assume())
     control_deps.insert(from);
 
+  const irep_idt id=goto_programt::get_function_id(from);
+  const cfg_post_dominatorst &pd=dep_graph.cfg_post_dominators().at(id);
+
   // check all candidates for M
   for(depst::iterator
       it=control_deps.begin();
@@ -111,15 +114,17 @@ void dep_graph_domaint::control_dependencies(
     // we could hard-code assume and goto handling here to improve
     // performance
     cfg_post_dominatorst::cfgt::entry_mapt::const_iterator e=
-      dep_graph.cfg_post_dominators().cfg.entry_map.find(*it);
-    assert(e!=dep_graph.cfg_post_dominators().cfg.entry_map.end());
+      pd.cfg.entry_map.find(*it);
+
+    assert(e!=pd.cfg.entry_map.end());
+
     const cfg_post_dominatorst::cfgt::nodet &m=
-      dep_graph.cfg_post_dominators().cfg[e->second];
+      pd.cfg[e->second];
 
     for(const auto &edge : m.out)
     {
       const cfg_post_dominatorst::cfgt::nodet &m_s=
-        dep_graph.cfg_post_dominators().cfg[edge.first];
+        pd.cfg[edge.first];
 
       if(m_s.dominators.find(to)!=m_s.dominators.end())
         post_dom_one=true;
@@ -252,30 +257,39 @@ void dep_graph_domaint::transform(
   const namespacet &ns)
 {
   dependence_grapht *dep_graph=dynamic_cast<dependence_grapht*>(&ai);
-  assert(dep_graph!=0);
+  assert(dep_graph!=nullptr);
 
   // propagate control dependencies across function calls
   if(from->is_function_call())
   {
     goto_programt::const_targett next=from;
     ++next;
 
-    dep_graph_domaint *s=
-      dynamic_cast<dep_graph_domaint*>(&(dep_graph->get_state(next)));
-    assert(s!=0);
-
-    depst::iterator it=s->control_deps.begin();
-    for(const auto &c_dep : control_deps)
+    if(next==to)
     {
-      while(it!=s->control_deps.end() && *it<c_dep)
-        ++it;
-      if(it==s->control_deps.end() || c_dep<*it)
-        s->control_deps.insert(it, c_dep);
-      else if(it!=s->control_deps.end())
-        ++it;
+      control_dependencies(from, to, *dep_graph);
+    }
+    else
+    {
+      // edge to function entry point
+
+      dep_graph_domaint *s=
+        dynamic_cast<dep_graph_domaint*>(&(dep_graph->get_state(next)));
+      assert(s!=nullptr);
+
+      depst::iterator it=s->control_deps.begin();
+      for(const auto &c_dep : control_deps)
+      {
+        while(it!=s->control_deps.end() && *it<c_dep)
+          ++it;
+        if(it==s->control_deps.end() || c_dep<*it)
+          s->control_deps.insert(it, c_dep);
+        else if(it!=s->control_deps.end())
+          ++it;
+      }
+
+      control_deps.clear();
     }
-
-    control_dependencies(from, next, *dep_graph);
   }
   else
     control_dependencies(from, to, *dep_graph);