Catch and log invariant errors.

jeannielynnmoulton · jeannielynnmoulton · commit fe1290a6ebf1 · 2020-02-06T17:36:43.000Z
If cbmc_invariants_should_throwt is enabled, then invariants become
exceptions and we should log them instead of putting them into the catch
all with no information.
diff --git a/src/util/parse_options.cpp b/src/util/parse_options.cpp
@@ -118,6 +118,11 @@ int parse_options_baset::main()
     log.error() << e.what() << messaget::eom;
     return CPROVER_EXIT_EXCEPTION;
   }
+  catch(const invariant_failedt &e)
+  {
+    log.error() << e.what() << messaget::eom;
+    return CPROVER_EXIT_EXCEPTION;
+  }
   catch(...)
   {
     log.error() << "Unknown exception type!" << messaget::eom;

Original file line number	Diff line number	Diff line change
`@@ -118,6 +118,11 @@ int parse_options_baset::main()`
`118`	`118`	`log.error() << e.what() << messaget::eom;`
`119`	`119`	`return CPROVER_EXIT_EXCEPTION;`
`120`	`120`	`}`
	`121`	`+ catch(const invariant_failedt &e)`
	`122`	`+ {`
	`123`	`+ log.error() << e.what() << messaget::eom;`
	`124`	`+ return CPROVER_EXIT_EXCEPTION;`
	`125`	`+ }`
`121`	`126`	`catch(...)`
`122`	`127`	`{`
`123`	`128`	`log.error() << "Unknown exception type!" << messaget::eom;`