Add in elf model from Dominic/Stephen. Make run_power build again. Does not effectively use elf model yet

1 files changed, 18 insertions, 0 deletions

diff --git a/src/elf_model/bitstring.ml b/src/elf_model/bitstring.ml
new file mode 100644
index 00000000..82eeec18
--- /dev/null
+++ b/src/elf_model/bitstring.ml
@@ -0,0 +1,18 @@
+(*Generated by Lem from bitstring.lem.*)
+open Lem_basic_classes
+open Lem_bool
+open Lem_num
+
+(*type bitstring*)
+
+(*val length    : bitstring -> nat*)
+
+(*val partition : nat -> bitstring -> (bitstring * bitstring)*)
+
+(*val equal     : bitstring -> bitstring -> bool*)
+
+let instance_Basic_classes_Eq_Bitstring_bitstring_dict =({
+
+  isEqual_method = (=);
+
+  isInequal_method = (fun l r->not (l = r))})