Skip to content

Commit 129444d

Browse files
[WIP] Replace throws with invariants where appropriate
Also: * adds a new expr class * fixes regression test that doesn't work with newer/stricter perl * changes return code on one regression test because its changed by the PR (If that's unwanted I can change it back though) Marked as WIP because we'll likely want to replace io_exception and interpreter_exception with system_exception and analyses_exception
1 parent 3999db0 commit 129444d

File tree

4 files changed

+205
-205
lines changed

4 files changed

+205
-205
lines changed

regression/cbmc/return6/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
main.c
33
f_def.c
4-
^EXIT=6$
4+
^EXIT=1$
55
^SIGNAL=0$
66
CONVERSION ERROR
77
--

src/goto-programs/interpreter_class.h

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ Author: Daniel Kroening, [email protected]
2323
#include "goto_functions.h"
2424
#include "goto_trace.h"
2525
#include "json_goto_trace.h"
26+
#include "interpreter.h"
2627

2728
class interpretert:public messaget
2829
{
@@ -279,8 +280,9 @@ class interpretert:public messaget
279280
{
280281
mp_vectort v;
281282
evaluate(expr, v);
283+
// FIXME not sure if this can happen
282284
if(v.size()!=1)
283-
throw "invalid boolean value";
285+
throw interpreter_errort("invalid boolean value");
284286
return v.front()!=0;
285287
}
286288

0 commit comments

Comments
 (0)