CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
cbmc_main.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: CBMC Main Module
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12/*
13
14 CBMC
15 Bounded Model Checking for ANSI-C
16 Copyright (C) 2001-2014 Daniel Kroening <kroening@kroening.com>
17
18*/
19
20#include "cbmc_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
31extern unsigned long long irep_hash_cnt;
32extern unsigned long long irep_cmp_cnt;
33extern unsigned long long irep_cmp_ne_cnt;
34#endif
35
36#ifdef _MSC_VER
37int 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
43int main(int argc, const char **argv)
44{
45#endif
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}
CBMC Command Line Option Processing.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
int main()
Definition example.cpp:18
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:148
std::vector< const char * > to_c_str_array(It b, It e)
Definition unicode.h:65