CBMC
typecheck.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "typecheck.h"
10 
11 #include "exception_utils.h"
12 #include "invariant.h"
13 
15 {
17 
18  const unsigned errors_before=
20 
21  try
22  {
23  typecheck();
24  }
25 
26  catch(int)
27  {
28  error();
29  }
30 
31  catch(const char *e)
32  {
33  error() << e << eom;
34  }
35 
36  catch(const std::string &e)
37  {
38  error() << e << eom;
39  }
40 
41  catch(const invalid_source_file_exceptiont &e)
42  {
43  error().source_location = e.get_source_location();
44  error() << e.get_reason() << messaget::eom;
45  }
46 
47  catch(const errort &e)
48  {
49  if(e.what().empty())
50  error();
51  else
52  {
53  error().source_location = e.source_location();
54  error() << e.what() << messaget::eom;
55  }
56  }
57 
58  return message_handler->get_message_count(messaget::M_ERROR)!=errors_before;
59 }
Thrown when we can't handle something in an input source file.
std::size_t get_message_count(unsigned level) const
Definition: message.h:56
source_locationt source_location
Definition: message.h:247
mstreamt & error() const
Definition: message.h:399
message_handlert * message_handler
Definition: message.h:439
@ M_ERROR
Definition: message.h:170
static eomt eom
Definition: message.h:297
virtual void typecheck()=0
virtual bool typecheck_main()
Definition: typecheck.cpp:14
#define PRECONDITION(CONDITION)
Definition: invariant.h:463