added jbmc executable

Author: Daniel Kroening

src/Makefile

@@ -1,10 +1,11 @@
-DIRS = ansi-c big-int cbmc cpp goto-cc goto-instrument goto-programs \
+DIRS = ansi-c big-int cbmc jbmc cpp goto-cc goto-instrument goto-programs \
        goto-symex langapi pointer-analysis solvers util linking xmllang \
        assembler analyses java_bytecode \
        json goto-analyzer jsil goto-diff clobber \
        memory-models miniz
 
-all: cbmc.dir goto-cc.dir goto-instrument.dir goto-analyzer.dir goto-diff.dir
+all: cbmc.dir jbmc.dir goto-cc.dir goto-instrument.dir \
+     goto-analyzer.dir goto-diff.dir
 
 ###############################################################################
 
@@ -30,6 +31,8 @@ cbmc.dir: languages solvers.dir goto-symex.dir analyses.dir \
           pointer-analysis.dir goto-programs.dir linking.dir \
           goto-instrument.dir
 
+jbmc.dir: cbmc.dir
+
 goto-analyzer.dir: languages analyses.dir goto-programs.dir linking.dir \
                    json.dir goto-instrument.dir
 

src/jbmc/Makefile

@@ -0,0 +1,63 @@
+SRC = jbmc_main.cpp \
+      jbmc_parse_options.cpp \
+      # Empty last line
+
+OBJ += ../ansi-c/ansi-c$(LIBEXT) \
+      ../java_bytecode/java_bytecode$(LIBEXT) \
+      ../linking/linking$(LIBEXT) \
+      ../big-int/big-int$(LIBEXT) \
+      ../goto-programs/goto-programs$(LIBEXT) \
+      ../goto-symex/goto-symex$(LIBEXT) \
+      ../pointer-analysis/value_set$(OBJEXT) \
+      ../pointer-analysis/value_set_analysis_fi$(OBJEXT) \
+      ../pointer-analysis/value_set_domain_fi$(OBJEXT) \
+      ../pointer-analysis/value_set_fi$(OBJEXT) \
+      ../pointer-analysis/value_set_dereference$(OBJEXT) \
+      ../pointer-analysis/dereference_callback$(OBJEXT) \
+      ../pointer-analysis/add_failed_symbols$(OBJEXT) \
+      ../pointer-analysis/rewrite_index$(OBJEXT) \
+      ../pointer-analysis/goto_program_dereference$(OBJEXT) \
+      ../goto-instrument/full_slicer$(OBJEXT) \
+      ../goto-instrument/nondet_static$(OBJEXT) \
+      ../goto-instrument/cover$(OBJEXT) \
+      ../analyses/analyses$(LIBEXT) \
+      ../langapi/langapi$(LIBEXT) \
+      ../xmllang/xmllang$(LIBEXT) \
+      ../assembler/assembler$(LIBEXT) \
+      ../solvers/solvers$(LIBEXT) \
+      ../util/util$(LIBEXT) \
+      ../miniz/miniz$(OBJEXT) \
+      ../json/json$(LIBEXT) \
+      ../cbmc/all_properties$(OBJEXT) \
+      ../cbmc/bmc$(OBJEXT) \
+      ../cbmc/bmc_cover$(OBJEXT) \
+      ../cbmc/bv_cbmc$(OBJEXT) \
+      ../cbmc/cbmc_dimacs$(OBJEXT) \
+      ../cbmc/cbmc_solvers$(OBJEXT) \
+      ../cbmc/counterexample_beautification$(OBJEXT) \
+      ../cbmc/fault_localization$(OBJEXT) \
+      ../cbmc/show_vcc$(OBJEXT) \
+      ../cbmc/symex_bmc$(OBJEXT) \
+      ../cbmc/symex_coverage$(OBJEXT) \
+      # Empty last line
+
+INCLUDES= -I ..
+
+LIBS =
+
+include ../config.inc
+include ../common
+
+CLEANFILES = jbmc$(EXEEXT)
+
+all: jbmc$(EXEEXT)
+
+###############################################################################
+
+jbmc$(EXEEXT): $(OBJ)
+	$(LINKBIN)
+
+.PHONY: jbmc-mac-signed
+
+jbmc-mac-signed: jbmc$(EXEEXT)
+	strip jbmc$(EXEEXT) ; codesign -v -s $(OSX_IDENTITY) jbmc$(EXEEXT)

src/jbmc/jbmc_main.cpp

@@ -0,0 +1,55 @@
+/*******************************************************************\
+
+Module: CBMC Main Module
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// CBMC Main Module
+
+/*
+
+  JBMC
+  Bounded Model Checking for Java
+  Copyright (C) 2017 Daniel Kroening <[email protected]>
+
+*/
+
+#include "jbmc_parse_options.h"
+
+#include <util/unicode.h>
+
+#ifdef IREP_HASH_STATS
+#include <iostream>
+#endif
+
+#ifdef IREP_HASH_STATS
+extern unsigned long long irep_hash_cnt;
+extern unsigned long long irep_cmp_cnt;
+extern unsigned long long irep_cmp_ne_cnt;
+#endif
+
+#ifdef _MSC_VER
+int wmain(int argc, const wchar_t **argv_wide)
+{
+  auto vec=narrow_argv(argc, argv_wide);
+  auto narrow=to_c_str_array(std::begin(vec), std::end(vec));
+  auto argv=narrow.data();
+#else
+int main(int argc, const char **argv)
+{
+#endif
+  jbmc_parse_optionst parse_options(argc, argv);
+
+  int res=parse_options.main();
+
+  #ifdef IREP_HASH_STATS
+  std::cout << "IREP_HASH_CNT=" << irep_hash_cnt << '\n';
+  std::cout << "IREP_CMP_CNT=" << irep_cmp_cnt << '\n';
+  std::cout << "IREP_CMP_NE_CNT=" << irep_cmp_ne_cnt << '\n';
+  #endif
+
+  return res;
+}