Merge master into test-gen-support

CODING_STANDARD.md

@@ -107,6 +107,9 @@ Here a few minimalistic coding rules for the CPROVER source tree.
   include in the source file. For example, given `foo.h` and `foo.cpp`, the
   line `#include "foo.h"` should precede all other include statements in
   `foo.cpp`.
+- Use the C++ versions of C headers (e.g. `cmath` instead of `math.h`).
+  Some of the C headers use macros instead of functions which can have
+  unexpected consequences.
 
 # Makefiles
 - Each source file should appear on a separate line

regression/ansi-c/Struct_Initialization1/main.c

@@ -1,13 +1,19 @@
 #define STATIC_ASSERT(condition) \
   int some_array##__LINE__[(condition) ? 1 : -1]
 
+struct A {
+  int x;
+  int y;
+};
+
 struct _classinfo {
   char a;
+  struct A s;
   int *interfaces[];
 };
 
-struct _classinfo nullclass1 = { 42, 0, 0 };
-struct _classinfo nullclass2 = { 42, { 0, 0 } };
+struct _classinfo nullclass1 = { 42, 1, 2, 3, 4 };
+struct _classinfo nullclass2 = { 42, { 1, 2 }, { 3, 4 } };
 
 STATIC_ASSERT(sizeof(nullclass1)==sizeof(struct _classinfo));
 STATIC_ASSERT(sizeof(nullclass2)==sizeof(struct _classinfo));

regression/ansi-c/Struct_Initialization1/test.desc

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

regression/ansi-c/Struct_Initialization2/main.c

@@ -0,0 +1,24 @@
+#define STATIC_ASSERT(condition) \
+  int some_array##__LINE__[(condition) ? 1 : -1]
+
+struct A {
+  int x;
+  int y;
+  int arr[];
+};
+
+struct _classinfo {
+  char a;
+  struct A s;
+  int *interfaces[];
+};
+
+struct _classinfo nullclass1 = { 42, 1, 2, 0, 3, 4 };
+struct _classinfo nullclass2 = { 42, { 1, 2, 0 }, { 3, 4 } };
+
+STATIC_ASSERT(sizeof(nullclass1)==sizeof(struct _classinfo));
+STATIC_ASSERT(sizeof(nullclass2)==sizeof(struct _classinfo));
+
+int main()
+{
+}

regression/ansi-c/Struct_Initialization2/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+
+^EXIT=(64|1)$
+^SIGNAL=0$
+^CONVERSION ERROR$
+--
+^warning: ignoring
+--
+variable-length arrays in the middle of a struct are not permitted

regression/ansi-c/gcc_attributes10/main.c

@@ -0,0 +1,19 @@
+#define STATIC_ASSERT(condition) \
+  int array##__LINE__[(condition) ? 1 : -1]
+
+#ifdef __GNUC__
+
+int  x   __attribute__ ((__vector_size__ (12), __may_alias__));
+int  x2   __attribute__ ((__may_alias__));
+int  x3   __attribute__ ((__may_alias__, __vector_size__ (12)));
+
+STATIC_ASSERT(sizeof(x)==12);
+STATIC_ASSERT(sizeof(x2)==sizeof(int));
+STATIC_ASSERT(sizeof(x3)==12);
+
+#endif
+
+int main(int argc, char* argv[])
+{
+  return 0;
+}

regression/ansi-c/gcc_attributes10/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/ansi-c/gcc_attributes5/test.desc

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

regression/ansi-c/sizeof4/main.c

@@ -0,0 +1,12 @@
+
+#define STATIC_ASSERT(condition) \
+  int some_array##__LINE__[(condition) ? 1 : -1];
+
+// The result of boolean operators is always an int
+STATIC_ASSERT(sizeof(1.0 && 1.0)==sizeof(int));
+STATIC_ASSERT(sizeof(1.0 || 1.0)==sizeof(int));
+STATIC_ASSERT(sizeof(!1.0)==sizeof(int));
+
+int main()
+{
+}

regression/ansi-c/sizeof4/test.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/cbmc/Float-Rounding3/main.c

@@ -0,0 +1,31 @@
+// This is C99, but currently only works with clang.
+// gcc and Visual Studio appear to hard-wire FLT_ROUNDS to 1.
+
+#ifdef __clang__
+
+#include <assert.h>
+#include <fenv.h>
+#include <float.h>
+
+int main()
+{
+  fesetround(FE_DOWNWARD);
+  assert(FLT_ROUNDS==3);
+
+  fesetround(FE_TONEAREST);
+  assert(FLT_ROUNDS==1);
+
+  fesetround(FE_TOWARDZERO);
+  assert(FLT_ROUNDS==0);
+
+  fesetround(FE_UPWARD);
+  assert(FLT_ROUNDS==2);
+}
+
+#else
+
+int main()
+{
+}
+
+#endif

regression/cbmc/Float-Rounding3/test.desc

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

regression/cbmc/dynamic_size1/main.c

@@ -0,0 +1,14 @@
+#include <stdlib.h>
+
+int main()
+{
+  unsigned x;
+
+  int *A=malloc(x*sizeof(int));
+
+  char *p=&A[1];
+
+  char c=*p;
+
+  return c;
+}

regression/cbmc/dynamic_size1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+^unknown or invalid type size:

