Merge pull request #1612 from reuk/reuk/more-iterator-fixes

Iterator comparison and memory bug fixes

Author: tautschnig

.travis.yml

@@ -65,7 +65,9 @@ jobs:
       before_install:
         - mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
       # env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
-      env: COMPILER="ccache g++-5"
+      env:
+        - COMPILER="ccache g++-5"
+        - EXTRA_CXXFLAGS="-D_GLIBCXX_DEBUG"
 
     # OS X using g++
     - stage: Test different OS/CXX/Flags

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

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc --unwind 5
 ^EXIT=0$
@@ -7,3 +7,6 @@ main.c
 --
 ^warning: ignoring
 ^\[.*<builtin-library-
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details

regression/cbmc-cover/mcdc1/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -12,3 +12,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details

regression/cbmc-cover/mcdc10/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -10,3 +10,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details

regression/cbmc-cover/mcdc11/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -12,3 +12,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details

regression/cbmc-cover/mcdc12/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -15,3 +15,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details

regression/cbmc-cover/mcdc13/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -10,3 +10,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details

regression/cbmc-cover/mcdc14/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -8,3 +8,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details

regression/cbmc-cover/mcdc2/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -10,3 +10,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details

regression/cbmc-cover/mcdc3/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --cover mcdc
 ^EXIT=0$
@@ -9,3 +9,6 @@ main.c
 ^\*\* .* of .* covered \(100.0%\)$
 --
 ^warning: ignoring
+--
+Knownbug added because this test triggers an invariant in cover.cpp
+See #1622 for details