>>> Building on exopi-1 under devel/cbmc BDEPENDS = [devel/bison;devel/gmake] DIST = [devel/cbmc:minisat2_2.2.1.orig.tar.gz;devel/cbmc:cbmc-cbmc-5.5.tar.gz] FULLPKGNAME = cbmc-5.5p5 (Junk lock obtained for exopi-1 at 1732149079.42) >>> Running depends in devel/cbmc at 1732149079.46 last junk was in devel/py-testtools,python3 /usr/sbin/pkg_add -aI -Drepair bison-3.8.2 was: /usr/sbin/pkg_add -aI -Drepair bison-3.8.2 gmake-4.4.1 /usr/sbin/pkg_add -aI -Drepair bison-3.8.2 >>> Running show-prepare-results in devel/cbmc at 1732149084.21 ===> devel/cbmc ===> Building from scratch cbmc-5.5p5 ===> cbmc-5.5p5 depends on: bison-* -> bison-3.8.2 ===> cbmc-5.5p5 depends on: gmake-* -> gmake-4.4.1 ===> Verifying specs: c m c++ c++abi pthread ===> found c.100.3 m.10.1 c++.10.0 c++abi.7.0 pthread.27.1 bison-3.8.2 gmake-4.4.1 (Junk lock released for exopi-1 at 1732149084.83) distfiles size=5319101 >>> Running patch in devel/cbmc at 1732149084.86 ===> devel/cbmc ===> Checking files for cbmc-5.5p5 `/exopi-cvs/ports/distfiles/cbmc-cbmc-5.5.tar.gz' is up to date. `/exopi-cvs/ports/distfiles/minisat2_2.2.1.orig.tar.gz' is up to date. >> (SHA256) all files: OK ===> Extracting for cbmc-5.5p5 mv /exopi-obj/pobj/cbmc-5.5/minisat2-2.2.1 /exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/minisat-2.2.1 cd /exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/minisat-2.2.1; patch -z .bak -p1 < ../scripts/minisat-2.2.1-patch Hmm... Looks like a unified diff to me... The text leading up to this was: -------------------------- |diff -urN minisat-2.2.1/minisat/core/Solver.cc minisat-2.2.1.patched/minisat/core/Solver.cc |--- minisat-2.2.1/minisat/core/Solver.cc 2011-02-21 13:31:17.000000000 +0000 |+++ minisat-2.2.1.patched/minisat/core/Solver.cc 2016-03-05 16:21:17.000000000 +0000 -------------------------- Patching file minisat/core/Solver.cc using Plan A... Hunk #1 succeeded at 210. Hunk #2 succeeded at 666. Hmm... The next patch looks like a unified diff to me... The text leading up to this was: -------------------------- |diff -urN minisat-2.2.1/minisat/core/SolverTypes.h minisat-2.2.1.patched/minisat/core/SolverTypes.h |--- minisat-2.2.1/minisat/core/SolverTypes.h 2011-02-21 13:31:17.000000000 +0000 |+++ minisat-2.2.1.patched/minisat/core/SolverTypes.h 2016-03-05 16:29:42.000000000 +0000 -------------------------- Patching file minisat/core/SolverTypes.h using Plan A... Hunk #1 succeeded at 47. Hunk #2 succeeded at 55. Hunk #3 succeeded at 142. Hunk #4 succeeded at 158. Hmm... The next patch looks like a unified diff to me... The text leading up to this was: -------------------------- |diff -urN minisat-2.2.1/minisat/mtl/IntTypes.h minisat-2.2.1.patched/minisat/mtl/IntTypes.h |--- minisat-2.2.1/minisat/mtl/IntTypes.h 2011-02-21 13:31:17.000000000 +0000 |+++ minisat-2.2.1.patched/minisat/mtl/IntTypes.h 2016-03-05 16:21:17.000000000 +0000 -------------------------- Patching file minisat/mtl/IntTypes.h using Plan A... Hunk #1 succeeded at 31. Hmm... The next patch looks like a unified diff to me... The text leading up to this was: -------------------------- |diff -urN minisat-2.2.1/minisat/mtl/Vec.h minisat-2.2.1.patched/minisat/mtl/Vec.h |--- minisat-2.2.1/minisat/mtl/Vec.h 2011-02-21 13:31:17.000000000 +0000 |+++ minisat-2.2.1.patched/minisat/mtl/Vec.h 2016-03-05 16:21:17.000000000 +0000 -------------------------- Patching file minisat/mtl/Vec.h using Plan A... Hunk #1 succeeded at 96. Hmm... The next patch looks like a unified diff to me... The text leading up to this was: -------------------------- |diff -urN minisat-2.2.1/minisat/simp/SimpSolver.cc minisat-2.2.1.patched/minisat/simp/SimpSolver.cc |--- minisat-2.2.1/minisat/simp/SimpSolver.cc 2011-02-21 13:31:17.000000000 +0000 |+++ minisat-2.2.1.patched/minisat/simp/SimpSolver.cc 2016-03-05 16:21:17.000000000 +0000 -------------------------- Patching file minisat/simp/SimpSolver.cc using Plan A... Hunk #1 succeeded at 130. Hunk #2 succeeded at 225. Hunk #3 succeeded at 261. Hmm... The next patch looks like a unified diff to me... The text leading up to this was: -------------------------- |diff -urN minisat-2.2.1/minisat/utils/Options.h minisat-2.2.1.patched/minisat/utils/Options.h |--- minisat-2.2.1/minisat/utils/Options.h 2011-02-21 13:31:17.000000000 +0000 |+++ minisat-2.2.1.patched/minisat/utils/Options.h 2016-03-05 16:21:17.000000000 +0000 -------------------------- Patching file minisat/utils/Options.h using Plan A... Hunk #1 succeeded at 60. Hunk #2 succeeded at 282. Hmm... The next patch looks like a unified diff to me... The text leading up to this was: -------------------------- |diff -urN minisat-2.2.1/minisat/utils/ParseUtils.h minisat-2.2.1.patched/minisat/utils/ParseUtils.h |--- minisat-2.2.1/minisat/utils/ParseUtils.h 2011-02-21 13:31:17.000000000 +0000 |+++ minisat-2.2.1.patched/minisat/utils/ParseUtils.h 2016-03-05 16:21:17.000000000 +0000 -------------------------- Patching file minisat/utils/ParseUtils.h using Plan A... Hunk #1 succeeded at 24. Hunk #2 succeeded at 35. Hunk #3 succeeded at 43. done ===> Patching for cbmc-5.5p5 ===> Applying OpenBSD patch patch-src_ansi-c_Makefile Hmm... Looks like a unified diff to me... The text leading up to this was: -------------------------- |Newer bison includes the defines file in the parser so the name must match. | |Index: src/ansi-c/Makefile |--- src/ansi-c/Makefile.orig |+++ src/ansi-c/Makefile -------------------------- Patching file src/ansi-c/Makefile using Plan A... Hunk #1 succeeded at 36. done ===> Applying OpenBSD patch patch-src_big-int_allocainc_h Hmm... Looks like a unified diff to me... The text leading up to this was: -------------------------- |--- src/big-int/allocainc.h.orig Sun Oct 16 18:58:41 2016 |+++ src/big-int/allocainc.h Sun Oct 16 18:58:58 2016 -------------------------- Patching file src/big-int/allocainc.h using Plan A... Hunk #1 succeeded at 41. done ===> Applying OpenBSD patch patch-src_common Hmm... Looks like a unified diff to me... The text leading up to this was: -------------------------- |--- src/common.orig Sat Aug 20 14:08:13 2016 |+++ src/common Fri Oct 14 16:29:34 2016 -------------------------- Patching file src/common using Plan A... Hunk #1 succeeded at 9. Hunk #2 succeeded at 22. Hunk #3 succeeded at 61. done ===> Applying OpenBSD patch patch-src_jsil_Makefile Hmm... Looks like a unified diff to me... The text leading up to this was: -------------------------- |Newer bison includes the defines file in the parser so the name must match. | |Index: src/jsil/Makefile |--- src/jsil/Makefile.orig |+++ src/jsil/Makefile -------------------------- Patching file src/jsil/Makefile using Plan A... Hunk #1 succeeded at 19. done ===> Applying OpenBSD patch patch-src_json_Makefile Hmm... Looks like a unified diff to me... The text leading up to this was: -------------------------- |Newer bison includes the defines file in the parser so the name must match. | |Index: src/json/Makefile |--- src/json/Makefile.orig |+++ src/json/Makefile -------------------------- Patching file src/json/Makefile using Plan A... Hunk #1 succeeded at 15. done ===> Applying OpenBSD patch patch-src_memory-models_Makefile Hmm... Looks like a unified diff to me... The text leading up to this was: -------------------------- |Newer bison includes the defines file in the parser so the name must match. | |Index: src/memory-models/Makefile |--- src/memory-models/Makefile.orig |+++ src/memory-models/Makefile -------------------------- Patching file src/memory-models/Makefile using Plan A... Hunk #1 succeeded at 16. done ===> Applying OpenBSD patch patch-src_xmllang_Makefile Hmm... Looks like a unified diff to me... The text leading up to this was: -------------------------- |Newer bison includes the defines file in the parser so the name must match. | |Index: src/xmllang/Makefile |--- src/xmllang/Makefile.orig |+++ src/xmllang/Makefile -------------------------- Patching file src/xmllang/Makefile using Plan A... Hunk #1 succeeded at 15. done ===> Compiler link: clang -> /usr/bin/clang ===> Compiler link: clang++ -> /usr/bin/clang++ ===> Compiler link: cc -> /usr/bin/cc ===> Compiler link: c++ -> /usr/bin/c++ >>> Running configure in devel/cbmc at 1732149086.05 ===> devel/cbmc ===> Generating configure for cbmc-5.5p5 ===> Configuring for cbmc-5.5p5 >>> Running build in devel/cbmc at 1732149086.28 ===> devel/cbmc ===> Building for cbmc-5.5p5 ## Entering big-int gmake -C big-int gmake[1]: Entering directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/big-int' c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -o bigint-func.o bigint-func.cc c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -o bigint.o bigint.cc c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -o bigint-test.o bigint-test.cc bigint-test.cc:30:49: warning: 'fscanf' may overflow; destination buffer in argument 3 has size 4096, but the corresponding specifier may require size 4097 [-Wfortify-source] return 1 == fscanf (f, " %4096[-+0-9a-zA-Z]", buf) ^ 1 warning generated. c++ -o test-bigint -Wl,--start-group bigint-func.o bigint.o bigint-test.o -Wl,--end-group ar rc big-int.a bigint-func.o bigint.o gmake[1]: Leaving directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/big-int' ## Entering util gmake -C util gmake[1]: Entering directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/util' c++ -o irep_ids_convert irep_ids_convert.cpp ./irep_ids_convert header < irep_ids.txt > irep_ids.h c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o arith_tools.o arith_tools.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o base_type.o base_type.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cmdline.o cmdline.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o config.o config.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o symbol_table.o symbol_table.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o expr.o expr.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o expr_util.o expr_util.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o i2string.o i2string.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o irep.o irep.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o language.o language.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o lispexpr.o lispexpr.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o lispirep.o lispirep.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o source_location.o source_location.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o message.o message.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o language_file.o language_file.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o mp_arith.o mp_arith.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o namespace.o namespace.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o parse_options.o parse_options.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o rename.o rename.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o replace_expr.o replace_expr.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o threeval.o threeval.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o typecheck.o typecheck.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o graph.o graph.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o type.o type.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cnf_simplify.o cnf_simplify.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o pointer_predicates.o pointer_predicates.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o merge_irep.o merge_irep.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o parser.o parser.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o replace_symbol.o replace_symbol.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o json.o json.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o get_base_name.o get_base_name.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o simplify_expr.o simplify_expr.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o simplify_expr_floatbv.o simplify_expr_floatbv.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o simplify_expr_int.o simplify_expr_int.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o simplify_expr_array.o simplify_expr_array.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o simplify_expr_struct.o simplify_expr_struct.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o simplify_expr_boolean.o simplify_expr_boolean.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o simplify_expr_pointer.o simplify_expr_pointer.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o get_module.o get_module.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o string_hash.o string_hash.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o string_container.o string_container.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o identifier.o identifier.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o rational.o rational.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o options.o options.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o c_misc.o c_misc.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o dstring.o dstring.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o find_symbols.o find_symbols.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o rational_tools.o rational_tools.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o ui_message.o ui_message.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o simplify_utils.o simplify_utils.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o time_stopping.o time_stopping.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o symbol.o symbol.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o irep_hash_container.o irep_hash_container.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cout_message.o cout_message.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o type_eq.o type_eq.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o guard.o guard.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o array_name.o array_name.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o message_stream.o message_stream.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o substitute.o substitute.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o decision_procedure.o decision_procedure.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o union_find.o union_find.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o xml.o xml.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o xml_irep.o xml_irep.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o xml_expr.o xml_expr.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o std_types.o std_types.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o std_code.o std_code.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o format_constant.o format_constant.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o find_macros.o find_macros.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o ref_expr_set.o ref_expr_set.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o std_expr.o std_expr.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o irep_serialization.o irep_serialization.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o fixedbv.o fixedbv.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o rename_symbol.o rename_symbol.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o ieee_float.o ieee_float.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o signal_catcher.o signal_catcher.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o pointer_offset_size.o pointer_offset_size.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o bv_arithmetic.o bv_arithmetic.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o tempdir.o tempdir.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o tempfile.o tempfile.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o timer.o timer.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o unicode.o unicode.cpp ./irep_ids_convert table < irep_ids.txt > irep_ids.inc c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o irep_ids.o irep_ids.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o byte_operators.o byte_operators.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o string2int.o string2int.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o file_util.o file_util.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o memory_info.o memory_info.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o pipe_stream.o pipe_stream.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o irep_hash.o irep_hash.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o endianness_map.o endianness_map.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o ssa_expr.o ssa_expr.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o json_expr.o json_expr.cpp ar rc util.a arith_tools.o base_type.o cmdline.o config.o symbol_table.o expr.o expr_util.o i2string.o irep.o language.o lispexpr.o lispirep.o source_location.o message.o language_file.o mp_arith.o namespace.o parse_options.o rename.o replace_expr.o threeval.o typecheck.o graph.o type.o cnf_simplify.o pointer_predicates.o merge_irep.o parser.o replace_symbol.o json.o get_base_name.o simplify_expr.o simplify_expr_floatbv.o simplify_expr_int.o simplify_expr_array.o simplify_expr_struct.o simplify_expr_boolean.o simplify_expr_pointer.o get_module.o string_hash.o string_container.o identifier.o rational.o options.o c_misc.o dstring.o find_symbols.o rational_tools.o ui_message.o simplify_utils.o time_stopping.o symbol.o irep_hash_container.o cout_message.o type_eq.o guard.o array_name.o message_stream.o substitute.o decision_procedure.o union_find.o xml.o xml_irep.o xml_expr.o std_types.o std_code.o format_constant.o find_macros.o ref_expr_set.o std_expr.o irep_serialization.o fixedbv.o rename_symbol.o ieee_float.o signal_catcher.o pointer_offset_size.o bv_arithmetic.o tempdir.o tempfile.o timer.o unicode.o irep_ids.o byte_operators.o string2int.o file_util.o memory_info.o pipe_stream.o irep_hash.o endianness_map.o ssa_expr.o json_expr.o gmake[1]: Leaving directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/util' ## Entering langapi gmake -C langapi gmake[1]: Entering directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/langapi' c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o mode.o mode.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o language_ui.o language_ui.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o languages.o languages.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o language_util.o language_util.cpp ar rc langapi.a mode.o language_ui.o languages.o language_util.o gmake[1]: Leaving directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/langapi' ## Entering ansi-c gmake -C ansi-c gmake[1]: Entering directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/ansi-c' c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o c_typecast.o c_typecast.cpp bison -y -v $flags -pyyansi_c --defines=ansi_c_y.tab.h parser.y -o ansi_c_y.tab.cpp parser.y:36.22-27: warning: POSIX Yacc does not support string literals [-Wyacc] 36 | %token TOK_AUTO "auto" | ^~~~~~ parser.y:37.22-27: warning: POSIX Yacc does not support string literals [-Wyacc] 37 | %token TOK_BOOL "bool" | ^~~~~~ parser.y:38.22-30: warning: POSIX Yacc does not support string literals [-Wyacc] 38 | %token TOK_COMPLEX "complex" | ^~~~~~~~~ parser.y:39.22-28: warning: POSIX Yacc does not support string literals [-Wyacc] 39 | %token TOK_BREAK "break" | ^~~~~~~ parser.y:40.22-27: warning: POSIX Yacc does not support string literals [-Wyacc] 40 | %token TOK_CASE "case" | ^~~~~~ parser.y:41.22-27: warning: POSIX Yacc does not support string literals [-Wyacc] 41 | %token TOK_CHAR "char" | ^~~~~~ parser.y:42.22-28: warning: POSIX Yacc does not support string literals [-Wyacc] 42 | %token TOK_CONST "const" | ^~~~~~~ parser.y:43.22-31: warning: POSIX Yacc does not support string literals [-Wyacc] 43 | %token TOK_CONTINUE "continue" | ^~~~~~~~~~ parser.y:44.22-30: warning: POSIX Yacc does not support string literals [-Wyacc] 44 | %token TOK_DEFAULT "default" | ^~~~~~~~~ parser.y:45.22-25: warning: POSIX Yacc does not support string literals [-Wyacc] 45 | %token TOK_DO "do" | ^~~~ parser.y:46.22-29: warning: POSIX Yacc does not support string literals [-Wyacc] 46 | %token TOK_DOUBLE "double" | ^~~~~~~~ parser.y:47.22-27: warning: POSIX Yacc does not support string literals [-Wyacc] 47 | %token TOK_ELSE "else" | ^~~~~~ parser.y:48.22-27: warning: POSIX Yacc does not support string literals [-Wyacc] 48 | %token TOK_ENUM "enum" | ^~~~~~ parser.y:49.22-29: warning: POSIX Yacc does not support string literals [-Wyacc] 49 | %token TOK_EXTERN "extern" | ^~~~~~~~ parser.y:50.22-28: warning: POSIX Yacc does not support string literals [-Wyacc] 50 | %token TOK_FLOAT "float" | ^~~~~~~ parser.y:51.22-26: warning: POSIX Yacc does not support string literals [-Wyacc] 51 | %token TOK_FOR "for" | ^~~~~ parser.y:52.22-27: warning: POSIX Yacc does not support string literals [-Wyacc] 52 | %token TOK_GOTO "goto" | ^~~~~~ parser.y:53.22-25: warning: POSIX Yacc does not support string literals [-Wyacc] 53 | %token TOK_IF "if" | ^~~~ parser.y:54.22-29: warning: POSIX Yacc does not support string literals [-Wyacc] 54 | %token TOK_INLINE "inline" | ^~~~~~~~ parser.y:55.22-26: warning: POSIX Yacc does not support string literals [-Wyacc] 55 | %token TOK_INT "int" | ^~~~~ parser.y:56.22-27: warning: POSIX Yacc does not support string literals [-Wyacc] 56 | %token TOK_LONG "long" | ^~~~~~ parser.y:57.22-31: warning: POSIX Yacc does not support string literals [-Wyacc] 57 | %token TOK_REGISTER "register" | ^~~~~~~~~~ parser.y:58.22-31: warning: POSIX Yacc does not support string literals [-Wyacc] 58 | %token TOK_RESTRICT "restrict" | ^~~~~~~~~~ parser.y:59.22-29: warning: POSIX Yacc does not support string literals [-Wyacc] 59 | %token TOK_RETURN "return" | ^~~~~~~~ parser.y:60.22-28: warning: POSIX Yacc does not support string literals [-Wyacc] 60 | %token TOK_SHORT "short" | ^~~~~~~ parser.y:61.22-29: warning: POSIX Yacc does not support string literals [-Wyacc] 61 | %token TOK_SIGNED "signed" | ^~~~~~~~ parser.y:62.22-29: warning: POSIX Yacc does not support string literals [-Wyacc] 62 | %token TOK_SIZEOF "sizeof" | ^~~~~~~~ parser.y:63.22-29: warning: POSIX Yacc does not support string literals [-Wyacc] 63 | %token TOK_STATIC "static" | ^~~~~~~~ parser.y:64.22-29: warning: POSIX Yacc does not support string literals [-Wyacc] 64 | %token TOK_STRUCT "struct" | ^~~~~~~~ parser.y:65.22-29: warning: POSIX Yacc does not support string literals [-Wyacc] 65 | %token TOK_SWITCH "switch" | ^~~~~~~~ parser.y:66.22-30: warning: POSIX Yacc does not support string literals [-Wyacc] 66 | %token TOK_TYPEDEF "typedef" | ^~~~~~~~~ parser.y:67.22-28: warning: POSIX Yacc does not support string literals [-Wyacc] 67 | %token TOK_UNION "union" | ^~~~~~~ parser.y:68.22-31: warning: POSIX Yacc does not support string literals [-Wyacc] 68 | %token TOK_UNSIGNED "unsigned" | ^~~~~~~~~~ parser.y:69.22-27: warning: POSIX Yacc does not support string literals [-Wyacc] 69 | %token TOK_VOID "void" | ^~~~~~ parser.y:70.22-31: warning: POSIX Yacc does not support string literals [-Wyacc] 70 | %token TOK_VOLATILE "volatile" | ^~~~~~~~~~ parser.y:71.22-30: warning: POSIX Yacc does not support string literals [-Wyacc] 71 | %token TOK_WCHAR_T "wchar_t" | ^~~~~~~~~ parser.y:72.22-28: warning: POSIX Yacc does not support string literals [-Wyacc] 72 | %token TOK_WHILE "while" | ^~~~~~~ parser.y:76.22-25: warning: POSIX Yacc does not support string literals [-Wyacc] 76 | %token TOK_ARROW "->" | ^~~~ parser.y:77.22-25: warning: POSIX Yacc does not support string literals [-Wyacc] 77 | %token TOK_INCR "++" | ^~~~ parser.y:78.22-25: warning: POSIX Yacc does not support string literals [-Wyacc] 78 | %token TOK_DECR "--" | ^~~~ parser.y:79.22-25: warning: POSIX Yacc does not support string literals [-Wyacc] 79 | %token TOK_SHIFTLEFT "<<" | ^~~~ parser.y:80.23-26: warning: POSIX Yacc does not support string literals [-Wyacc] 80 | %token TOK_SHIFTRIGHT ">>" | ^~~~ parser.y:81.22-25: warning: POSIX Yacc does not support string literals [-Wyacc] 81 | %token TOK_LE "<=" | ^~~~ parser.y:82.22-25: warning: POSIX Yacc does not support string literals [-Wyacc] 82 | %token TOK_GE ">=" | ^~~~ parser.y:83.22-25: warning: POSIX Yacc does not support string literals [-Wyacc] 83 | %token TOK_EQ "==" | ^~~~ parser.y:84.22-25: warning: POSIX Yacc does not support string literals [-Wyacc] 84 | %token TOK_NE "!=" | ^~~~ parser.y:85.22-25: warning: POSIX Yacc does not support string literals [-Wyacc] 85 | %token TOK_ANDAND "&&" | ^~~~ parser.y:86.22-25: warning: POSIX Yacc does not support string literals [-Wyacc] 86 | %token TOK_OROR "||" | ^~~~ parser.y:87.22-26: warning: POSIX Yacc does not support string literals [-Wyacc] 87 | %token TOK_ELLIPSIS "..." | ^~~~~ parser.y:91.24-27: warning: POSIX Yacc does not support string literals [-Wyacc] 91 | %token TOK_MULTASSIGN "*=" | ^~~~ parser.y:92.24-27: warning: POSIX Yacc does not support string literals [-Wyacc] 92 | %token TOK_DIVASSIGN "/=" | ^~~~ parser.y:93.24-27: warning: POSIX Yacc does not support string literals [-Wyacc] 93 | %token TOK_MODASSIGN "%=" | ^~~~ parser.y:94.24-27: warning: POSIX Yacc does not support string literals [-Wyacc] 94 | %token TOK_PLUSASSIGN "+=" | ^~~~ parser.y:95.24-27: warning: POSIX Yacc does not support string literals [-Wyacc] 95 | %token TOK_MINUSASSIGN "-=" | ^~~~ parser.y:96.24-28: warning: POSIX Yacc does not support string literals [-Wyacc] 96 | %token TOK_SHLASSIGN "<<=" | ^~~~~ parser.y:97.24-28: warning: POSIX Yacc does not support string literals [-Wyacc] 97 | %token TOK_SHRASSIGN ">>=" | ^~~~~ parser.y:98.24-27: warning: POSIX Yacc does not support string literals [-Wyacc] 98 | %token TOK_ANDASSIGN "&=" | ^~~~ parser.y:99.24-27: warning: POSIX Yacc does not support string literals [-Wyacc] 99 | %token TOK_XORASSIGN "^=" | ^~~~ parser.y:100.24-27: warning: POSIX Yacc does not support string literals [-Wyacc] 100 | %token TOK_ORASSIGN "|=" | ^~~~ parser.y:114.24-31: warning: POSIX Yacc does not support string literals [-Wyacc] 114 | %token TOK_INT8 "__int8" | ^~~~~~~~ parser.y:115.24-32: warning: POSIX Yacc does not support string literals [-Wyacc] 115 | %token TOK_INT16 "__int16" | ^~~~~~~~~ parser.y:116.24-32: warning: POSIX Yacc does not support string literals [-Wyacc] 116 | %token TOK_INT32 "__int32" | ^~~~~~~~~ parser.y:117.24-32: warning: POSIX Yacc does not support string literals [-Wyacc] 117 | %token TOK_INT64 "__int64" | ^~~~~~~~~ parser.y:118.24-32: warning: POSIX Yacc does not support string literals [-Wyacc] 118 | %token TOK_PTR32 "__ptr32" | ^~~~~~~~~ parser.y:119.24-32: warning: POSIX Yacc does not support string literals [-Wyacc] 119 | %token TOK_PTR64 "__ptr64" | ^~~~~~~~~ parser.y:120.24-31: warning: POSIX Yacc does not support string literals [-Wyacc] 120 | %token TOK_TYPEOF "typeof" | ^~~~~~~~ parser.y:121.26-38: warning: POSIX Yacc does not support string literals [-Wyacc] 121 | %token TOK_GCC_AUTO_TYPE "__auto_type" | ^~~~~~~~~~~~~ parser.y:122.24-34: warning: POSIX Yacc does not support string literals [-Wyacc] 122 | %token TOK_GCC_FLOAT80 "__float80" | ^~~~~~~~~~~ parser.y:123.25-36: warning: POSIX Yacc does not support string literals [-Wyacc] 123 | %token TOK_GCC_FLOAT128 "__float128" | ^~~~~~~~~~~~ parser.y:124.23-32: warning: POSIX Yacc does not support string literals [-Wyacc] 124 | %token TOK_GCC_INT128 "__int128" | ^~~~~~~~~~ parser.y:125.26-37: warning: POSIX Yacc does not support string literals [-Wyacc] 125 | %token TOK_GCC_DECIMAL32 "_Decimal32" | ^~~~~~~~~~~~ parser.y:126.26-37: warning: POSIX Yacc does not support string literals [-Wyacc] 126 | %token TOK_GCC_DECIMAL64 "_Decimal64" | ^~~~~~~~~~~~ parser.y:127.27-39: warning: POSIX Yacc does not support string literals [-Wyacc] 127 | %token TOK_GCC_DECIMAL128 "_Decimal128" | ^~~~~~~~~~~~~ parser.y:128.24-32: warning: POSIX Yacc does not support string literals [-Wyacc] 128 | %token TOK_GCC_ASM "__asm__" | ^~~~~~~~~ parser.y:129.26-53: warning: POSIX Yacc does not support string literals [-Wyacc] 129 | %token TOK_GCC_ASM_PAREN "__asm__ (with parentheses)" | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~ parser.y:130.26-40: warning: POSIX Yacc does not support string literals [-Wyacc] 130 | %token TOK_GCC_ATTRIBUTE "__attribute__" | ^~~~~~~~~~~~~~~ parser.y:131.34-42: warning: POSIX Yacc does not support string literals [-Wyacc] 131 | %token TOK_GCC_ATTRIBUTE_ALIGNED "aligned" | ^~~~~~~~~ parser.y:132.44-62: warning: POSIX Yacc does not support string literals [-Wyacc] 132 | %token TOK_GCC_ATTRIBUTE_TRANSPARENT_UNION "transparent_union" | ^~~~~~~~~~~~~~~~~~~ parser.y:133.33-40: warning: POSIX Yacc does not support string literals [-Wyacc] 133 | %token TOK_GCC_ATTRIBUTE_PACKED "packed" | ^~~~~~~~ parser.y:134.38-50: warning: POSIX Yacc does not support string literals [-Wyacc] 134 | %token TOK_GCC_ATTRIBUTE_VECTOR_SIZE "vector_size" | ^~~~~~~~~~~~~ parser.y:135.31-36: warning: POSIX Yacc does not support string literals [-Wyacc] 135 | %token TOK_GCC_ATTRIBUTE_MODE "mode" | ^~~~~~ parser.y:136.37-52: warning: POSIX Yacc does not support string literals [-Wyacc] 136 | %token TOK_GCC_ATTRIBUTE_GNU_INLINE "__gnu_inline__" | ^~~~~~~~~~~~~~~~ parser.y:137.31-36: warning: POSIX Yacc does not support string literals [-Wyacc] 137 | %token TOK_GCC_ATTRIBUTE_WEAK "weak" | ^~~~~~ parser.y:138.32-38: warning: POSIX Yacc does not support string literals [-Wyacc] 138 | %token TOK_GCC_ATTRIBUTE_ALIAS "alias" | ^~~~~~~ parser.y:139.34-42: warning: POSIX Yacc does not support string literals [-Wyacc] 139 | %token TOK_GCC_ATTRIBUTE_SECTION "section" | ^~~~~~~~~ parser.y:140.35-44: warning: POSIX Yacc does not support string literals [-Wyacc] 140 | %token TOK_GCC_ATTRIBUTE_NORETURN "noreturn" | ^~~~~~~~~~ parser.y:141.38-50: warning: POSIX Yacc does not support string literals [-Wyacc] 141 | %token TOK_GCC_ATTRIBUTE_CONSTRUCTOR "constructor" | ^~~~~~~~~~~~~ parser.y:142.37-48: warning: POSIX Yacc does not support string literals [-Wyacc] 142 | %token TOK_GCC_ATTRIBUTE_DESTRUCTOR "destructor" | ^~~~~~~~~~~~ parser.y:143.24-34: warning: POSIX Yacc does not support string literals [-Wyacc] 143 | %token TOK_GCC_LABEL "__label__" | ^~~~~~~~~~~ parser.y:144.24-30: warning: POSIX Yacc does not support string literals [-Wyacc] 144 | %token TOK_MSC_ASM "__asm" | ^~~~~~~ parser.y:145.24-32: warning: POSIX Yacc does not support string literals [-Wyacc] 145 | %token TOK_MSC_BASED "__based" | ^~~~~~~~~ parser.y:146.30-46: warning: POSIX Yacc does not support string literals [-Wyacc] 146 | %token TOK_CW_VAR_ARG_TYPEOF "_var_arg_typeof" | ^~~~~~~~~~~~~~~~~ parser.y:147.27-44: warning: POSIX Yacc does not support string literals [-Wyacc] 147 | %token TOK_BUILTIN_VA_ARG "__builtin_va_arg" | ^~~~~~~~~~~~~~~~~~ parser.y:148.43-72: warning: POSIX Yacc does not support string literals [-Wyacc] 148 | %token TOK_GCC_BUILTIN_TYPES_COMPATIBLE_P "__builtin_types_compatible... | ^~~~~~~~~~~~~~~~~~~~~~~~~~~ parser.y:149.24-35: warning: POSIX Yacc does not support string literals [-Wyacc] 149 | %token TOK_OFFSETOF "__offsetof" | ^~~~~~~~~~~~ parser.y:150.24-36: warning: POSIX Yacc does not support string literals [-Wyacc] 150 | %token TOK_ALIGNOF "__alignof__" | ^~~~~~~~~~~~~ parser.y:151.24-30: warning: POSIX Yacc does not support string literals [-Wyacc] 151 | %token TOK_MSC_TRY "__try" | ^~~~~~~ parser.y:152.24-34: warning: POSIX Yacc does not support string literals [-Wyacc] 152 | %token TOK_MSC_FINALLY "__finally" | ^~~~~~~~~~~ parser.y:153.24-33: warning: POSIX Yacc does not support string literals [-Wyacc] 153 | %token TOK_MSC_EXCEPT "__except" | ^~~~~~~~~~ parser.y:154.24-32: warning: POSIX Yacc does not support string literals [-Wyacc] 154 | %token TOK_MSC_LEAVE "__leave" | ^~~~~~~~~ parser.y:155.25-36: warning: POSIX Yacc does not support string literals [-Wyacc] 155 | %token TOK_MSC_DECLSPEC "__declspec" | ^~~~~~~~~~~~ parser.y:156.24-36: warning: POSIX Yacc does not support string literals [-Wyacc] 156 | %token TOK_INTERFACE "__interface" | ^~~~~~~~~~~~~ parser.y:157.24-32: warning: POSIX Yacc does not support string literals [-Wyacc] 157 | %token TOK_CDECL "__cdecl" | ^~~~~~~~~ parser.y:158.24-34: warning: POSIX Yacc does not support string literals [-Wyacc] 158 | %token TOK_STDCALL "__stdcall" | ^~~~~~~~~~~ parser.y:159.24-35: warning: POSIX Yacc does not support string literals [-Wyacc] 159 | %token TOK_FASTCALL "__fastcall" | ^~~~~~~~~~~~ parser.y:160.24-34: warning: POSIX Yacc does not support string literals [-Wyacc] 160 | %token TOK_CLRCALL "__clrcall" | ^~~~~~~~~~~ parser.y:161.24-31: warning: POSIX Yacc does not support string literals [-Wyacc] 161 | %token TOK_FORALL "forall" | ^~~~~~~~ parser.y:162.24-31: warning: POSIX Yacc does not support string literals [-Wyacc] 162 | %token TOK_EXISTS "exists" | ^~~~~~~~ parser.y:163.24-33: warning: POSIX Yacc does not support string literals [-Wyacc] 163 | %token TOK_ACSL_FORALL "\\forall" | ^~~~~~~~~~ parser.y:164.24-33: warning: POSIX Yacc does not support string literals [-Wyacc] 164 | %token TOK_ACSL_EXISTS "\\exists" | ^~~~~~~~~~ parser.y:165.24-33: warning: POSIX Yacc does not support string literals [-Wyacc] 165 | %token TOK_ARRAY_OF "array_of" | ^~~~~~~~~~ parser.y:166.30-50: warning: POSIX Yacc does not support string literals [-Wyacc] 166 | %token TOK_CPROVER_BITVECTOR "__CPROVER_bitvector" | ^~~~~~~~~~~~~~~~~~~~~ parser.y:167.28-46: warning: POSIX Yacc does not support string literals [-Wyacc] 167 | %token TOK_CPROVER_FLOATBV "__CPROVER_floatbv" | ^~~~~~~~~~~~~~~~~~~ parser.y:168.28-46: warning: POSIX Yacc does not support string literals [-Wyacc] 168 | %token TOK_CPROVER_FIXEDBV "__CPROVER_fixedbv" | ^~~~~~~~~~~~~~~~~~~ parser.y:169.27-44: warning: POSIX Yacc does not support string literals [-Wyacc] 169 | %token TOK_CPROVER_ATOMIC "__CPROVER_atomic" | ^~~~~~~~~~~~~~~~~~ parser.y:170.25-40: warning: POSIX Yacc does not support string literals [-Wyacc] 170 | %token TOK_CPROVER_BOOL "__CPROVER_bool" | ^~~~~~~~~~~~~~~~ parser.y:171.26-42: warning: POSIX Yacc does not support string literals [-Wyacc] 171 | %token TOK_CPROVER_THROW "__CPROVER_throw" | ^~~~~~~~~~~~~~~~~ parser.y:172.26-42: warning: POSIX Yacc does not support string literals [-Wyacc] 172 | %token TOK_CPROVER_CATCH "__CPROVER_catch" | ^~~~~~~~~~~~~~~~~ parser.y:173.24-38: warning: POSIX Yacc does not support string literals [-Wyacc] 173 | %token TOK_CPROVER_TRY "__CPROVER_try" | ^~~~~~~~~~~~~~~ parser.y:174.28-46: warning: POSIX Yacc does not support string literals [-Wyacc] 174 | %token TOK_CPROVER_FINALLY "__CPROVER_finally" | ^~~~~~~~~~~~~~~~~~~ parser.y:175.24-37: warning: POSIX Yacc does not support string literals [-Wyacc] 175 | %token TOK_CPROVER_ID "__CPROVER_ID" | ^~~~~~~~~~~~~~ parser.y:176.36-61: warning: POSIX Yacc does not support string literals [-Wyacc] 176 | %token TOK_CPROVER_LOOP_INVARIANT "__CPROVER_loop_invariant" | ^~~~~~~~~~~~~~~~~~~~~~~~~~ parser.y:177.30-49: warning: POSIX Yacc does not support string literals [-Wyacc] 177 | %token TOK_CPROVER_REQUIRES "__CPROVER_requires" | ^~~~~~~~~~~~~~~~~~~~ parser.y:178.29-47: warning: POSIX Yacc does not support string literals [-Wyacc] 178 | %token TOK_CPROVER_ENSURES "__CPROVER_ensures" | ^~~~~~~~~~~~~~~~~~~ parser.y:179.24-28: warning: POSIX Yacc does not support string literals [-Wyacc] 179 | %token TOK_IMPLIES "==>" | ^~~~~ parser.y:180.24-29: warning: POSIX Yacc does not support string literals [-Wyacc] 180 | %token TOK_EQUIVALENT "<==>" | ^~~~~~ parser.y:181.24-29: warning: POSIX Yacc does not support string literals [-Wyacc] 181 | %token TOK_TRUE "TRUE" | ^~~~~~ parser.y:182.24-30: warning: POSIX Yacc does not support string literals [-Wyacc] 182 | %token TOK_FALSE "FALSE" | ^~~~~~~ parser.y:183.24-33: warning: POSIX Yacc does not support string literals [-Wyacc] 183 | %token TOK_REAL "__real__" | ^~~~~~~~~~ parser.y:184.24-33: warning: POSIX Yacc does not support string literals [-Wyacc] 184 | %token TOK_IMAG "__imag__" | ^~~~~~~~~~ parser.y:185.24-33: warning: POSIX Yacc does not support string literals [-Wyacc] 185 | %token TOK_ALIGNAS "_Alignas" | ^~~~~~~~~~ parser.y:186.34-42: warning: POSIX Yacc does not support string literals [-Wyacc] 186 | %token TOK_ATOMIC_TYPE_QUALIFIER "_Atomic" | ^~~~~~~~~ parser.y:187.34-44: warning: POSIX Yacc does not support string literals [-Wyacc] 187 | %token TOK_ATOMIC_TYPE_SPECIFIER "_Atomic()" | ^~~~~~~~~~~ parser.y:188.24-33: warning: POSIX Yacc does not support string literals [-Wyacc] 188 | %token TOK_GENERIC "_Generic" | ^~~~~~~~~~ parser.y:189.24-35: warning: POSIX Yacc does not support string literals [-Wyacc] 189 | %token TOK_IMAGINARY "_Imaginary" | ^~~~~~~~~~~~ parser.y:190.24-34: warning: POSIX Yacc does not support string literals [-Wyacc] 190 | %token TOK_NORETURN "_Noreturn" | ^~~~~~~~~~~ parser.y:191.26-41: warning: POSIX Yacc does not support string literals [-Wyacc] 191 | %token TOK_STATIC_ASSERT "_Static_assert" | ^~~~~~~~~~~~~~~~ parser.y:192.25-39: warning: POSIX Yacc does not support string literals [-Wyacc] 192 | %token TOK_THREAD_LOCAL "_Thread_local" | ^~~~~~~~~~~~~~~ parser.y:193.24-32: warning: POSIX Yacc does not support string literals [-Wyacc] 193 | %token TOK_NULLPTR "nullptr" | ^~~~~~~~~ parser.y:194.24-34: warning: POSIX Yacc does not support string literals [-Wyacc] 194 | %token TOK_CONSTEXPR "constexpr" | ^~~~~~~~~~~ parser.y:203.24-30: warning: POSIX Yacc does not support string literals [-Wyacc] 203 | %token TOK_CATCH "catch" | ^~~~~~~ parser.y:204.24-33: warning: POSIX Yacc does not support string literals [-Wyacc] 204 | %token TOK_CHAR16_T "char16_t" | ^~~~~~~~~~ parser.y:205.24-33: warning: POSIX Yacc does not support string literals [-Wyacc] 205 | %token TOK_CHAR32_T "char32_t" | ^~~~~~~~~~ parser.y:206.24-30: warning: POSIX Yacc does not support string literals [-Wyacc] 206 | %token TOK_CLASS "class" | ^~~~~~~ parser.y:207.24-31: warning: POSIX Yacc does not support string literals [-Wyacc] 207 | %token TOK_DELETE "delete" | ^~~~~~~~ parser.y:208.24-33: warning: POSIX Yacc does not support string literals [-Wyacc] 208 | %token TOK_DECLTYPE "decltype" | ^~~~~~~~~~ parser.y:209.24-33: warning: POSIX Yacc does not support string literals [-Wyacc] 209 | %token TOK_EXPLICIT "explicit" | ^~~~~~~~~~ parser.y:210.24-31: warning: POSIX Yacc does not support string literals [-Wyacc] 210 | %token TOK_FRIEND "friend" | ^~~~~~~~ parser.y:211.24-32: warning: POSIX Yacc does not support string literals [-Wyacc] 211 | %token TOK_MUTABLE "mutable" | ^~~~~~~~~ parser.y:212.24-34: warning: POSIX Yacc does not support string literals [-Wyacc] 212 | %token TOK_NAMESPACE "namespace" | ^~~~~~~~~~~ parser.y:213.24-28: warning: POSIX Yacc does not support string literals [-Wyacc] 213 | %token TOK_NEW "new" | ^~~~~ parser.y:214.24-33: warning: POSIX Yacc does not support string literals [-Wyacc] 214 | %token TOK_NOEXCEPT "noexcept" | ^~~~~~~~~~ parser.y:215.24-33: warning: POSIX Yacc does not support string literals [-Wyacc] 215 | %token TOK_OPERATOR "operator" | ^~~~~~~~~~ parser.y:216.24-32: warning: POSIX Yacc does not support string literals [-Wyacc] 216 | %token TOK_PRIVATE "private" | ^~~~~~~~~ parser.y:217.24-34: warning: POSIX Yacc does not support string literals [-Wyacc] 217 | %token TOK_PROTECTED "protected" | ^~~~~~~~~~~ parser.y:218.24-31: warning: POSIX Yacc does not support string literals [-Wyacc] 218 | %token TOK_PUBLIC "public" | ^~~~~~~~ parser.y:219.24-33: warning: POSIX Yacc does not support string literals [-Wyacc] 219 | %token TOK_TEMPLATE "template" | ^~~~~~~~~~ parser.y:220.24-29: warning: POSIX Yacc does not support string literals [-Wyacc] 220 | %token TOK_THIS "this" | ^~~~~~ parser.y:221.24-30: warning: POSIX Yacc does not support string literals [-Wyacc] 221 | %token TOK_THROW "throw" | ^~~~~~~ parser.y:222.24-31: warning: POSIX Yacc does not support string literals [-Wyacc] 222 | %token TOK_TYPEID "typeid" | ^~~~~~~~ parser.y:223.24-33: warning: POSIX Yacc does not support string literals [-Wyacc] 223 | %token TOK_TYPENAME "typename" | ^~~~~~~~~~ parser.y:224.24-28: warning: POSIX Yacc does not support string literals [-Wyacc] 224 | %token TOK_TRY "try" | ^~~~~ parser.y:225.24-30: warning: POSIX Yacc does not support string literals [-Wyacc] 225 | %token TOK_USING "using" | ^~~~~~~ parser.y:226.24-32: warning: POSIX Yacc does not support string literals [-Wyacc] 226 | %token TOK_VIRTUAL "virtual" | ^~~~~~~~~ parser.y:227.24-27: warning: POSIX Yacc does not support string literals [-Wyacc] 227 | %token TOK_SCOPE "::" | ^~~~ parser.y:228.24-27: warning: POSIX Yacc does not support string literals [-Wyacc] 228 | %token TOK_DOTPM ".*" | ^~~~ parser.y:229.24-28: warning: POSIX Yacc does not support string literals [-Wyacc] 229 | %token TOK_ARROWPM "->*" | ^~~~~ parser.y:232.24-33: warning: POSIX Yacc does not support string literals [-Wyacc] 232 | %token TOK_MSC_UUIDOF "__uuidof" | ^~~~~~~~~~ parser.y:233.26-38: warning: POSIX Yacc does not support string literals [-Wyacc] 233 | %token TOK_MSC_IF_EXISTS "__if_exists" | ^~~~~~~~~~~~~ parser.y:234.30-46: warning: POSIX Yacc does not support string literals [-Wyacc] 234 | %token TOK_MSC_IF_NOT_EXISTS "__if_not_exists" | ^~~~~~~~~~~~~~~~~ parser.y:235.28-46: warning: POSIX Yacc does not support string literals [-Wyacc] 235 | %token TOK_UNDERLYING_TYPE "__underlying_type" | ^~~~~~~~~~~~~~~~~~~ parser.y:241.1-7: warning: POSIX Yacc does not support %expect [-Wyacc] 241 | %expect 1 /* the famous "dangling `else'" ambiguity */ | ^~~~~~~ c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o ansi_c_y.tab.o ansi_c_y.tab.cpp flex -Pyyansi_c -oansi_c_lex.yy.cpp scanner.l c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o ansi_c_lex.yy.o ansi_c_lex.yy.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o ansi_c_parser.o ansi_c_parser.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o expr2c.o expr2c.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o ansi_c_language.o ansi_c_language.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o c_sizeof.o c_sizeof.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o ansi_c_scope.o ansi_c_scope.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o c_types.o c_types.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o ansi_c_typecheck.o ansi_c_typecheck.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o c_preprocess.o c_preprocess.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o c_storage_spec.o c_storage_spec.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o c_typecheck_base.o c_typecheck_base.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o c_typecheck_initializer.o c_typecheck_initializer.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o c_typecheck_typecast.o c_typecheck_typecast.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o c_typecheck_code.o c_typecheck_code.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o c_typecheck_expr.o c_typecheck_expr.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o c_typecheck_type.o c_typecheck_type.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o string_constant.o string_constant.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o c_qualifiers.o c_qualifiers.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o c_typecheck_argc_argv.o c_typecheck_argc_argv.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o ansi_c_parse_tree.o ansi_c_parse_tree.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o preprocessor_line.o preprocessor_line.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o ansi_c_convert_type.o ansi_c_convert_type.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o type2name.o type2name.cpp c++ -o library/converter library/converter.cpp cat library/*.c | library/converter > cprover_library.inc c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cprover_library.o cprover_library.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o anonymous_member.o anonymous_member.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o printf_formatter.o printf_formatter.cpp c++ -o file_converter file_converter.cpp ./file_converter < gcc_builtin_headers_generic.h > gcc_builtin_headers_generic.inc ./file_converter < gcc_builtin_headers_ia32.h > gcc_builtin_headers_ia32.inc ./file_converter < gcc_builtin_headers_ia32-2.h > gcc_builtin_headers_ia32-2.inc ./file_converter < gcc_builtin_headers_alpha.h > gcc_builtin_headers_alpha.inc ./file_converter < gcc_builtin_headers_arm.h > gcc_builtin_headers_arm.inc ./file_converter < gcc_builtin_headers_mips.h > gcc_builtin_headers_mips.inc ./file_converter < gcc_builtin_headers_power.h > gcc_builtin_headers_power.inc ./file_converter < arm_builtin_headers.h > arm_builtin_headers.inc ./file_converter < cw_builtin_headers.h > cw_builtin_headers.inc ./file_converter < clang_builtin_headers.h > clang_builtin_headers.inc c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o ansi_c_internal_additions.o ansi_c_internal_additions.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o padding.o padding.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o ansi_c_declaration.o ansi_c_declaration.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o designator.o designator.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o ansi_c_entry_point.o ansi_c_entry_point.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o literals/parse_float.o literals/parse_float.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o literals/unescape_string.o literals/unescape_string.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o literals/convert_float_literal.o literals/convert_float_literal.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o literals/convert_character_literal.o literals/convert_character_literal.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o literals/convert_integer_literal.o literals/convert_integer_literal.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o literals/convert_string_literal.o literals/convert_string_literal.cpp ar rc ansi-c.a c_typecast.o ansi_c_y.tab.o ansi_c_lex.yy.o ansi_c_parser.o expr2c.o ansi_c_language.o c_sizeof.o ansi_c_scope.o c_types.o ansi_c_typecheck.o c_preprocess.o c_storage_spec.o c_typecheck_base.o c_typecheck_initializer.o c_typecheck_typecast.o c_typecheck_code.o c_typecheck_expr.o c_typecheck_type.o string_constant.o c_qualifiers.o c_typecheck_argc_argv.o ansi_c_parse_tree.o preprocessor_line.o ansi_c_convert_type.o type2name.o cprover_library.o anonymous_member.o printf_formatter.o ansi_c_internal_additions.o padding.o ansi_c_declaration.o designator.o ansi_c_entry_point.o literals/parse_float.o literals/unescape_string.o literals/convert_float_literal.o literals/convert_character_literal.o literals/convert_integer_literal.o literals/convert_string_literal.o gmake[1]: Leaving directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/ansi-c' ## Entering linking gmake -C linking gmake[1]: Entering directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/linking' c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o linking.o linking.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o zero_initializer.o zero_initializer.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o static_lifetime_init.o static_lifetime_init.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o remove_internal_symbols.o remove_internal_symbols.cpp ar rc linking.a linking.o zero_initializer.o static_lifetime_init.o remove_internal_symbols.o gmake[1]: Leaving directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/linking' ## Entering cpp gmake -C cpp gmake[1]: Entering directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/cpp' c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_id.o cpp_id.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_language.o cpp_language.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o expr2cpp.o expr2cpp.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_parser.o cpp_parser.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_typecheck.o cpp_typecheck.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_convert_type.o cpp_convert_type.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_typecheck_expr.o cpp_typecheck_expr.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_typecheck_code.o cpp_typecheck_code.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_typecheck_type.o cpp_typecheck_type.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o parse.o parse.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_parse_tree.o cpp_parse_tree.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_token_buffer.o cpp_token_buffer.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_typecheck_fargs.o cpp_typecheck_fargs.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_typecheck_resolve.o cpp_typecheck_resolve.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_util.o cpp_util.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_enum_type.o cpp_enum_type.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_typecheck_function.o cpp_typecheck_function.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_typecheck_namespace.o cpp_typecheck_namespace.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_name.o cpp_name.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_is_pod.o cpp_is_pod.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_scope.o cpp_scope.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o template_map.o template_map.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_scopes.o cpp_scopes.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_declarator.o cpp_declarator.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_instantiate_template.o cpp_instantiate_template.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_internal_additions.o cpp_internal_additions.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_type2name.o cpp_type2name.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_typecheck_linkage_spec.o cpp_typecheck_linkage_spec.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_typecheck_template.o cpp_typecheck_template.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_typecheck_function_bodies.o cpp_typecheck_function_bodies.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_typecheck_initializer.o cpp_typecheck_initializer.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_typecheck_compound_type.o cpp_typecheck_compound_type.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_constructor.o cpp_constructor.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_destructor.o cpp_destructor.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_typecheck_conversions.o cpp_typecheck_conversions.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_typecheck_declaration.o cpp_typecheck_declaration.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_declarator_converter.o cpp_declarator_converter.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_declaration.o cpp_declaration.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_namespace_spec.o cpp_namespace_spec.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_typecheck_using.o cpp_typecheck_using.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_exception_id.o cpp_exception_id.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_typecheck_enum_type.o cpp_typecheck_enum_type.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_typecheck_bases.o cpp_typecheck_bases.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_typecheck_constructor.o cpp_typecheck_constructor.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_typecheck_destructor.o cpp_typecheck_destructor.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_typecheck_virtual_table.o cpp_typecheck_virtual_table.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o cpp_typecheck_static_assert.o cpp_typecheck_static_assert.cpp ar rc cpp.a cpp_id.o cpp_language.o expr2cpp.o cpp_parser.o cpp_typecheck.o cpp_convert_type.o cpp_typecheck_expr.o cpp_typecheck_code.o cpp_typecheck_type.o parse.o cpp_parse_tree.o cpp_token_buffer.o cpp_typecheck_fargs.o cpp_typecheck_resolve.o cpp_util.o cpp_enum_type.o cpp_typecheck_function.o cpp_typecheck_namespace.o cpp_name.o cpp_is_pod.o cpp_scope.o template_map.o cpp_scopes.o cpp_declarator.o cpp_instantiate_template.o cpp_internal_additions.o cpp_type2name.o cpp_typecheck_linkage_spec.o cpp_typecheck_template.o cpp_typecheck_function_bodies.o cpp_typecheck_initializer.o cpp_typecheck_compound_type.o cpp_constructor.o cpp_destructor.o cpp_typecheck_conversions.o cpp_typecheck_declaration.o cpp_declarator_converter.o cpp_declaration.o cpp_namespace_spec.o cpp_typecheck_using.o cpp_exception_id.o cpp_typecheck_enum_type.o cpp_typecheck_bases.o cpp_typecheck_constructor.o cpp_typecheck_destructor.o cpp_typecheck_virtual_table.o cpp_typecheck_static_assert.o gmake[1]: Leaving directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/cpp' ## Entering xmllang gmake -C xmllang gmake[1]: Entering directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/xmllang' c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o xml_parser.o xml_parser.cpp bison -y -v $flags -pyyxml --defines=xml_y.tab.h parser.y -o xml_y.tab.cpp parser.y:17.1-14: warning: POSIX Yacc does not support %error-verbose [-Wyacc] 17 | %error-verbose | ^~~~~~~~~~~~~~ parser.y:17.1-14: warning: deprecated directive: '%error-verbose', use '%define parse.error verbose' [-Wdeprecated] 17 | %error-verbose | ^~~~~~~~~~~~~~ | %define parse.error verbose parser.y: warning: fix-its can be applied. Rerun with option '--update'. [-Wother] c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o xml_y.tab.o xml_y.tab.cpp flex -Pyyxml -oxml_lex.yy.cpp scanner.l c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o xml_lex.yy.o xml_lex.yy.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o xml_parse_tree.o xml_parse_tree.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o graphml.o graphml.cpp ar rc xmllang.a xml_parser.o xml_y.tab.o xml_lex.yy.o xml_parse_tree.o graphml.o gmake[1]: Leaving directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/xmllang' ## Entering assembler gmake -C assembler gmake[1]: Entering directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/assembler' flex -Pyyassembler -oassembler_lex.yy.cpp scanner.l c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o assembler_lex.yy.o assembler_lex.yy.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o assembler_parser.o assembler_parser.cpp ar rc assembler.a assembler_lex.yy.o assembler_parser.o gmake[1]: Leaving directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/assembler' ## Entering java_bytecode gmake -C java_bytecode gmake[1]: Entering directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/java_bytecode' c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o java_bytecode_language.o java_bytecode_language.cpp In file included from java_bytecode_language.cpp:9: In file included from ../util/symbol_table.h:22: In file included from /usr/include/c++/v1/map:541: In file included from /usr/include/c++/v1/__memory/allocator.h:14: In file included from /usr/include/c++/v1/__memory/allocate_at_least.h:13: /usr/include/c++/v1/__memory/allocator_traits.h:325:9: warning: destructor called on non-final 'java_bytecode_parse_treet::fieldt' that has virtual functions but non-virtual destructor [-Wdelete-non-abstract-non-virtual-dtor] __p->~_Tp(); ^ /usr/include/c++/v1/list:739:34: note: in instantiation of function template specialization 'std::allocator_traits>>::destroy' requested here __node_alloc_traits::destroy(__na, _VSTD::addressof(__np->__value_)); ^ /usr/include/c++/v1/list:720:3: note: in instantiation of member function 'std::__list_imp>::clear' requested here clear(); ^ /usr/include/c++/v1/list:811:28: note: in instantiation of member function 'std::__list_imp>::~__list_imp' requested here class _LIBCPP_TEMPLATE_VIS list ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:15: note: qualify call to silence this warning __p->~_Tp(); ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:9: warning: destructor called on non-final 'java_bytecode_parse_treet::methodt' that has virtual functions but non-virtual destructor [-Wdelete-non-abstract-non-virtual-dtor] __p->~_Tp(); ^ /usr/include/c++/v1/list:739:34: note: in instantiation of function template specialization 'std::allocator_traits>>::destroy' requested here __node_alloc_traits::destroy(__na, _VSTD::addressof(__np->__value_)); ^ /usr/include/c++/v1/list:720:3: note: in instantiation of member function 'std::__list_imp>::clear' requested here clear(); ^ /usr/include/c++/v1/list:811:28: note: in instantiation of member function 'std::__list_imp>::~__list_imp' requested here class _LIBCPP_TEMPLATE_VIS list ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:15: note: qualify call to silence this warning __p->~_Tp(); ^ 2 warnings generated. c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o java_bytecode_parse_tree.o java_bytecode_parse_tree.cpp In file included from java_bytecode_parse_tree.cpp:9: In file included from /usr/include/c++/v1/ostream:168: In file included from /usr/include/c++/v1/__memory/shared_ptr.h:22: In file included from /usr/include/c++/v1/__memory/allocation_guard.h:14: /usr/include/c++/v1/__memory/allocator_traits.h:325:9: warning: destructor called on non-final 'java_bytecode_parse_treet::fieldt' that has virtual functions but non-virtual destructor [-Wdelete-non-abstract-non-virtual-dtor] __p->~_Tp(); ^ /usr/include/c++/v1/list:739:34: note: in instantiation of function template specialization 'std::allocator_traits>>::destroy' requested here __node_alloc_traits::destroy(__na, _VSTD::addressof(__np->__value_)); ^ /usr/include/c++/v1/list:720:3: note: in instantiation of member function 'std::__list_imp>::clear' requested here clear(); ^ /usr/include/c++/v1/list:811:28: note: in instantiation of member function 'std::__list_imp>::~__list_imp' requested here class _LIBCPP_TEMPLATE_VIS list ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:15: note: qualify call to silence this warning __p->~_Tp(); ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:9: warning: destructor called on non-final 'java_bytecode_parse_treet::methodt' that has virtual functions but non-virtual destructor [-Wdelete-non-abstract-non-virtual-dtor] __p->~_Tp(); ^ /usr/include/c++/v1/list:739:34: note: in instantiation of function template specialization 'std::allocator_traits>>::destroy' requested here __node_alloc_traits::destroy(__na, _VSTD::addressof(__np->__value_)); ^ /usr/include/c++/v1/list:720:3: note: in instantiation of member function 'std::__list_imp>::clear' requested here clear(); ^ /usr/include/c++/v1/list:811:28: note: in instantiation of member function 'std::__list_imp>::~__list_imp' requested here class _LIBCPP_TEMPLATE_VIS list ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:15: note: qualify call to silence this warning __p->~_Tp(); ^ 2 warnings generated. c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o java_bytecode_typecheck.o java_bytecode_typecheck.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o expr2java.o expr2java.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o java_bytecode_convert_class.o java_bytecode_convert_class.cpp In file included from java_bytecode_convert_class.cpp:12: In file included from /usr/include/c++/v1/iostream:43: In file included from /usr/include/c++/v1/ios:221: In file included from /usr/include/c++/v1/__locale:18: In file included from /usr/include/c++/v1/mutex:191: In file included from /usr/include/c++/v1/__memory/shared_ptr.h:22: In file included from /usr/include/c++/v1/__memory/allocation_guard.h:14: /usr/include/c++/v1/__memory/allocator_traits.h:325:9: warning: destructor called on non-final 'java_bytecode_parse_treet::fieldt' that has virtual functions but non-virtual destructor [-Wdelete-non-abstract-non-virtual-dtor] __p->~_Tp(); ^ /usr/include/c++/v1/list:739:34: note: in instantiation of function template specialization 'std::allocator_traits>>::destroy' requested here __node_alloc_traits::destroy(__na, _VSTD::addressof(__np->__value_)); ^ /usr/include/c++/v1/list:720:3: note: in instantiation of member function 'std::__list_imp>::clear' requested here clear(); ^ /usr/include/c++/v1/list:811:28: note: in instantiation of member function 'std::__list_imp>::~__list_imp' requested here class _LIBCPP_TEMPLATE_VIS list ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:15: note: qualify call to silence this warning __p->~_Tp(); ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:9: warning: destructor called on non-final 'java_bytecode_parse_treet::methodt' that has virtual functions but non-virtual destructor [-Wdelete-non-abstract-non-virtual-dtor] __p->~_Tp(); ^ /usr/include/c++/v1/list:739:34: note: in instantiation of function template specialization 'std::allocator_traits>>::destroy' requested here __node_alloc_traits::destroy(__na, _VSTD::addressof(__np->__value_)); ^ /usr/include/c++/v1/list:720:3: note: in instantiation of member function 'std::__list_imp>::clear' requested here clear(); ^ /usr/include/c++/v1/list:811:28: note: in instantiation of member function 'std::__list_imp>::~__list_imp' requested here class _LIBCPP_TEMPLATE_VIS list ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:15: note: qualify call to silence this warning __p->~_Tp(); ^ 2 warnings generated. c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o java_types.o java_types.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o java_entry_point.o java_entry_point.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o java_bytecode_typecheck_code.o java_bytecode_typecheck_code.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o java_bytecode_typecheck_expr.o java_bytecode_typecheck_expr.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o java_bytecode_typecheck_type.o java_bytecode_typecheck_type.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o java_bytecode_internal_additions.o java_bytecode_internal_additions.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o java_class_identifier.o java_class_identifier.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o java_bytecode_parser.o java_bytecode_parser.cpp In file included from java_bytecode_parser.cpp:9: In file included from /usr/include/c++/v1/fstream:186: In file included from /usr/include/c++/v1/__locale:18: In file included from /usr/include/c++/v1/mutex:191: In file included from /usr/include/c++/v1/__memory/shared_ptr.h:22: In file included from /usr/include/c++/v1/__memory/allocation_guard.h:14: /usr/include/c++/v1/__memory/allocator_traits.h:325:9: warning: destructor called on non-final 'java_bytecode_parse_treet::fieldt' that has virtual functions but non-virtual destructor [-Wdelete-non-abstract-non-virtual-dtor] __p->~_Tp(); ^ /usr/include/c++/v1/list:739:34: note: in instantiation of function template specialization 'std::allocator_traits>>::destroy' requested here __node_alloc_traits::destroy(__na, _VSTD::addressof(__np->__value_)); ^ /usr/include/c++/v1/list:720:3: note: in instantiation of member function 'std::__list_imp>::clear' requested here clear(); ^ /usr/include/c++/v1/list:811:28: note: in instantiation of member function 'std::__list_imp>::~__list_imp' requested here class _LIBCPP_TEMPLATE_VIS list ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:15: note: qualify call to silence this warning __p->~_Tp(); ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:9: warning: destructor called on non-final 'java_bytecode_parse_treet::methodt' that has virtual functions but non-virtual destructor [-Wdelete-non-abstract-non-virtual-dtor] __p->~_Tp(); ^ /usr/include/c++/v1/list:739:34: note: in instantiation of function template specialization 'std::allocator_traits>>::destroy' requested here __node_alloc_traits::destroy(__na, _VSTD::addressof(__np->__value_)); ^ /usr/include/c++/v1/list:720:3: note: in instantiation of member function 'std::__list_imp>::clear' requested here clear(); ^ /usr/include/c++/v1/list:811:28: note: in instantiation of member function 'std::__list_imp>::~__list_imp' requested here class _LIBCPP_TEMPLATE_VIS list ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:15: note: qualify call to silence this warning __p->~_Tp(); ^ 2 warnings generated. c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o bytecode_info.o bytecode_info.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o java_class_loader.o java_class_loader.cpp In file included from java_class_loader.cpp:9: In file included from /usr/include/c++/v1/stack:106: In file included from /usr/include/c++/v1/deque:180: In file included from /usr/include/c++/v1/__memory/allocator_destructor.h:13: /usr/include/c++/v1/__memory/allocator_traits.h:325:9: warning: destructor called on non-final 'java_bytecode_parse_treet::fieldt' that has virtual functions but non-virtual destructor [-Wdelete-non-abstract-non-virtual-dtor] __p->~_Tp(); ^ /usr/include/c++/v1/list:739:34: note: in instantiation of function template specialization 'std::allocator_traits>>::destroy' requested here __node_alloc_traits::destroy(__na, _VSTD::addressof(__np->__value_)); ^ /usr/include/c++/v1/list:720:3: note: in instantiation of member function 'std::__list_imp>::clear' requested here clear(); ^ /usr/include/c++/v1/list:811:28: note: in instantiation of member function 'std::__list_imp>::~__list_imp' requested here class _LIBCPP_TEMPLATE_VIS list ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:15: note: qualify call to silence this warning __p->~_Tp(); ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:9: warning: destructor called on non-final 'java_bytecode_parse_treet::methodt' that has virtual functions but non-virtual destructor [-Wdelete-non-abstract-non-virtual-dtor] __p->~_Tp(); ^ /usr/include/c++/v1/list:739:34: note: in instantiation of function template specialization 'std::allocator_traits>>::destroy' requested here __node_alloc_traits::destroy(__na, _VSTD::addressof(__np->__value_)); ^ /usr/include/c++/v1/list:720:3: note: in instantiation of member function 'std::__list_imp>::clear' requested here clear(); ^ /usr/include/c++/v1/list:811:28: note: in instantiation of member function 'std::__list_imp>::~__list_imp' requested here class _LIBCPP_TEMPLATE_VIS list ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:15: note: qualify call to silence this warning __p->~_Tp(); ^ 2 warnings generated. c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o jar_file.o jar_file.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o java_object_factory.o java_object_factory.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o java_bytecode_convert_method.o java_bytecode_convert_method.cpp In file included from java_bytecode_convert_method.cpp:12: In file included from /usr/include/c++/v1/iostream:43: In file included from /usr/include/c++/v1/ios:221: In file included from /usr/include/c++/v1/__locale:18: In file included from /usr/include/c++/v1/mutex:191: In file included from /usr/include/c++/v1/__memory/shared_ptr.h:22: In file included from /usr/include/c++/v1/__memory/allocation_guard.h:14: /usr/include/c++/v1/__memory/allocator_traits.h:325:9: warning: destructor called on non-final 'java_bytecode_parse_treet::fieldt' that has virtual functions but non-virtual destructor [-Wdelete-non-abstract-non-virtual-dtor] __p->~_Tp(); ^ /usr/include/c++/v1/list:739:34: note: in instantiation of function template specialization 'std::allocator_traits>>::destroy' requested here __node_alloc_traits::destroy(__na, _VSTD::addressof(__np->__value_)); ^ /usr/include/c++/v1/list:720:3: note: in instantiation of member function 'std::__list_imp>::clear' requested here clear(); ^ /usr/include/c++/v1/list:811:28: note: in instantiation of member function 'std::__list_imp>::~__list_imp' requested here class _LIBCPP_TEMPLATE_VIS list ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:15: note: qualify call to silence this warning __p->~_Tp(); ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:9: warning: destructor called on non-final 'java_bytecode_parse_treet::methodt' that has virtual functions but non-virtual destructor [-Wdelete-non-abstract-non-virtual-dtor] __p->~_Tp(); ^ /usr/include/c++/v1/list:739:34: note: in instantiation of function template specialization 'std::allocator_traits>>::destroy' requested here __node_alloc_traits::destroy(__na, _VSTD::addressof(__np->__value_)); ^ /usr/include/c++/v1/list:720:3: note: in instantiation of member function 'std::__list_imp>::clear' requested here clear(); ^ /usr/include/c++/v1/list:811:28: note: in instantiation of member function 'std::__list_imp>::~__list_imp' requested here class _LIBCPP_TEMPLATE_VIS list ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:15: note: qualify call to silence this warning __p->~_Tp(); ^ 2 warnings generated. ar rc java_bytecode.a java_bytecode_language.o java_bytecode_parse_tree.o java_bytecode_typecheck.o expr2java.o java_bytecode_convert_class.o java_types.o java_entry_point.o java_bytecode_typecheck_code.o java_bytecode_typecheck_expr.o java_bytecode_typecheck_type.o java_bytecode_internal_additions.o java_class_identifier.o java_bytecode_parser.o bytecode_info.o java_class_loader.o jar_file.o java_object_factory.o java_bytecode_convert_method.o gmake[1]: Leaving directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/java_bytecode' ## Entering jsil gmake -C jsil gmake[1]: Entering directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/jsil' bison -y -v $flags -pyyjsil --defines=jsil_y.tab.h parser.y -o jsil_y.tab.cpp parser.y:26.20-30: warning: POSIX Yacc does not support string literals [-Wyacc] 26 | %token TOK_NEWLINE "" | ^~~~~~~~~~~ parser.y:30.22-32: warning: POSIX Yacc does not support string literals [-Wyacc] 30 | %token TOK_PROCEDURE "procedure" | ^~~~~~~~~~~ parser.y:31.20-28: warning: POSIX Yacc does not support string literals [-Wyacc] 31 | %token TOK_RETURNS "returns" | ^~~~~~~~~ parser.y:32.15-18: warning: POSIX Yacc does not support string literals [-Wyacc] 32 | %token TOK_TO "to" | ^~~~ parser.y:33.19-26: warning: POSIX Yacc does not support string literals [-Wyacc] 33 | %token TOK_THROWS "throws" | ^~~~~~~~ parser.y:34.17-22: warning: POSIX Yacc does not support string literals [-Wyacc] 34 | %token TOK_EVAL "eval" | ^~~~~~ parser.y:35.18-24: warning: POSIX Yacc does not support string literals [-Wyacc] 35 | %token TOK_LABEL "label" | ^~~~~~~ parser.y:36.17-22: warning: POSIX Yacc does not support string literals [-Wyacc] 36 | %token TOK_GOTO "goto" | ^~~~~~ parser.y:37.17-22: warning: POSIX Yacc does not support string literals [-Wyacc] 37 | %token TOK_SKIP "skip" | ^~~~~~ parser.y:38.17-22: warning: POSIX Yacc does not support string literals [-Wyacc] 38 | %token TOK_WITH "with" | ^~~~~~ parser.y:39.16-20: warning: POSIX Yacc does not support string literals [-Wyacc] 39 | %token TOK_NEW "new" | ^~~~~ parser.y:40.22-31: warning: POSIX Yacc does not support string literals [-Wyacc] 40 | %token TOK_HAS_FIELD "hasField" | ^~~~~~~~~~ parser.y:41.19-26: warning: POSIX Yacc does not support string literals [-Wyacc] 41 | %token TOK_DELETE "delete" | ^~~~~~~~ parser.y:42.24-35: warning: POSIX Yacc does not support string literals [-Wyacc] 42 | %token TOK_PROTO_FIELD "protoField" | ^~~~~~~~~~~~ parser.y:43.22-31: warning: POSIX Yacc does not support string literals [-Wyacc] 43 | %token TOK_PROTO_OBJ "protoObj" | ^~~~~~~~~~ parser.y:44.16-20: warning: POSIX Yacc does not support string literals [-Wyacc] 44 | %token TOK_REF "ref" | ^~~~~ parser.y:45.18-24: warning: POSIX Yacc does not support string literals [-Wyacc] 45 | %token TOK_FIELD "field" | ^~~~~~~ parser.y:46.17-22: warning: POSIX Yacc does not support string literals [-Wyacc] 46 | %token TOK_BASE "base" | ^~~~~~ parser.y:47.19-26: warning: POSIX Yacc does not support string literals [-Wyacc] 47 | %token TOK_TYPEOF "typeOf" | ^~~~~~~~ parser.y:48.17-22: warning: POSIX Yacc does not support string literals [-Wyacc] 48 | %token TOK_NULL "null" | ^~~~~~ parser.y:49.22-33: warning: POSIX Yacc does not support string literals [-Wyacc] 49 | %token TOK_UNDEFINED "#undefined" | ^~~~~~~~~~~~ parser.y:50.18-25: warning: POSIX Yacc does not support string literals [-Wyacc] 50 | %token TOK_EMPTY "#empty" | ^~~~~~~~ parser.y:51.17-22: warning: POSIX Yacc does not support string literals [-Wyacc] 51 | %token TOK_TRUE "true" | ^~~~~~ parser.y:52.18-24: warning: POSIX Yacc does not support string literals [-Wyacc] 52 | %token TOK_FALSE "false" | ^~~~~~~ parser.y:53.18-25: warning: POSIX Yacc does not support string literals [-Wyacc] 53 | %token TOK_PROTO "#proto" | ^~~~~~~~ parser.y:54.16-21: warning: POSIX Yacc does not support string literals [-Wyacc] 54 | %token TOK_FID "#fid" | ^~~~~~ parser.y:55.18-25: warning: POSIX Yacc does not support string literals [-Wyacc] 55 | %token TOK_SCOPE "#scope" | ^~~~~~~~ parser.y:56.24-37: warning: POSIX Yacc does not support string literals [-Wyacc] 56 | %token TOK_CONSTRUCTID "#constructid" | ^~~~~~~~~~~~~~ parser.y:57.22-33: warning: POSIX Yacc does not support string literals [-Wyacc] 57 | %token TOK_PRIMVALUE "#primvalue" | ^~~~~~~~~~~~ parser.y:58.27-43: warning: POSIX Yacc does not support string literals [-Wyacc] 58 | %token TOK_TARGETFUNCTION "#targetfunction" | ^~~~~~~~~~~~~~~~~ parser.y:59.18-25: warning: POSIX Yacc does not support string literals [-Wyacc] 59 | %token TOK_CLASS "#class" | ^~~~~~~~ parser.y:60.26-40: warning: POSIX Yacc does not support string literals [-Wyacc] 60 | %token TOK_NUM_TO_STRING "num_to_string" | ^~~~~~~~~~~~~~~ parser.y:61.26-40: warning: POSIX Yacc does not support string literals [-Wyacc] 61 | %token TOK_STRING_TO_NUM "string_to_num" | ^~~~~~~~~~~~~~~ parser.y:62.25-38: warning: POSIX Yacc does not support string literals [-Wyacc] 62 | %token TOK_NUM_TO_INT32 "num_to_int32" | ^~~~~~~~~~~~~~ parser.y:63.26-40: warning: POSIX Yacc does not support string literals [-Wyacc] 63 | %token TOK_NUM_TO_UINT32 "num_to_uint32" | ^~~~~~~~~~~~~~~ parser.y:64.29-46: warning: POSIX Yacc does not support string literals [-Wyacc] 64 | %token TOK_MEMBER_REFERENCE "#MemberReference" | ^~~~~~~~~~~~~~~~~~ parser.y:65.31-50: warning: POSIX Yacc does not support string literals [-Wyacc] 65 | %token TOK_VARIABLE_REFERENCE "#VariableReference" | ^~~~~~~~~~~~~~~~~~~~ parser.y:69.19-25: warning: POSIX Yacc does not support string literals [-Wyacc] 69 | %token TOK_T_NULL "#Null" | ^~~~~~~ parser.y:70.24-35: warning: POSIX Yacc does not support string literals [-Wyacc] 70 | %token TOK_T_UNDEFINED "#Undefined" | ^~~~~~~~~~~~ parser.y:71.22-31: warning: POSIX Yacc does not support string literals [-Wyacc] 71 | %token TOK_T_BOOLEAN "#Boolean" | ^~~~~~~~~~ parser.y:72.21-29: warning: POSIX Yacc does not support string literals [-Wyacc] 72 | %token TOK_T_STRING "#String" | ^~~~~~~~~ parser.y:73.21-29: warning: POSIX Yacc does not support string literals [-Wyacc] 73 | %token TOK_T_NUMBER "#Number" | ^~~~~~~~~ parser.y:74.29-44: warning: POSIX Yacc does not support string literals [-Wyacc] 74 | %token TOK_T_BUILTIN_OBJECT "#BuiltinObject" | ^~~~~~~~~~~~~~~~ parser.y:75.26-38: warning: POSIX Yacc does not support string literals [-Wyacc] 75 | %token TOK_T_USER_OBJECT "#UserObject" | ^~~~~~~~~~~~~ parser.y:76.21-29: warning: POSIX Yacc does not support string literals [-Wyacc] 76 | %token TOK_T_OBJECT "#Object" | ^~~~~~~~~ parser.y:77.24-35: warning: POSIX Yacc does not support string literals [-Wyacc] 77 | %token TOK_T_REFERENCE "#Reference" | ^~~~~~~~~~~~ parser.y:81.18-21: warning: POSIX Yacc does not support string literals [-Wyacc] 81 | %token TOK_DEFEQ ":=" | ^~~~ parser.y:82.16-19: warning: POSIX Yacc does not support string literals [-Wyacc] 82 | %token TOK_LEQ "<=" | ^~~~ parser.y:83.16-20: warning: POSIX Yacc does not support string literals [-Wyacc] 83 | %token TOK_AND "and" | ^~~~~ parser.y:84.15-18: warning: POSIX Yacc does not support string literals [-Wyacc] 84 | %token TOK_OR "or" | ^~~~ parser.y:85.23-26: warning: POSIX Yacc does not support string literals [-Wyacc] 85 | %token TOK_SUBTYPE_OF "<:" | ^~~~ parser.y:86.23-26: warning: POSIX Yacc does not support string literals [-Wyacc] 86 | %token TOK_LEFT_SHIFT "<<" | ^~~~ parser.y:87.31-34: warning: POSIX Yacc does not support string literals [-Wyacc] 87 | %token TOK_SIGNED_RIGHT_SHIFT ">>" | ^~~~ parser.y:88.33-37: warning: POSIX Yacc does not support string literals [-Wyacc] 88 | %token TOK_UNSIGNED_RIGHT_SHIFT ">>>" | ^~~~~ parser.y:89.16-20: warning: POSIX Yacc does not support string literals [-Wyacc] 89 | %token TOK_NOT "not" | ^~~~~ parser.y:104.1-14: warning: POSIX Yacc does not support %error-verbose [-Wyacc] 104 | %error-verbose | ^~~~~~~~~~~~~~ parser.y:104.1-14: warning: deprecated directive: '%error-verbose', use '%define parse.error verbose' [-Wdeprecated] 104 | %error-verbose | ^~~~~~~~~~~~~~ | %define parse.error verbose parser.y:105.1-7: warning: POSIX Yacc does not support %expect [-Wyacc] 105 | %expect 0 | ^~~~~~~ parser.y: warning: fix-its can be applied. Rerun with option '--update'. [-Wother] c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o jsil_y.tab.o jsil_y.tab.cpp flex -Pyyjsil -ojsil_lex.yy.cpp scanner.l c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o jsil_lex.yy.o jsil_lex.yy.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o jsil_convert.o jsil_convert.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o jsil_language.o jsil_language.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o jsil_parse_tree.o jsil_parse_tree.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o jsil_types.o jsil_types.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o jsil_parser.o jsil_parser.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o jsil_typecheck.o jsil_typecheck.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o expr2jsil.o expr2jsil.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o jsil_entry_point.o jsil_entry_point.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o jsil_internal_additions.o jsil_internal_additions.cpp ar rc jsil.a jsil_y.tab.o jsil_lex.yy.o jsil_convert.o jsil_language.o jsil_parse_tree.o jsil_types.o jsil_parser.o jsil_typecheck.o expr2jsil.o jsil_entry_point.o jsil_internal_additions.o gmake[1]: Leaving directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/jsil' ## Entering solvers gmake -C solvers gmake[1]: Entering directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/solvers' c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o sat/satcheck_minisat2.o sat/satcheck_minisat2.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o sat/cnf.o sat/cnf.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o sat/dimacs_cnf.o sat/dimacs_cnf.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o sat/cnf_clause_list.o sat/cnf_clause_list.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o sat/pbs_dimacs_cnf.o sat/pbs_dimacs_cnf.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o sat/read_dimacs_cnf.o sat/read_dimacs_cnf.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o sat/resolution_proof.o sat/resolution_proof.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o sat/satcheck.o sat/satcheck.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o qbf/qdimacs_cnf.o qbf/qdimacs_cnf.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o qbf/qbf_quantor.o qbf/qbf_quantor.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o qbf/qbf_skizzo.o qbf/qbf_skizzo.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o qbf/qdimacs_core.o qbf/qdimacs_core.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o qbf/qbf_qube.o qbf/qbf_qube.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o qbf/qbf_qube_core.o qbf/qbf_qube_core.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o prop/prop.o prop/prop.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o prop/prop_conv.o prop/prop_conv.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o prop/prop_conv_store.o prop/prop_conv_store.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o prop/cover_goals.o prop/cover_goals.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o prop/literal.o prop/literal.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o prop/aig.o prop/aig.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o prop/aig_prop.o prop/aig_prop.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o prop/minimize.o prop/minimize.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o prop/prop_assignment.o prop/prop_assignment.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o prop/bdd_expr.o prop/bdd_expr.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o cvc/cvc_conv.o cvc/cvc_conv.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o cvc/cvc_dec.o cvc/cvc_dec.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o smt1/smt1_dec.o smt1/smt1_dec.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o smt1/smt1_conv.o smt1/smt1_conv.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o smt2/smt2_dec.o smt2/smt2_dec.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o smt2/smt2_conv.o smt2/smt2_conv.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o smt2/smt2_parser.o smt2/smt2_parser.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o smt2/smt2irep.o smt2/smt2irep.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/equality.o flattening/equality.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/arrays.o flattening/arrays.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/functions.o flattening/functions.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/bv_minimize.o flattening/bv_minimize.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_width.o flattening/boolbv_width.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv.o flattening/boolbv.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_constraint_select_one.o flattening/boolbv_constraint_select_one.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/bv_pointers.o flattening/bv_pointers.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/bv_utils.o flattening/bv_utils.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_abs.o flattening/boolbv_abs.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_with.o flattening/boolbv_with.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_typecast.o flattening/boolbv_typecast.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_index.o flattening/boolbv_index.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_member.o flattening/boolbv_member.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_if.o flattening/boolbv_if.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_byte_extract.o flattening/boolbv_byte_extract.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_add_sub.o flattening/boolbv_add_sub.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_mult.o flattening/boolbv_mult.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_constant.o flattening/boolbv_constant.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_extractbit.o flattening/boolbv_extractbit.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_bv_rel.o flattening/boolbv_bv_rel.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_shift.o flattening/boolbv_shift.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_case.o flattening/boolbv_case.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_cond.o flattening/boolbv_cond.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_concatenation.o flattening/boolbv_concatenation.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_div.o flattening/boolbv_div.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_mod.o flattening/boolbv_mod.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_extractbits.o flattening/boolbv_extractbits.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_replication.o flattening/boolbv_replication.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_reduction.o flattening/boolbv_reduction.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_overflow.o flattening/boolbv_overflow.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_get.o flattening/boolbv_get.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_bitwise.o flattening/boolbv_bitwise.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_equality.o flattening/boolbv_equality.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_unary_minus.o flattening/boolbv_unary_minus.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_ieee_float_rel.o flattening/boolbv_ieee_float_rel.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/pointer_logic.o flattening/pointer_logic.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_quantifier.o flattening/boolbv_quantifier.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_struct.o flattening/boolbv_struct.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_byte_update.o flattening/boolbv_byte_update.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_array_of.o flattening/boolbv_array_of.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_map.o flattening/boolbv_map.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_type.o flattening/boolbv_type.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_array.o flattening/boolbv_array.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_vector.o flattening/boolbv_vector.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_complex.o flattening/boolbv_complex.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_floatbv_op.o flattening/boolbv_floatbv_op.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_union.o flattening/boolbv_union.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/flatten_byte_operators.o flattening/flatten_byte_operators.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_update.o flattening/boolbv_update.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/c_bit_field_replacement_type.o flattening/c_bit_field_replacement_type.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_onehot.o flattening/boolbv_onehot.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_not.o flattening/boolbv_not.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o flattening/boolbv_power.o flattening/boolbv_power.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o floatbv/float_utils.o floatbv/float_utils.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o floatbv/float_bv.o floatbv/float_bv.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o refinement/bv_refinement_loop.o refinement/bv_refinement_loop.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o refinement/refine_arithmetic.o refinement/refine_arithmetic.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o refinement/refine_arrays.o refinement/refine_arrays.cpp refinement/refine_arrays.cpp:108:10: warning: comparison of different enumeration types in switch statement ('resultt' and 'decision_proceduret::resultt') [-Wenum-compare-switch] case decision_proceduret::D_UNSATISFIABLE: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ refinement/refine_arrays.cpp:105:10: warning: comparison of different enumeration types in switch statement ('resultt' and 'decision_proceduret::resultt') [-Wenum-compare-switch] case decision_proceduret::D_SATISFIABLE: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2 warnings generated. c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o miniBDD/miniBDD.o miniBDD/miniBDD.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o ../../minisat-2.2.1/minisat/simp/SimpSolver.o ../../minisat-2.2.1/minisat/simp/SimpSolver.cc c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -I ../../minisat-2.2.1 -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -o ../../minisat-2.2.1/minisat/core/Solver.o ../../minisat-2.2.1/minisat/core/Solver.cc ar rc solvers.a sat/satcheck_minisat2.o sat/cnf.o sat/dimacs_cnf.o sat/cnf_clause_list.o sat/pbs_dimacs_cnf.o sat/read_dimacs_cnf.o sat/resolution_proof.o sat/satcheck.o qbf/qdimacs_cnf.o qbf/qbf_quantor.o qbf/qbf_skizzo.o qbf/qdimacs_core.o qbf/qbf_qube.o qbf/qbf_qube_core.o prop/prop.o prop/prop_conv.o prop/prop_conv_store.o prop/cover_goals.o prop/literal.o prop/aig.o prop/aig_prop.o prop/minimize.o prop/prop_assignment.o prop/bdd_expr.o cvc/cvc_conv.o cvc/cvc_dec.o smt1/smt1_dec.o smt1/smt1_conv.o smt2/smt2_dec.o smt2/smt2_conv.o smt2/smt2_parser.o smt2/smt2irep.o flattening/equality.o flattening/arrays.o flattening/functions.o flattening/bv_minimize.o flattening/boolbv_width.o flattening/boolbv.o flattening/boolbv_constraint_select_one.o flattening/bv_pointers.o flattening/bv_utils.o flattening/boolbv_abs.o flattening/boolbv_with.o flattening/boolbv_typecast.o flattening/boolbv_index.o flattening/boolbv_member.o flattening/boolbv_if.o flattening/boolbv_byte_extract.o flattening/boolbv_add_sub.o flattening/boolbv_mult.o flattening/boolbv_constant.o flattening/boolbv_extractbit.o flattening/boolbv_bv_rel.o flattening/boolbv_shift.o flattening/boolbv_case.o flattening/boolbv_cond.o flattening/boolbv_concatenation.o flattening/boolbv_div.o flattening/boolbv_mod.o flattening/boolbv_extractbits.o flattening/boolbv_replication.o flattening/boolbv_reduction.o flattening/boolbv_overflow.o flattening/boolbv_get.o flattening/boolbv_bitwise.o flattening/boolbv_equality.o flattening/boolbv_unary_minus.o flattening/boolbv_ieee_float_rel.o flattening/pointer_logic.o flattening/boolbv_quantifier.o flattening/boolbv_struct.o flattening/boolbv_byte_update.o flattening/boolbv_array_of.o flattening/boolbv_map.o flattening/boolbv_type.o flattening/boolbv_array.o flattening/boolbv_vector.o flattening/boolbv_complex.o flattening/boolbv_floatbv_op.o flattening/boolbv_union.o flattening/flatten_byte_operators.o flattening/boolbv_update.o flattening/c_bit_field_replacement_type.o flattening/boolbv_onehot.o flattening/boolbv_not.o flattening/boolbv_power.o floatbv/float_utils.o floatbv/float_bv.o refinement/bv_refinement_loop.o refinement/refine_arithmetic.o refinement/refine_arrays.o miniBDD/miniBDD.o ../../minisat-2.2.1/minisat/simp/SimpSolver.o ../../minisat-2.2.1/minisat/core/Solver.o gmake[1]: Leaving directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/solvers' ## Entering goto-symex gmake -C goto-symex gmake[1]: Entering directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/goto-symex' c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o symex_target.o symex_target.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o symex_target_equation.o symex_target_equation.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o goto_symex.o goto_symex.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o symex_main.o symex_main.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o build_goto_trace.o build_goto_trace.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o adjust_float_expressions.o adjust_float_expressions.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o symex_function_call.o symex_function_call.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o goto_symex_state.o goto_symex_state.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o symex_dereference.o symex_dereference.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o symex_goto.o symex_goto.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o symex_builtin_functions.o symex_builtin_functions.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o slice.o slice.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o symex_other.o symex_other.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o slice_by_trace.o slice_by_trace.cpp slice_by_trace.cpp:429:10: warning: variable 'conds_seen' set but not used [-Wunused-but-set-variable] size_t conds_seen = 0; ^ slice_by_trace.cpp:431:10: warning: variable 'potential_SSA_steps' set but not used [-Wunused-but-set-variable] size_t potential_SSA_steps = 0; ^ 2 warnings generated. c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o symex_decl.o symex_decl.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o symex_dead.o symex_dead.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o rewrite_union.o rewrite_union.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o precondition.o precondition.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o postcondition.o postcondition.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o symex_clean_expr.o symex_clean_expr.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o symex_dereference_state.o symex_dereference_state.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o auto_objects.o auto_objects.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o symex_catch.o symex_catch.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o symex_start_thread.o symex_start_thread.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o symex_assign.o symex_assign.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o symex_throw.o symex_throw.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o symex_atomic_section.o symex_atomic_section.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o memory_model.o memory_model.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o memory_model_sc.o memory_model_sc.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o partial_order_concurrency.o partial_order_concurrency.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o memory_model_tso.o memory_model_tso.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o memory_model_pso.o memory_model_pso.cpp ar rc goto-symex.a symex_target.o symex_target_equation.o goto_symex.o symex_main.o build_goto_trace.o adjust_float_expressions.o symex_function_call.o goto_symex_state.o symex_dereference.o symex_goto.o symex_builtin_functions.o slice.o symex_other.o slice_by_trace.o symex_decl.o symex_dead.o rewrite_union.o precondition.o postcondition.o symex_clean_expr.o symex_dereference_state.o auto_objects.o symex_catch.o symex_start_thread.o symex_assign.o symex_throw.o symex_atomic_section.o memory_model.o memory_model_sc.o partial_order_concurrency.o memory_model_tso.o memory_model_pso.o gmake[1]: Leaving directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/goto-symex' ## Entering analyses gmake -C analyses gmake[1]: Entering directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/analyses' c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o natural_loops.o natural_loops.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o is_threaded.o is_threaded.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o dirty.o dirty.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o interval_analysis.o interval_analysis.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o invariant_set.o invariant_set.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o invariant_set_domain.o invariant_set_domain.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o invariant_propagation.o invariant_propagation.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o static_analysis.o static_analysis.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o uninitialized_domain.o uninitialized_domain.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o local_may_alias.o local_may_alias.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o locals.o locals.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o goto_check.o goto_check.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o call_graph.o call_graph.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o interval_domain.o interval_domain.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o goto_rw.o goto_rw.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o reaching_definitions.o reaching_definitions.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o ai.o ai.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o local_cfg.o local_cfg.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o local_bitvector_analysis.o local_bitvector_analysis.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o dependence_graph.o dependence_graph.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o constant_propagator.o constant_propagator.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o replace_symbol_ext.o replace_symbol_ext.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o flow_insensitive_analysis.o flow_insensitive_analysis.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o custom_bitvector_analysis.o custom_bitvector_analysis.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o escape_analysis.o escape_analysis.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o global_may_alias.o global_may_alias.cpp ar rc analyses.a natural_loops.o is_threaded.o dirty.o interval_analysis.o invariant_set.o invariant_set_domain.o invariant_propagation.o static_analysis.o uninitialized_domain.o local_may_alias.o locals.o goto_check.o call_graph.o interval_domain.o goto_rw.o reaching_definitions.o ai.o local_cfg.o local_bitvector_analysis.o dependence_graph.o constant_propagator.o replace_symbol_ext.o flow_insensitive_analysis.o custom_bitvector_analysis.o escape_analysis.o global_may_alias.o gmake[1]: Leaving directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/analyses' ## Entering pointer-analysis gmake -C pointer-analysis gmake[1]: Entering directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/pointer-analysis' c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o value_set.o value_set.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o goto_program_dereference.o goto_program_dereference.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o value_set_analysis.o value_set_analysis.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o dereference.o dereference.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o pointer_offset_sum.o pointer_offset_sum.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o add_failed_symbols.o add_failed_symbols.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o show_value_sets.o show_value_sets.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o value_set_domain.o value_set_domain.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o rewrite_index.o rewrite_index.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o value_set_analysis_fi.o value_set_analysis_fi.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o value_set_fi.o value_set_fi.cpp value_set_fi.cpp:876:9: warning: parentheses were disambiguated as redundant parentheses around declaration of variable named 'it' [-Wvexing-parse] forall_objects(it, omt.read()) ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ value_set_fi.cpp:34:37: note: expanded from macro 'forall_objects' for(object_map_dt::const_iterator (it) = (map).begin(); \ ^~~~ value_set_fi.cpp:876:9: note: add enclosing parentheses to perform a function-style cast value_set_fi.cpp:34:7: note: expanded from macro 'forall_objects' for(object_map_dt::const_iterator (it) = (map).begin(); \ ^ value_set_fi.cpp:876:9: note: remove parentheses to silence this warning value_set_fi.cpp:34:37: note: expanded from macro 'forall_objects' for(object_map_dt::const_iterator (it) = (map).begin(); \ ^ 1 warning generated. c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o value_set_domain_fi.o value_set_domain_fi.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o value_set_analysis_fivr.o value_set_analysis_fivr.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o value_set_fivr.o value_set_fivr.cpp value_set_fivr.cpp:120:14: warning: variable 'width' set but not used [-Wunused-but-set-variable] unsigned width=0; ^ value_set_fivr.cpp:999:9: warning: parentheses were disambiguated as redundant parentheses around declaration of variable named 'it' [-Wvexing-parse] forall_objects(it, omt.read()) ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ value_set_fivr.cpp:35:37: note: expanded from macro 'forall_objects' for(object_map_dt::const_iterator (it) = (map).begin(); \ ^~~~ value_set_fivr.cpp:999:9: note: add enclosing parentheses to perform a function-style cast value_set_fivr.cpp:35:7: note: expanded from macro 'forall_objects' for(object_map_dt::const_iterator (it) = (map).begin(); \ ^ value_set_fivr.cpp:999:9: note: remove parentheses to silence this warning value_set_fivr.cpp:35:37: note: expanded from macro 'forall_objects' for(object_map_dt::const_iterator (it) = (map).begin(); \ ^ 2 warnings generated. c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o value_set_domain_fivr.o value_set_domain_fivr.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o value_set_analysis_fivrns.o value_set_analysis_fivrns.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o value_set_fivrns.o value_set_fivrns.cpp value_set_fivrns.cpp:123:12: warning: variable 'width' set but not used [-Wunused-but-set-variable] unsigned width=0; ^ 1 warning generated. c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o value_set_domain_fivrns.o value_set_domain_fivrns.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o value_set_dereference.o value_set_dereference.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o dereference_callback.o dereference_callback.cpp ar rc pointer-analysis.a value_set.o goto_program_dereference.o value_set_analysis.o dereference.o pointer_offset_sum.o add_failed_symbols.o show_value_sets.o value_set_domain.o rewrite_index.o value_set_analysis_fi.o value_set_fi.o value_set_domain_fi.o value_set_analysis_fivr.o value_set_fivr.o value_set_domain_fivr.o value_set_analysis_fivrns.o value_set_fivrns.o value_set_domain_fivrns.o value_set_dereference.o dereference_callback.o gmake[1]: Leaving directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/pointer-analysis' ## Entering goto-programs gmake -C goto-programs gmake[1]: Entering directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/goto-programs' c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o goto_convert.o goto_convert.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o goto_convert_function_call.o goto_convert_function_call.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o goto_convert_side_effect.o goto_convert_side_effect.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o goto_program.o goto_program.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o basic_blocks.o basic_blocks.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o goto_convert_exceptions.o goto_convert_exceptions.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o property_checker.o property_checker.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o remove_function_pointers.o remove_function_pointers.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o goto_functions.o goto_functions.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o goto_inline.o goto_inline.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o remove_skip.o remove_skip.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o goto_convert_functions.o goto_convert_functions.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o string_instrumentation.o string_instrumentation.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o builtin_functions.o builtin_functions.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o show_properties.o show_properties.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o set_properties.o set_properties.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o read_goto_binary.o read_goto_binary.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o goto_asm.o goto_asm.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o elf_reader.o elf_reader.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o show_symbol_table.o show_symbol_table.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o string_abstraction.o string_abstraction.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o destructor.o destructor.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o remove_asm.o remove_asm.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o read_bin_goto_object.o read_bin_goto_object.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o goto_program_irep.o goto_program_irep.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o interpreter.o interpreter.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o interpreter_evaluate.o interpreter_evaluate.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o json_goto_trace.o json_goto_trace.cpp json_goto_trace.cpp:141:24: warning: loop variable 'l_it' creates a copy from type 'const value_type' (aka 'const exprt') [-Wrange-loop-construct] for(const auto l_it : it.io_args) ^ json_goto_trace.cpp:141:13: note: use reference type 'const value_type &' (aka 'const exprt &') to prevent copying for(const auto l_it : it.io_args) ^~~~~~~~~~~~~~~~~ & json_goto_trace.cpp:165:24: warning: loop variable 'l_it' creates a copy from type 'const value_type' (aka 'const exprt') [-Wrange-loop-construct] for(const auto l_it : it.io_args) ^ json_goto_trace.cpp:165:13: note: use reference type 'const value_type &' (aka 'const exprt &') to prevent copying for(const auto l_it : it.io_args) ^~~~~~~~~~~~~~~~~ & 2 warnings generated. c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o format_strings.o format_strings.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o loop_ids.o loop_ids.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o pointer_arithmetic.o pointer_arithmetic.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o goto_program_template.o goto_program_template.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o write_goto_binary.o write_goto_binary.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o remove_unreachable.o remove_unreachable.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o remove_unused_functions.o remove_unused_functions.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o remove_vector.o remove_vector.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o wp.o wp.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o goto_clean_expr.o goto_clean_expr.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o safety_checker.o safety_checker.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o parameter_assignments.o parameter_assignments.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o compute_called_functions.o compute_called_functions.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o link_to_library.o link_to_library.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o remove_returns.o remove_returns.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o osx_fat_reader.o osx_fat_reader.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o remove_complex.o remove_complex.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o goto_trace.o goto_trace.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o xml_goto_trace.o xml_goto_trace.cpp xml_goto_trace.cpp:154:24: warning: loop variable 'l_it' creates a copy from type 'const value_type' (aka 'const exprt') [-Wrange-loop-construct] for(const auto l_it : it.io_args) ^ xml_goto_trace.cpp:154:13: note: use reference type 'const value_type &' (aka 'const exprt &') to prevent copying for(const auto l_it : it.io_args) ^~~~~~~~~~~~~~~~~ & 1 warning generated. c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o vcd_goto_trace.o vcd_goto_trace.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o graphml_goto_trace.o graphml_goto_trace.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o remove_virtual_functions.o remove_virtual_functions.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o class_hierarchy.o class_hierarchy.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o show_goto_functions.o show_goto_functions.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o get_goto_model.o get_goto_model.cpp ar rc goto-programs.a goto_convert.o goto_convert_function_call.o goto_convert_side_effect.o goto_program.o basic_blocks.o goto_convert_exceptions.o property_checker.o remove_function_pointers.o goto_functions.o goto_inline.o remove_skip.o goto_convert_functions.o string_instrumentation.o builtin_functions.o show_properties.o set_properties.o read_goto_binary.o goto_asm.o elf_reader.o show_symbol_table.o string_abstraction.o destructor.o remove_asm.o read_bin_goto_object.o goto_program_irep.o interpreter.o interpreter_evaluate.o json_goto_trace.o format_strings.o loop_ids.o pointer_arithmetic.o goto_program_template.o write_goto_binary.o remove_unreachable.o remove_unused_functions.o remove_vector.o wp.o goto_clean_expr.o safety_checker.o parameter_assignments.o compute_called_functions.o link_to_library.o remove_returns.o osx_fat_reader.o remove_complex.o goto_trace.o xml_goto_trace.o vcd_goto_trace.o graphml_goto_trace.o remove_virtual_functions.o class_hierarchy.o show_goto_functions.o get_goto_model.o gmake[1]: Leaving directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/goto-programs' ## Entering json gmake -C json gmake[1]: Entering directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/json' c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o json_parser.o json_parser.cpp bison -y -v $flags -pyyjson --defines=json_y.tab.h parser.y -o json_y.tab.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o json_y.tab.o json_y.tab.cpp flex -Pyyjson -ojson_lex.yy.cpp scanner.l c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o json_lex.yy.o json_lex.yy.cpp ar rc json.a json_parser.o json_y.tab.o json_lex.yy.o gmake[1]: Leaving directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/json' ## Entering goto-instrument gmake -C goto-instrument gmake[1]: Entering directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/goto-instrument' c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o goto_instrument_parse_options.o goto_instrument_parse_options.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o rw_set.o rw_set.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o document_properties.o document_properties.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o goto_instrument_languages.o goto_instrument_languages.cpp In file included from goto_instrument_languages.cpp:9: In file included from ../langapi/mode.h:12: In file included from ../util/irep.h:12: In file included from /usr/include/c++/v1/vector:302: In file included from /usr/include/c++/v1/__memory/allocate_at_least.h:13: /usr/include/c++/v1/__memory/allocator_traits.h:325:9: warning: destructor called on non-final 'java_bytecode_parse_treet::fieldt' that has virtual functions but non-virtual destructor [-Wdelete-non-abstract-non-virtual-dtor] __p->~_Tp(); ^ /usr/include/c++/v1/list:739:34: note: in instantiation of function template specialization 'std::allocator_traits>>::destroy' requested here __node_alloc_traits::destroy(__na, _VSTD::addressof(__np->__value_)); ^ /usr/include/c++/v1/list:720:3: note: in instantiation of member function 'std::__list_imp>::clear' requested here clear(); ^ /usr/include/c++/v1/list:811:28: note: in instantiation of member function 'std::__list_imp>::~__list_imp' requested here class _LIBCPP_TEMPLATE_VIS list ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:15: note: qualify call to silence this warning __p->~_Tp(); ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:9: warning: destructor called on non-final 'java_bytecode_parse_treet::methodt' that has virtual functions but non-virtual destructor [-Wdelete-non-abstract-non-virtual-dtor] __p->~_Tp(); ^ /usr/include/c++/v1/list:739:34: note: in instantiation of function template specialization 'std::allocator_traits>>::destroy' requested here __node_alloc_traits::destroy(__na, _VSTD::addressof(__np->__value_)); ^ /usr/include/c++/v1/list:720:3: note: in instantiation of member function 'std::__list_imp>::clear' requested here clear(); ^ /usr/include/c++/v1/list:811:28: note: in instantiation of member function 'std::__list_imp>::~__list_imp' requested here class _LIBCPP_TEMPLATE_VIS list ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:15: note: qualify call to silence this warning __p->~_Tp(); ^ 2 warnings generated. c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o uninitialized.o uninitialized.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o full_slicer.o full_slicer.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o k_induction.o k_induction.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o object_id.o object_id.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o show_locations.o show_locations.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o points_to.o points_to.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o alignment_checks.o alignment_checks.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o race_check.o race_check.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o nondet_volatile.o nondet_volatile.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o interrupt.o interrupt.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o function.o function.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o branch.o branch.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o mmio.o mmio.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o stack_depth.o stack_depth.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o nondet_static.o nondet_static.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o concurrency.o concurrency.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o dump_c.o dump_c.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o dot.o dot.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o havoc_loops.o havoc_loops.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o call_sequences.o call_sequences.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o unwind.o unwind.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o function_modifies.o function_modifies.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o accelerate/accelerate.o accelerate/accelerate.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o accelerate/polynomial.o accelerate/polynomial.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o accelerate/scratch_program.o accelerate/scratch_program.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o accelerate/polynomial_accelerator.o accelerate/polynomial_accelerator.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o accelerate/util.o accelerate/util.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o accelerate/trace_automaton.o accelerate/trace_automaton.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o accelerate/enumerating_loop_acceleration.o accelerate/enumerating_loop_acceleration.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o accelerate/all_paths_enumerator.o accelerate/all_paths_enumerator.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o accelerate/sat_path_enumerator.o accelerate/sat_path_enumerator.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o accelerate/disjunctive_polynomial_acceleration.o accelerate/disjunctive_polynomial_acceleration.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o accelerate/cone_of_influence.o accelerate/cone_of_influence.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o accelerate/overflow_instrumenter.o accelerate/overflow_instrumenter.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o accelerate/path.o accelerate/path.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o accelerate/acceleration_utils.o accelerate/acceleration_utils.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o count_eloc.o count_eloc.cpp count_eloc.cpp:72:44: warning: loop variable 'lines' of type 'const std::pair &' (aka 'const pair> &') binds to a temporary constructed from type 'reference' (aka 'const pair, std::allocator>> &') [-Wrange-loop-construct] for(const std::pair &lines : files.second) ^ count_eloc.cpp:72:9: note: use non-reference type 'std::pair' (aka 'pair>') to make construction explicit or type 'const value_type &' (aka 'const pair, std::allocator>> &') to prevent copying for(const std::pair &lines : files.second) ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ count_eloc.cpp:71:42: warning: loop variable 'files' of type 'const std::pair &' (aka 'const pair, dstring_hash>> &') binds to a temporary constructed from type 'reference' (aka 'pair, std::allocator>, dstring_hash, std::equal_to, std::allocator, std::allocator>>>>> &') [-Wrange-loop-construct] for(const std::pair &files : eloc_map) ^ count_eloc.cpp:71:7: note: use non-reference type 'std::pair' (aka 'pair, dstring_hash>>') to make construction explicit or type 'const value_type &' (aka 'const pair, std::allocator>, dstring_hash, std::equal_to, std::allocator, std::allocator>>>>> &') to prevent copying for(const std::pair &files : eloc_map) ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ count_eloc.cpp:96:44: warning: loop variable 'lines' of type 'const std::pair &' (aka 'const pair> &') binds to a temporary constructed from type 'reference' (aka 'const pair, std::allocator>> &') [-Wrange-loop-construct] for(const std::pair &lines : files.second) ^ count_eloc.cpp:96:9: note: use non-reference type 'std::pair' (aka 'pair>') to make construction explicit or type 'const value_type &' (aka 'const pair, std::allocator>> &') to prevent copying for(const std::pair &lines : files.second) ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ count_eloc.cpp:95:42: warning: loop variable 'files' of type 'const std::pair &' (aka 'const pair, dstring_hash>> &') binds to a temporary constructed from type 'reference' (aka 'pair, std::allocator>, dstring_hash, std::equal_to, std::allocator, std::allocator>>>>> &') [-Wrange-loop-construct] for(const std::pair &files : eloc_map) ^ count_eloc.cpp:95:7: note: use non-reference type 'std::pair' (aka 'pair, dstring_hash>>') to make construction explicit or type 'const value_type &' (aka 'const pair, std::allocator>, dstring_hash, std::equal_to, std::allocator, std::allocator>>>>> &') to prevent copying for(const std::pair &files : eloc_map) ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 4 warnings generated. c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o reachability_slicer.o reachability_slicer.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o goto_program2code.o goto_program2code.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o wmm/abstract_event.o wmm/abstract_event.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o wmm/fence.o wmm/fence.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o wmm/shared_buffers.o wmm/shared_buffers.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o wmm/cycle_collection.o wmm/cycle_collection.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o wmm/goto2graph.o wmm/goto2graph.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o wmm/weak_memory.o wmm/weak_memory.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o wmm/data_dp.o wmm/data_dp.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o wmm/instrumenter_strategies.o wmm/instrumenter_strategies.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o wmm/event_graph.o wmm/event_graph.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o wmm/pair_collection.o wmm/pair_collection.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o goto_instrument_main.o goto_instrument_main.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o horn_encoding.o horn_encoding.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o thread_instrumentation.o thread_instrumentation.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o skip_loops.o skip_loops.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o loop_utils.o loop_utils.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o code_contracts.o code_contracts.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o cover.o cover.cpp c++ -o goto-instrument -Wl,--start-group ../ansi-c/ansi-c.a ../cpp/cpp.a ../linking/linking.a ../big-int/big-int.a ../goto-programs/goto-programs.a ../goto-symex/goto-symex.a ../assembler/assembler.a ../pointer-analysis/pointer-analysis.a ../analyses/analyses.a ../langapi/langapi.a ../xmllang/xmllang.a ../util/util.a ../solvers/solvers.a goto_instrument_parse_options.o rw_set.o document_properties.o goto_instrument_languages.o uninitialized.o full_slicer.o k_induction.o object_id.o show_locations.o points_to.o alignment_checks.o race_check.o nondet_volatile.o interrupt.o function.o branch.o mmio.o stack_depth.o nondet_static.o concurrency.o dump_c.o dot.o havoc_loops.o call_sequences.o unwind.o function_modifies.o accelerate/accelerate.o accelerate/polynomial.o accelerate/scratch_program.o accelerate/polynomial_accelerator.o accelerate/util.o accelerate/trace_automaton.o accelerate/enumerating_loop_acceleration.o accelerate/all_paths_enumerator.o accelerate/sat_path_enumerator.o accelerate/disjunctive_polynomial_acceleration.o accelerate/cone_of_influence.o accelerate/overflow_instrumenter.o accelerate/path.o accelerate/acceleration_utils.o count_eloc.o reachability_slicer.o goto_program2code.o wmm/abstract_event.o wmm/fence.o wmm/shared_buffers.o wmm/cycle_collection.o wmm/goto2graph.o wmm/weak_memory.o wmm/data_dp.o wmm/instrumenter_strategies.o wmm/event_graph.o wmm/pair_collection.o goto_instrument_main.o horn_encoding.o thread_instrumentation.o skip_loops.o loop_utils.o code_contracts.o cover.o ../java_bytecode/java_bytecode.a -Wl,--end-group gmake[1]: Leaving directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/goto-instrument' ## Entering cbmc gmake -C cbmc gmake[1]: Entering directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/cbmc' c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -DHAVE_JSIL -o cbmc_main.o cbmc_main.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -DHAVE_JSIL -o cbmc_parse_options.o cbmc_parse_options.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -DHAVE_JSIL -o bmc.o bmc.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -DHAVE_JSIL -o cbmc_dimacs.o cbmc_dimacs.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -DHAVE_JSIL -o cbmc_languages.o cbmc_languages.cpp In file included from cbmc_languages.cpp:9: In file included from ../langapi/mode.h:12: In file included from ../util/irep.h:12: In file included from /usr/include/c++/v1/vector:302: In file included from /usr/include/c++/v1/__memory/allocate_at_least.h:13: /usr/include/c++/v1/__memory/allocator_traits.h:325:9: warning: destructor called on non-final 'java_bytecode_parse_treet::fieldt' that has virtual functions but non-virtual destructor [-Wdelete-non-abstract-non-virtual-dtor] __p->~_Tp(); ^ /usr/include/c++/v1/list:739:34: note: in instantiation of function template specialization 'std::allocator_traits>>::destroy' requested here __node_alloc_traits::destroy(__na, _VSTD::addressof(__np->__value_)); ^ /usr/include/c++/v1/list:720:3: note: in instantiation of member function 'std::__list_imp>::clear' requested here clear(); ^ /usr/include/c++/v1/list:811:28: note: in instantiation of member function 'std::__list_imp>::~__list_imp' requested here class _LIBCPP_TEMPLATE_VIS list ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:15: note: qualify call to silence this warning __p->~_Tp(); ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:9: warning: destructor called on non-final 'java_bytecode_parse_treet::methodt' that has virtual functions but non-virtual destructor [-Wdelete-non-abstract-non-virtual-dtor] __p->~_Tp(); ^ /usr/include/c++/v1/list:739:34: note: in instantiation of function template specialization 'std::allocator_traits>>::destroy' requested here __node_alloc_traits::destroy(__na, _VSTD::addressof(__np->__value_)); ^ /usr/include/c++/v1/list:720:3: note: in instantiation of member function 'std::__list_imp>::clear' requested here clear(); ^ /usr/include/c++/v1/list:811:28: note: in instantiation of member function 'std::__list_imp>::~__list_imp' requested here class _LIBCPP_TEMPLATE_VIS list ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:15: note: qualify call to silence this warning __p->~_Tp(); ^ 2 warnings generated. c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -DHAVE_JSIL -o counterexample_beautification.o counterexample_beautification.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -DHAVE_JSIL -o bv_cbmc.o bv_cbmc.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -DHAVE_JSIL -o symex_bmc.o symex_bmc.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -DHAVE_JSIL -o show_vcc.o show_vcc.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -DHAVE_JSIL -o cbmc_solvers.o cbmc_solvers.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -DHAVE_JSIL -o xml_interface.o xml_interface.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -DHAVE_JSIL -o bmc_cover.o bmc_cover.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -DHAVE_JSIL -o all_properties.o all_properties.cpp c++ -o cbmc -Wl,--start-group ../ansi-c/ansi-c.a ../cpp/cpp.a ../linking/linking.a ../big-int/big-int.a ../goto-programs/goto-programs.a ../goto-symex/goto-symex.a ../pointer-analysis/value_set.o ../pointer-analysis/value_set_analysis_fi.o ../pointer-analysis/value_set_domain_fi.o ../pointer-analysis/value_set_fi.o ../pointer-analysis/value_set_dereference.o ../pointer-analysis/dereference_callback.o ../pointer-analysis/add_failed_symbols.o ../pointer-analysis/rewrite_index.o ../pointer-analysis/goto_program_dereference.o ../goto-instrument/full_slicer.o ../goto-instrument/nondet_static.o ../goto-instrument/cover.o ../analyses/analyses.a ../langapi/langapi.a ../xmllang/xmllang.a ../assembler/assembler.a ../solvers/solvers.a ../util/util.a cbmc_main.o cbmc_parse_options.o bmc.o cbmc_dimacs.o cbmc_languages.o counterexample_beautification.o bv_cbmc.o symex_bmc.o show_vcc.o cbmc_solvers.o xml_interface.o bmc_cover.o all_properties.o ../java_bytecode/java_bytecode.a ../jsil/jsil.a -Wl,--end-group gmake[1]: Leaving directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/cbmc' ## Entering goto-cc gmake -C goto-cc gmake[1]: Entering directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/goto-cc' c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JSIL -o goto_cc_main.o goto_cc_main.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JSIL -o goto_cc_mode.o goto_cc_mode.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JSIL -o gcc_mode.o gcc_mode.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JSIL -o gcc_cmdline.o gcc_cmdline.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JSIL -o ms_cl_cmdline.o ms_cl_cmdline.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JSIL -o ld_cmdline.o ld_cmdline.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JSIL -o compile.o compile.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JSIL -o armcc_cmdline.o armcc_cmdline.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JSIL -o run.o run.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JSIL -o goto_cc_languages.o goto_cc_languages.cpp In file included from goto_cc_languages.cpp:9: In file included from ../langapi/mode.h:12: In file included from ../util/irep.h:12: In file included from /usr/include/c++/v1/vector:302: In file included from /usr/include/c++/v1/__memory/allocate_at_least.h:13: /usr/include/c++/v1/__memory/allocator_traits.h:325:9: warning: destructor called on non-final 'java_bytecode_parse_treet::fieldt' that has virtual functions but non-virtual destructor [-Wdelete-non-abstract-non-virtual-dtor] __p->~_Tp(); ^ /usr/include/c++/v1/list:739:34: note: in instantiation of function template specialization 'std::allocator_traits>>::destroy' requested here __node_alloc_traits::destroy(__na, _VSTD::addressof(__np->__value_)); ^ /usr/include/c++/v1/list:720:3: note: in instantiation of member function 'std::__list_imp>::clear' requested here clear(); ^ /usr/include/c++/v1/list:811:28: note: in instantiation of member function 'std::__list_imp>::~__list_imp' requested here class _LIBCPP_TEMPLATE_VIS list ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:15: note: qualify call to silence this warning __p->~_Tp(); ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:9: warning: destructor called on non-final 'java_bytecode_parse_treet::methodt' that has virtual functions but non-virtual destructor [-Wdelete-non-abstract-non-virtual-dtor] __p->~_Tp(); ^ /usr/include/c++/v1/list:739:34: note: in instantiation of function template specialization 'std::allocator_traits>>::destroy' requested here __node_alloc_traits::destroy(__na, _VSTD::addressof(__np->__value_)); ^ /usr/include/c++/v1/list:720:3: note: in instantiation of member function 'std::__list_imp>::clear' requested here clear(); ^ /usr/include/c++/v1/list:811:28: note: in instantiation of member function 'std::__list_imp>::~__list_imp' requested here class _LIBCPP_TEMPLATE_VIS list ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:15: note: qualify call to silence this warning __p->~_Tp(); ^ 2 warnings generated. c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JSIL -o goto_cc_cmdline.o goto_cc_cmdline.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JSIL -o ms_cl_mode.o ms_cl_mode.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JSIL -o armcc_mode.o armcc_mode.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JSIL -o cw_mode.o cw_mode.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JSIL -o ld_mode.o ld_mode.cpp c++ -o goto-cc -Wl,--start-group ../big-int/big-int.a ../goto-programs/goto-programs.a ../util/util.a ../linking/linking.a ../ansi-c/ansi-c.a ../cpp/cpp.a ../xmllang/xmllang.a ../assembler/assembler.a ../langapi/langapi.a goto_cc_main.o goto_cc_mode.o gcc_mode.o gcc_cmdline.o ms_cl_cmdline.o ld_cmdline.o compile.o armcc_cmdline.o run.o goto_cc_languages.o goto_cc_cmdline.o ms_cl_mode.o armcc_mode.o cw_mode.o ld_mode.o ../java_bytecode/java_bytecode.a ../jsil/jsil.a -Wl,--end-group gmake[1]: Leaving directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/goto-cc' ## Entering path-symex gmake -C path-symex gmake[1]: Entering directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/path-symex' c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o locs.o locs.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o var_map.o var_map.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o path_symex_history.o path_symex_history.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o path_symex_state.o path_symex_state.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o path_symex.o path_symex.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o build_goto_trace.o build_goto_trace.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o path_replay.o path_replay.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -o path_symex_state_read.o path_symex_state_read.cpp ar rc path-symex.a locs.o var_map.o path_symex_history.o path_symex_state.o path_symex.o build_goto_trace.o path_replay.o path_symex_state_read.o gmake[1]: Leaving directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/path-symex' ## Entering symex gmake -C symex gmake[1]: Entering directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/symex' c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o symex_main.o symex_main.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o symex_parse_options.o symex_parse_options.cpp In file included from symex_parse_options.cpp:9: In file included from /usr/include/c++/v1/iostream:43: In file included from /usr/include/c++/v1/ios:221: In file included from /usr/include/c++/v1/__locale:18: In file included from /usr/include/c++/v1/mutex:191: In file included from /usr/include/c++/v1/__memory/shared_ptr.h:22: In file included from /usr/include/c++/v1/__memory/allocation_guard.h:14: /usr/include/c++/v1/__memory/allocator_traits.h:325:9: warning: destructor called on non-final 'java_bytecode_parse_treet::fieldt' that has virtual functions but non-virtual destructor [-Wdelete-non-abstract-non-virtual-dtor] __p->~_Tp(); ^ /usr/include/c++/v1/list:739:34: note: in instantiation of function template specialization 'std::allocator_traits>>::destroy' requested here __node_alloc_traits::destroy(__na, _VSTD::addressof(__np->__value_)); ^ /usr/include/c++/v1/list:720:3: note: in instantiation of member function 'std::__list_imp>::clear' requested here clear(); ^ /usr/include/c++/v1/list:811:28: note: in instantiation of member function 'std::__list_imp>::~__list_imp' requested here class _LIBCPP_TEMPLATE_VIS list ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:15: note: qualify call to silence this warning __p->~_Tp(); ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:9: warning: destructor called on non-final 'java_bytecode_parse_treet::methodt' that has virtual functions but non-virtual destructor [-Wdelete-non-abstract-non-virtual-dtor] __p->~_Tp(); ^ /usr/include/c++/v1/list:739:34: note: in instantiation of function template specialization 'std::allocator_traits>>::destroy' requested here __node_alloc_traits::destroy(__na, _VSTD::addressof(__np->__value_)); ^ /usr/include/c++/v1/list:720:3: note: in instantiation of member function 'std::__list_imp>::clear' requested here clear(); ^ /usr/include/c++/v1/list:811:28: note: in instantiation of member function 'std::__list_imp>::~__list_imp' requested here class _LIBCPP_TEMPLATE_VIS list ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:15: note: qualify call to silence this warning __p->~_Tp(); ^ 2 warnings generated. c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o path_search.o path_search.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o symex_cover.o symex_cover.cpp c++ -o symex -Wl,--start-group ../ansi-c/ansi-c.a ../cpp/cpp.a ../linking/linking.a ../big-int/big-int.a ../goto-programs/goto-programs.a ../analyses/analyses.a ../langapi/langapi.a ../xmllang/xmllang.a ../assembler/assembler.a ../solvers/solvers.a ../util/util.a ../goto-symex/adjust_float_expressions.o ../goto-symex/rewrite_union.o ../pointer-analysis/dereference.o ../goto-instrument/cover.o ../path-symex/path-symex.a symex_main.o symex_parse_options.o path_search.o symex_cover.o ../java_bytecode/java_bytecode.a -Wl,--end-group gmake[1]: Leaving directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/symex' ## Entering goto-analyzer gmake -C goto-analyzer gmake[1]: Entering directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/goto-analyzer' c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -DHAVE_JSIL -o goto_analyzer_main.o goto_analyzer_main.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -DHAVE_JSIL -o goto_analyzer_parse_options.o goto_analyzer_parse_options.cpp In file included from goto_analyzer_parse_options.cpp:10: In file included from /usr/include/c++/v1/iostream:43: In file included from /usr/include/c++/v1/ios:221: In file included from /usr/include/c++/v1/__locale:18: In file included from /usr/include/c++/v1/mutex:191: In file included from /usr/include/c++/v1/__memory/shared_ptr.h:22: In file included from /usr/include/c++/v1/__memory/allocation_guard.h:14: /usr/include/c++/v1/__memory/allocator_traits.h:325:9: warning: destructor called on non-final 'java_bytecode_parse_treet::fieldt' that has virtual functions but non-virtual destructor [-Wdelete-non-abstract-non-virtual-dtor] __p->~_Tp(); ^ /usr/include/c++/v1/list:739:34: note: in instantiation of function template specialization 'std::allocator_traits>>::destroy' requested here __node_alloc_traits::destroy(__na, _VSTD::addressof(__np->__value_)); ^ /usr/include/c++/v1/list:720:3: note: in instantiation of member function 'std::__list_imp>::clear' requested here clear(); ^ /usr/include/c++/v1/list:811:28: note: in instantiation of member function 'std::__list_imp>::~__list_imp' requested here class _LIBCPP_TEMPLATE_VIS list ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:15: note: qualify call to silence this warning __p->~_Tp(); ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:9: warning: destructor called on non-final 'java_bytecode_parse_treet::methodt' that has virtual functions but non-virtual destructor [-Wdelete-non-abstract-non-virtual-dtor] __p->~_Tp(); ^ /usr/include/c++/v1/list:739:34: note: in instantiation of function template specialization 'std::allocator_traits>>::destroy' requested here __node_alloc_traits::destroy(__na, _VSTD::addressof(__np->__value_)); ^ /usr/include/c++/v1/list:720:3: note: in instantiation of member function 'std::__list_imp>::clear' requested here clear(); ^ /usr/include/c++/v1/list:811:28: note: in instantiation of member function 'std::__list_imp>::~__list_imp' requested here class _LIBCPP_TEMPLATE_VIS list ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:15: note: qualify call to silence this warning __p->~_Tp(); ^ 2 warnings generated. c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -DHAVE_JSIL -o taint_parser.o taint_parser.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -DHAVE_JSIL -o taint_analysis.o taint_analysis.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -DHAVE_JSIL -o static_analyzer.o static_analyzer.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -DHAVE_JSIL -o unreachable_instructions.o unreachable_instructions.cpp c++ -o goto-analyzer -Wl,--start-group ../ansi-c/ansi-c.a ../cpp/cpp.a ../linking/linking.a ../big-int/big-int.a ../goto-programs/goto-programs.a ../analyses/analyses.a ../pointer-analysis/pointer-analysis.a ../langapi/langapi.a ../json/json.a ../assembler/assembler.a ../util/util.a goto_analyzer_main.o goto_analyzer_parse_options.o taint_parser.o taint_analysis.o static_analyzer.o unreachable_instructions.o ../java_bytecode/java_bytecode.a ../jsil/jsil.a -Wl,--end-group gmake[1]: Leaving directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/goto-analyzer' ## Entering goto-diff gmake -C goto-diff gmake[1]: Entering directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/goto-diff' c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o goto_diff_main.o goto_diff_main.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o goto_diff_parse_options.o goto_diff_parse_options.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o goto_diff_languages.o goto_diff_languages.cpp In file included from goto_diff_languages.cpp:9: In file included from ../langapi/mode.h:12: In file included from ../util/irep.h:12: In file included from /usr/include/c++/v1/vector:302: In file included from /usr/include/c++/v1/__memory/allocate_at_least.h:13: /usr/include/c++/v1/__memory/allocator_traits.h:325:9: warning: destructor called on non-final 'java_bytecode_parse_treet::fieldt' that has virtual functions but non-virtual destructor [-Wdelete-non-abstract-non-virtual-dtor] __p->~_Tp(); ^ /usr/include/c++/v1/list:739:34: note: in instantiation of function template specialization 'std::allocator_traits>>::destroy' requested here __node_alloc_traits::destroy(__na, _VSTD::addressof(__np->__value_)); ^ /usr/include/c++/v1/list:720:3: note: in instantiation of member function 'std::__list_imp>::clear' requested here clear(); ^ /usr/include/c++/v1/list:811:28: note: in instantiation of member function 'std::__list_imp>::~__list_imp' requested here class _LIBCPP_TEMPLATE_VIS list ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:15: note: qualify call to silence this warning __p->~_Tp(); ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:9: warning: destructor called on non-final 'java_bytecode_parse_treet::methodt' that has virtual functions but non-virtual destructor [-Wdelete-non-abstract-non-virtual-dtor] __p->~_Tp(); ^ /usr/include/c++/v1/list:739:34: note: in instantiation of function template specialization 'std::allocator_traits>>::destroy' requested here __node_alloc_traits::destroy(__na, _VSTD::addressof(__np->__value_)); ^ /usr/include/c++/v1/list:720:3: note: in instantiation of member function 'std::__list_imp>::clear' requested here clear(); ^ /usr/include/c++/v1/list:811:28: note: in instantiation of member function 'std::__list_imp>::~__list_imp' requested here class _LIBCPP_TEMPLATE_VIS list ^ /usr/include/c++/v1/__memory/allocator_traits.h:325:15: note: qualify call to silence this warning __p->~_Tp(); ^ 2 warnings generated. c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o goto_diff_base.o goto_diff_base.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o syntactic_diff.o syntactic_diff.cpp c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o unified_diff.o unified_diff.cpp unified_diff.cpp:480:48: warning: loop variable 'p' of type 'const std::pair &' (aka 'const pair> &') binds to a temporary constructed from type 'reference' (aka 'const pair>> &') [-Wrange-loop-construct] for(const std::pair &p : differences_map) ^ unified_diff.cpp:480:7: note: use non-reference type 'std::pair' (aka 'pair>') to make construction explicit or type 'const value_type &' (aka 'const pair>> &') to prevent copying for(const std::pair &p : differences_map) ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1 warning generated. c++ -c -MMD -MP -std=c++11 -Wall -O2 -pipe -I .. -DHAVE_JAVA_BYTECODE -o change_impact.o change_impact.cpp c++ -o goto-diff -Wl,--start-group ../ansi-c/ansi-c.a ../cpp/cpp.a ../linking/linking.a ../big-int/big-int.a ../goto-programs/goto-programs.a ../assembler/assembler.a ../pointer-analysis/pointer-analysis.a ../analyses/analyses.a ../langapi/langapi.a ../xmllang/xmllang.a ../util/util.a ../solvers/solvers.a goto_diff_main.o goto_diff_parse_options.o goto_diff_languages.o goto_diff_base.o syntactic_diff.o unified_diff.o change_impact.o ../java_bytecode/java_bytecode.a -Wl,--end-group gmake[1]: Leaving directory '/exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/goto-diff' >>> Running fake in devel/cbmc at 1732150693.39 ===> devel/cbmc ===> Faking installation for cbmc-5.5p5 /exopi-obj/pobj/cbmc-5.5/bin/install -c -s -m 755 /exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/goto-analyzer/goto-analyzer /exopi-obj/pobj/cbmc-5.5/fake-amd64/usr/local/bin/ /exopi-obj/pobj/cbmc-5.5/bin/install -c -s -m 755 /exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/goto-cc/goto-cc /exopi-obj/pobj/cbmc-5.5/fake-amd64/usr/local/bin/ /exopi-obj/pobj/cbmc-5.5/bin/install -c -s -m 755 /exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/goto-diff/goto-diff /exopi-obj/pobj/cbmc-5.5/fake-amd64/usr/local/bin/ /exopi-obj/pobj/cbmc-5.5/bin/install -c -s -m 755 /exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/goto-instrument/goto-instrument /exopi-obj/pobj/cbmc-5.5/fake-amd64/usr/local/bin/ /exopi-obj/pobj/cbmc-5.5/bin/install -c -s -m 755 /exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/cbmc/cbmc /exopi-obj/pobj/cbmc-5.5/fake-amd64/usr/local/bin/ /exopi-obj/pobj/cbmc-5.5/bin/install -c -m 644 /exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/doc/man/cbmc.1 /exopi-obj/pobj/cbmc-5.5/fake-amd64/usr/local/man/man1/ cd /exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/doc/ && find . -type d -exec /exopi-obj/pobj/cbmc-5.5/bin/install -d -m 755 /exopi-obj/pobj/cbmc-5.5/fake-amd64/usr/local/share/doc/cbmc/{} \; cd /exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/doc/ && find . -type f -exec /exopi-obj/pobj/cbmc-5.5/bin/install -c -m 644 /exopi-obj/pobj/cbmc-5.5/cbmc-cbmc-5.5/doc/{} /exopi-obj/pobj/cbmc-5.5/fake-amd64/usr/local/share/doc/cbmc/{} \; rm /exopi-obj/pobj/cbmc-5.5/fake-amd64/usr/local/share/doc/cbmc/man/cbmc.1 rmdir /exopi-obj/pobj/cbmc-5.5/fake-amd64/usr/local/share/doc/cbmc/man/ >>> Running package in devel/cbmc at 1732150701.69 ===> devel/cbmc `/exopi-obj/pobj/cbmc-5.5/fake-amd64/.fake_done' is up to date. ===> Building package for cbmc-5.5p5 Create /exopi-cvs/ports/packages/amd64/all/cbmc-5.5p5.tgz Creating package cbmc-5.5p5 reading plist| checking dependencies| checksumming| checksumming| | 0% checksumming| | 1% checksumming|* | 1% checksumming|* | 2% checksumming|** | 3% checksumming|** | 4% checksumming|*** | 4% checksumming|*** | 5% checksumming|**** | 6% checksumming|**** | 7% checksumming|***** | 8% checksumming|***** | 9% checksumming|****** | 9% checksumming|****** | 10% checksumming|******* | 11% checksumming|******* | 12% checksumming|******** | 13% checksumming|******** | 14% checksumming|********* | 14% checksumming|********* | 15% checksumming|********** | 16% checksumming|********** | 17% checksumming|*********** | 17% checksumming|*********** | 18% checksumming|*********** | 19% checksumming|************ | 19% checksumming|************ | 20% checksumming|************* | 21% checksumming|************* | 22% checksumming|************** | 22% checksumming|************** | 23% checksumming|*************** | 24% checksumming|*************** | 25% checksumming|**************** | 26% checksumming|**************** | 27% checksumming|***************** | 27% checksumming|***************** | 28% checksumming|****************** | 29% checksumming|****************** | 30% checksumming|******************* | 31% checksumming|******************* | 32% checksumming|******************** | 32% checksumming|******************** | 33% checksumming|********************* | 34% checksumming|********************* | 35% checksumming|********************** | 36% checksumming|********************** | 37% checksumming|*********************** | 37% checksumming|*********************** | 38% checksumming|************************ | 39% checksumming|************************ | 40% checksumming|************************* | 40% checksumming|************************* | 41% checksumming|************************* | 42% checksumming|************************** | 42% checksumming|************************** | 43% checksumming|*************************** | 44% checksumming|*************************** | 45% checksumming|**************************** | 45% checksumming|**************************** | 46% checksumming|***************************** | 47% checksumming|***************************** | 48% checksumming|****************************** | 49% checksumming|****************************** | 50% checksumming|******************************* | 50% checksumming|******************************* | 51% checksumming|******************************** | 52% checksumming|******************************** | 53% checksumming|********************************* | 54% checksumming|********************************* | 55% checksumming|********************************** | 55% checksumming|********************************** | 56% checksumming|*********************************** | 57% checksumming|*********************************** | 58% checksumming|************************************ | 58% checksumming|************************************ | 59% checksumming|************************************ | 60% checksumming|************************************* | 60% checksumming|************************************* | 61% checksumming|************************************** | 62% checksumming|************************************** | 63% checksumming|*************************************** | 63% checksumming|*************************************** | 64% checksumming|**************************************** | 65% checksumming|**************************************** | 66% checksumming|***************************************** | 67% checksumming|***************************************** | 68% checksumming|****************************************** | 68% checksumming|****************************************** | 69% checksumming|******************************************* | 70% checksumming|******************************************* | 71% checksumming|******************************************** | 72% checksumming|******************************************** | 73% checksumming|********************************************* | 73% checksumming|********************************************* | 74% checksumming|********************************************** | 75% checksumming|********************************************** | 76% checksumming|*********************************************** | 77% checksumming|*********************************************** | 78% checksumming|************************************************ | 78% checksumming|************************************************ | 79% checksumming|************************************************* | 80% checksumming|************************************************* | 81% checksumming|************************************************** | 81% checksumming|************************************************** | 82% checksumming|************************************************** | 83% checksumming|*************************************************** | 83% checksumming|*************************************************** | 84% checksumming|**************************************************** | 85% checksumming|**************************************************** | 86% checksumming|***************************************************** | 86% checksumming|***************************************************** | 87% checksumming|****************************************************** | 88% checksumming|****************************************************** | 89% checksumming|******************************************************* | 90% checksumming|******************************************************* | 91% checksumming|******************************************************** | 91% checksumming|******************************************************** | 92% checksumming|********************************************************* | 93% checksumming|********************************************************* | 94% checksumming|********************************************************** | 95% checksumming|********************************************************** | 96% checksumming|*********************************************************** | 96% checksumming|*********************************************************** | 97% checksumming|************************************************************ | 98% checksumming|************************************************************ | 99% checksumming|*************************************************************| 99% checksumming|*************************************************************|100% archiving| archiving| | 0% archiving|****** | 10% archiving|************* | 20% archiving|**************** | 25% archiving|********************** | 34% archiving|************************* | 40% archiving|******************************** | 50% archiving|*********************************** | 54% archiving|***************************************** | 64% archiving|********************************************* | 70% archiving|*************************************************** | 80% archiving|********************************************************** | 90% archiving|************************************************************** | 97% archiving|************************************************************** | 98% archiving|*************************************************************** | 98% archiving|*************************************************************** | 99% archiving|****************************************************************| 99% archiving|****************************************************************|100% Link to /exopi-cvs/ports/packages/amd64/ftp/cbmc-5.5p5.tgz >>> Running clean in devel/cbmc at 1732150705.37 ===> devel/cbmc ===> Cleaning for cbmc-5.5p5 >>> Ended at 1732150706.54 max_stuck=9.91/depends=4.77/show-prepare-results=0.64/patch=1.18/configure=0.25/build=1607.11/fake=8.29/package=3.69/clean=1.19