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

Author: Daniel Kroening

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/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

regression/test.pl

@@ -184,7 +184,7 @@ ()
   my @list;
 
   opendir CWD, ".";
-  @list = grep { !/^\./ && -d "$_" && !/CVS/ && -s "$_/test.desc" } readdir CWD;
+  @list = grep { !/^\./ && -d "$_" && !/CVS/ } readdir CWD;
   closedir CWD;
 
   @list = sort @list;

src/goto-programs/cfg.h

@@ -31,6 +31,31 @@ struct cfg_base_nodet:public graph_nodet<empty_edget>, public T
   I PC;
 };
 
+/// A multi-procedural control flow graph (CFG) whose nodes store references to
+/// instructions in a GOTO program.
+///
+/// An instance of cfg_baset<T> is a directed graph whose nodes inherit from a
+/// user-provided type T and store a pointer to an instruction of some
+/// goto program in the field `PC`. The field `PC` of every node points to the
+/// original GOTO instruction that gave rise to the node, and the field
+/// cfg_baset::entry_map maps every GOTO instruction to some CFG node.
+///
+/// The CFG is constructed on the operator() from either one goto_programt or
+/// multiple goto_programt objects (stored in a goto_functionst).  The edges of
+/// the CFG are created on the method compute_edges(), and notably include:
+///
+/// - Edges from location A to B if both A and B belong to the same
+///   goto_programt and A can flow into B.
+/// - An edge from each FUNCTION_CALL instruction and the first instruction of
+///   the called function, when that function body is available and its body is
+///   non-empty.
+/// - For each FUNCTION_CALL instruction found, an edge between the exit point
+///   of the called function and the instruction immediately after the
+///   FUNCTION_CALL, when the function body is available and its body is
+///   non-empty.
+///
+///   Note that cfg_baset is the base class of many other subclasses and the
+///   specific edges constructed by operator() can be different in those.
 template<class T,
          typename P=const goto_programt,
          typename I=goto_programt::const_targett>

src/goto-programs/goto_program.cpp

@@ -33,9 +33,13 @@ std::ostream &goto_programt::output_instruction(
   return output_instruction(ns, identifier, out, *it);
 }
 
-/// Writes to out a two line string representation of the specific instruction.
-/// It is of the format: // {location} file {source file} line {line in source
-/// file} {representation of the instruction}
+/// Writes to \p out a two/three line string representation of a given
+/// \p instruction. The output is of the format:
+/// ```
+///   // {location} file {source file} line {line in source file}
+///   // Labels: {list-of-labels}
+///   {representation of the instruction}
+/// ```
 /// \param ns: the namespace to resolve the expressions in
 /// \param identifier: the identifier used to find a symbol to identify the
 ///   source language