regression/cbmc/enum6/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+
+int main(void)
+{
+  enum A { zero, one, two, three } a = two, b = one, c = three;
+
+  a <<= b;
+  assert(a==4);
+
+  c += b;
+  assert(c==4);
+
+  enum E { fortytwo=42 } e = fortytwo;
+  double res;
+  res = -42.0 + (double) e;
+  assert ((res >= -0.000005) && (res <= 0.000005));
+
+  return 0;
+}

regression/cbmc/enum6/test.desc

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

regression/cbmc/fgets1/main.c

@@ -0,0 +1,22 @@
+#include <stdio.h>
+#include <assert.h>
+
+int main()
+{
+  char buffer[3]={'a', 'b', '\0'};
+  FILE *f=fdopen(0, "r");
+  if(!f)
+    return 1;
+
+  char *p=fgets(buffer, 3, f);
+  if(p)
+  {
+    assert(buffer[1]==p[1]);
+    assert(buffer[2]=='\0');
+    assert(p[1]=='b'); // expected to fail
+  }
+
+  fclose(f);
+
+  return 0;
+}

regression/cbmc/fgets1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--bounds-check --pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[main.assertion.3\] assertion p\[1\]=='b': FAILURE
+\*\* 1 of \d+ failed \(2 iterations\)
+--
+^warning: ignoring

regression/cbmc/memory_allocation1/test.desc

@@ -5,7 +5,7 @@ main.c
 ^SIGNAL=0$
 \[main.pointer_dereference.2\] dereference failure: pointer invalid in \*p: SUCCESS
 \[main.assertion.1\] assertion \*p==42: SUCCESS
-\[main.pointer_dereference.14\] dereference failure: pointer invalid in p\[\(signed( long)? long int\)1\]: FAILURE
+\[main.pointer_dereference.14\] dereference failure: pointer invalid in p\[.*1\]: FAILURE
 \[main.assertion.2\] assertion \*\(p\+1\)==42: SUCCESS
 \*\* 12 of 26 failed \(2 iterations\)
 --

regression/cbmc/union9/main.c

@@ -0,0 +1,35 @@
+#include <stdlib.h>
+#include <stdint.h>
+
+typedef union {
+  struct {
+    uint8_t x;
+    uint8_t z;
+  } b;
+} union_t;
+
+typedef struct {
+    uint32_t magic;
+    union_t unions[];
+} flex;
+
+int flex_init(flex * flex, size_t num)
+{
+    if (num == 0 || num >= 200) {
+        return -1;
+    }
+    flex->unions[num - 1].b.z = 255;
+    return 0;
+}
+
+int main() {
+    uint8_t num = nondet_size();
+    flex * pool = (flex *) malloc(sizeof(flex) + num * sizeof(union_t));
+    int ret = flex_init(pool, num);
+    if (num > 0 && num < 200) {
+        __CPROVER_assert(ret == 0, "Accept inside range");
+    } else {
+        __CPROVER_assert(ret != 0, "Reject outside range");
+    }
+}
+

regression/cbmc/union9/test.desc

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

scripts/cpplint.py

@@ -6511,7 +6511,7 @@ def ProcessFile(filename, vlevel, extra_check_functions=[]):
   if Search(r'(\.l|\.y|\.inc|\.d|\.o|y\.tab\.cpp|\.tab\.h|\.yy\.cpp)$', filename):
     return
 
-  if Search(r'_builtin_headers_[a-z0-9_-]+\.h$', filename):
+  if Search(r'_builtin_headers(_[a-z0-9_-]+)?\.h$', filename):
     return
 
   if not ProcessConfigOverrides(filename):

scripts/doxy_merge_driver.sh

@@ -0,0 +1,13 @@
+#!/usr/bin/env sh
+
+# This script can be used in conjunction with git and the doc-reformatting
+# script (reformat_docs.py) to facilitate automatic rebases/merges spanning the
+# transition to Doxygen-style comments.
+# Usage information: https://svn.cprover.org/wiki/doku.php?id=doxygen
+
+script_dir="$(dirname "$0")"
+
+python "${script_dir}/reformat_docs.py" "$1" -i
+python "${script_dir}/reformat_docs.py" "$2" -i
+python "${script_dir}/reformat_docs.py" "$3" -i
+git merge-file "$1" "$2" "$3"

src/analyses/flow_insensitive_analysis.h

@@ -25,7 +25,8 @@ Author: Daniel Kroening, [email protected]
 class flow_insensitive_abstract_domain_baset
 {
 public:
-  flow_insensitive_abstract_domain_baset()
+  flow_insensitive_abstract_domain_baset():
+    changed(false)
   {
   }
 

src/ansi-c/ansi_c_convert_type.h

@@ -53,6 +53,7 @@ class ansi_c_convert_typet:public messaget
 
   explicit ansi_c_convert_typet(message_handlert &_message_handler):
     messaget(_message_handler)
+    // class members are initialized by calling read()
   {
   }
 

src/ansi-c/ansi_c_parser.h

@@ -29,7 +29,12 @@ class ansi_c_parsert:public parsert
   ansi_c_parse_treet parse_tree;
 
   ansi_c_parsert():
-    cpp98(false), cpp11(false),
+    tag_following(false),
+    asm_block_following(false),
+    parenthesis_counter(0),
+    mode(modet::NONE),
+    cpp98(false),
+    cpp11(false),
     for_has_scope(false)
   {
   }