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

Author: Daniel Kroening

regression/goto-analyzer/approx-array-variable-const-fp/test.desc

@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --verbosity 10 --pointer-check
 ^Removing function pointers and virtual functions$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f2 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f3 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f4 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f2 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f3 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f4 THEN GOTO [0-9]$
 ^SIGNAL=0$
 --
-^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f1 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f5 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f6 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f7 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f8 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f9 THEN GOTO [0-9]$
 ^warning: ignoring

regression/goto-analyzer/no-match-dereference-const-pointer-const-array-literal-pointer-const-fp/test.desc

@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --verbosity 10 --pointer-check
 ^Removing function pointers and virtual functions$
-^\s*IF \*container_ptr->fp_tbl\[\(signed long int\)1\] == f1 THEN GOTO [0-9]$
-^\s*IF \*container_ptr->fp_tbl\[\(signed long int\)1\] == f2 THEN GOTO [0-9]$
-^\s*IF \*container_ptr->fp_tbl\[\(signed long int\)1\] == f3 THEN GOTO [0-9]$
-^\s*IF \*container_ptr->fp_tbl\[\(signed long int\)1\] == f4 THEN GOTO [0-9]$
-^\s*IF \*container_ptr->fp_tbl\[\(signed long int\)1\] == f5 THEN GOTO [0-9]$
-^\s*IF \*container_ptr->fp_tbl\[\(signed long int\)1\] == f6 THEN GOTO [0-9]$
-^\s*IF \*container_ptr->fp_tbl\[\(signed long int\)1\] == f7 THEN GOTO [0-9]$
-^\s*IF \*container_ptr->fp_tbl\[\(signed long int\)1\] == f8 THEN GOTO [0-9]$
-^\s*IF \*container_ptr->fp_tbl\[\(signed long int\)1\] == f9 THEN GOTO [0-9]$
+^\s*IF \*container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f1 THEN GOTO [0-9]$
+^\s*IF \*container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f2 THEN GOTO [0-9]$
+^\s*IF \*container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f3 THEN GOTO [0-9]$
+^\s*IF \*container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f4 THEN GOTO [0-9]$
+^\s*IF \*container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f5 THEN GOTO [0-9]$
+^\s*IF \*container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f6 THEN GOTO [0-9]$
+^\s*IF \*container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f7 THEN GOTO [0-9]$
+^\s*IF \*container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f8 THEN GOTO [0-9]$
+^\s*IF \*container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f9 THEN GOTO [0-9]$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/goto-analyzer/no-match-pointer-const-struct-array-literal-non-const-fp/test.desc

@@ -2,15 +2,15 @@ CORE
 main.c
 --show-goto-functions --verbosity 10 --pointer-check
 ^Removing function pointers and virtual functions$
-^\s*IF container_ptr->fp_tbl\[\(signed long int\)1\] == f1 THEN GOTO [0-9]$
-^\s*IF container_ptr->fp_tbl\[\(signed long int\)1\] == f2 THEN GOTO [0-9]$
-^\s*IF container_ptr->fp_tbl\[\(signed long int\)1\] == f3 THEN GOTO [0-9]$
-^\s*IF container_ptr->fp_tbl\[\(signed long int\)1\] == f4 THEN GOTO [0-9]$
-^\s*IF container_ptr->fp_tbl\[\(signed long int\)1\] == f5 THEN GOTO [0-9]$
-^\s*IF container_ptr->fp_tbl\[\(signed long int\)1\] == f6 THEN GOTO [0-9]$
-^\s*IF container_ptr->fp_tbl\[\(signed long int\)1\] == f7 THEN GOTO [0-9]$
-^\s*IF container_ptr->fp_tbl\[\(signed long int\)1\] == f8 THEN GOTO [0-9]$
-^\s*IF container_ptr->fp_tbl\[\(signed long int\)1\] == f9 THEN GOTO [0-9]$
+^\s*IF container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f1 THEN GOTO [0-9]$
+^\s*IF container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f2 THEN GOTO [0-9]$
+^\s*IF container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f3 THEN GOTO [0-9]$
+^\s*IF container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f4 THEN GOTO [0-9]$
+^\s*IF container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f5 THEN GOTO [0-9]$
+^\s*IF container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f6 THEN GOTO [0-9]$
+^\s*IF container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f7 THEN GOTO [0-9]$
+^\s*IF container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f8 THEN GOTO [0-9]$
+^\s*IF container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f9 THEN GOTO [0-9]$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/goto-instrument/approx-array-variable-const-fp-only-remove-const/test.desc

@@ -1,15 +1,15 @@
 CORE
 main.c
 --verbosity 10 --pointer-check --remove-const-function-pointers
-^\s*IF fp_tbl\[\(signed long int\)i\] == f2 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f3 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f4 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f2 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f3 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f4 THEN GOTO [0-9]$
 ^SIGNAL=0$
 --
-^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f1 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f5 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f6 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f7 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f8 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f9 THEN GOTO [0-9]$
 ^warning: ignoring

regression/goto-instrument/approx-array-variable-const-fp-remove-all-fp/test.desc

@@ -1,15 +1,15 @@
 CORE
 main.c
 --verbosity 10 --pointer-check --remove-function-pointers
-^\s*IF fp_tbl\[\(signed long int\)i\] == f2 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f3 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f4 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f2 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f3 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f4 THEN GOTO [0-9]$
 ^SIGNAL=0$
 --
-^\s*IF fp_tbl\[\(signed long int\)i\] == f1 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f5 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f6 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f7 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f8 THEN GOTO [0-9]$
-^\s*IF fp_tbl\[\(signed long int\)i\] == f9 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f1 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f5 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f6 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f7 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f8 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f9 THEN GOTO [0-9]$
 ^warning: ignoring