CBMC
jbmc_main.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: CBMC Main Module
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 /*
13 
14  JBMC
15  Bounded Model Checking for Java
16  Copyright (C) 2017-2018 Daniel Kroening <kroening@kroening.com>
17 
18 */
19 
20 #include "jbmc_parse_options.h"
21 
22 #ifdef _MSC_VER
23 # include <util/unicode.h>
24 #endif
25 
26 #ifdef IREP_HASH_STATS
27 #include <iostream>
28 #endif
29 
30 #ifdef IREP_HASH_STATS
31 extern unsigned long long irep_hash_cnt;
32 extern unsigned long long irep_cmp_cnt;
33 extern unsigned long long irep_cmp_ne_cnt;
34 #endif
35 
36 #ifdef _MSC_VER
37 int wmain(int argc, const wchar_t **argv_wide)
38 {
39  auto vec=narrow_argv(argc, argv_wide);
40  auto narrow=to_c_str_array(std::begin(vec), std::end(vec));
41  auto argv=narrow.data();
42 #else
43 int main(int argc, const char **argv)
44 {
45 #endif
46  jbmc_parse_optionst parse_options(argc, argv);
47 
48  int res=parse_options.main();
49 
50  #ifdef IREP_HASH_STATS
51  std::cout << "IREP_HASH_CNT=" << irep_hash_cnt << '\n';
52  std::cout << "IREP_CMP_CNT=" << irep_cmp_cnt << '\n';
53  std::cout << "IREP_CMP_NE_CNT=" << irep_cmp_ne_cnt << '\n';
54  #endif
55 
56  return res;
57 }
virtual int main()
int main(int argc, const char **argv)
Definition: jbmc_main.cpp:43
JBMC Command Line Option Processing.
output_type narrow(input_type input)
Run-time checked narrowing cast.
Definition: narrow.h:34
std::vector< std::string > narrow_argv(int argc, const wchar_t **argv_wide)
Definition: unicode.cpp:149
std::vector< const char * > to_c_str_array(It b, It e)
Definition: unicode.h:66