summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorAlasdair Armstrong2019-05-21 17:06:18 +0100
committerAlasdair Armstrong2019-05-21 17:06:18 +0100
commit9713d40546c732dab7ebd3d534267c696a0e84ed (patch)
treea7e9e366abb2660317c6f23bd49d5d0e2756a510 /src
parentd58e9c73731b969ebfb8e098dc5ea60d61747d79 (diff)
Fix: undefined_nat test for interpreter
Diffstat (limited to 'src')
-rw-r--r--src/value.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/value.ml b/src/value.ml
index 6c2e0839..e44ebda8 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -724,6 +724,7 @@ let primops =
("undefined_unit", fun _ -> V_unit);
("undefined_bit", fun _ -> V_bit Sail_lib.B0);
("undefined_int", fun _ -> V_int Big_int.zero);
+ ("undefined_nat", fun _ -> V_int Big_int.zero);
("undefined_bool", fun _ -> V_bool false);
("undefined_vector", value_undefined_vector);
("undefined_string", fun _ -> V_string "");