Merge pull request #5225 from jeannielynnmoulton/jeannie/LogInvariantViolations

jeannielynnmoulton · web-flow · commit 277e8a135513 · 2020-02-10T17:32:42.000Z
Catch and log invariant errors when `cbmc_invariants_should_throwt` is enabled
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;`