diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp
index 7ea1dd173..a6be102ae 100644
--- a/src/crab/ebpf_domain.cpp
+++ b/src/crab/ebpf_domain.cpp
@@ -1447,6 +1447,12 @@ void ebpf_domain_t::operator()(const Assume& s) {
 
 void ebpf_domain_t::operator()(const Undefined& a) {}
 
+// Simple truncation function usable with swap_endianness().
+template <class T>
+BOOST_CONSTEXPR T truncate(T x) BOOST_NOEXCEPT {
+    return x;
+}
+
 void ebpf_domain_t::operator()(const Un& stmt) {
     auto dst = reg_pack(stmt.dst);
     auto swap_endianness = [&](variable_t v, auto input, const auto& be_or_le) {
@@ -1464,34 +1470,57 @@ void ebpf_domain_t::operator()(const Un& stmt) {
         havoc(v);
         havoc_offsets(stmt.dst);
     };
-    // Swap bytes.  For 64-bit types we need the weights to fit in a
+    // Swap bytes if needed.  For 64-bit types we need the weights to fit in a
     // signed int64, but for smaller types we don't want sign extension,
     // so we use unsigned which still fits in a signed int64.
-    // TODO: use the big_endian property of the platform.
     switch (stmt.op) {
     case Un::Op::BE16:
-        swap_endianness(dst.svalue, uint16_t(0), boost::endian::native_to_big<uint16_t>);
-        swap_endianness(dst.uvalue, uint16_t(0), boost::endian::native_to_big<uint16_t>);
+        if (!thread_local_options.big_endian) {
+            swap_endianness(dst.svalue, uint16_t(0), boost::endian::endian_reverse<uint16_t>);
+            swap_endianness(dst.uvalue, uint16_t(0), boost::endian::endian_reverse<uint16_t>);
+        } else {
+            swap_endianness(dst.svalue, uint16_t(0), truncate<uint16_t>);
+            swap_endianness(dst.uvalue, uint16_t(0), truncate<uint16_t>);
+        }
         break;
     case Un::Op::BE32:
-        swap_endianness(dst.svalue, uint32_t(0), boost::endian::native_to_big<uint32_t>);
-        swap_endianness(dst.uvalue, uint32_t(0), boost::endian::native_to_big<uint32_t>);
+        if (!thread_local_options.big_endian) {
+            swap_endianness(dst.svalue, uint32_t(0), boost::endian::endian_reverse<uint32_t>);
+            swap_endianness(dst.uvalue, uint32_t(0), boost::endian::endian_reverse<uint32_t>);
+        } else {
+            swap_endianness(dst.svalue, uint32_t(0), truncate<uint32_t>);
+            swap_endianness(dst.uvalue, uint32_t(0), truncate<uint32_t>);
+        }
         break;
     case Un::Op::BE64:
-        swap_endianness(dst.svalue, int64_t(0), boost::endian::native_to_big<int64_t>);
-        swap_endianness(dst.uvalue, uint64_t(0), boost::endian::native_to_big<uint64_t>);
+        if (!thread_local_options.big_endian) {
+            swap_endianness(dst.svalue, int64_t(0), boost::endian::endian_reverse<int64_t>);
+            swap_endianness(dst.uvalue, uint64_t(0), boost::endian::endian_reverse<uint64_t>);
+        }
         break;
     case Un::Op::LE16:
-        swap_endianness(dst.svalue, uint16_t(0), boost::endian::native_to_little<uint16_t>);
-        swap_endianness(dst.uvalue, uint16_t(0), boost::endian::native_to_little<uint16_t>);
+        if (thread_local_options.big_endian) {
+            swap_endianness(dst.svalue, uint16_t(0), boost::endian::endian_reverse<uint16_t>);
+            swap_endianness(dst.uvalue, uint16_t(0), boost::endian::endian_reverse<uint16_t>);
+        } else {
+            swap_endianness(dst.svalue, uint16_t(0), truncate<uint16_t>);
+            swap_endianness(dst.uvalue, uint16_t(0), truncate<uint16_t>);
+        }
         break;
     case Un::Op::LE32:
-        swap_endianness(dst.svalue, uint32_t(0), boost::endian::native_to_little<uint32_t>);
-        swap_endianness(dst.uvalue, uint32_t(0), boost::endian::native_to_little<uint32_t>);
+        if (thread_local_options.big_endian) {
+            swap_endianness(dst.svalue, uint32_t(0), boost::endian::endian_reverse<uint32_t>);
+            swap_endianness(dst.uvalue, uint32_t(0), boost::endian::endian_reverse<uint32_t>);
+        } else {
+            swap_endianness(dst.svalue, uint32_t(0), truncate<uint32_t>);
+            swap_endianness(dst.uvalue, uint32_t(0), truncate<uint32_t>);
+        }
         break;
     case Un::Op::LE64:
-        swap_endianness(dst.svalue, int64_t(0), boost::endian::native_to_little<int64_t>);
-        swap_endianness(dst.svalue, uint64_t(0), boost::endian::native_to_little<uint64_t>);
+        if (thread_local_options.big_endian) {
+            swap_endianness(dst.svalue, int64_t(0), boost::endian::endian_reverse<int64_t>);
+            swap_endianness(dst.uvalue, uint64_t(0), boost::endian::endian_reverse<uint64_t>);
+        }
         break;
     case Un::Op::SWAP16:
         swap_endianness(dst.svalue, uint16_t(0), boost::endian::endian_reverse<uint16_t>);
diff --git a/test-data/unop.yaml b/test-data/unop.yaml
index 180ff41ca..124f33fe6 100644
--- a/test-data/unop.yaml
+++ b/test-data/unop.yaml
@@ -41,120 +41,288 @@ code:
 
 post: ["r1.type=number", "r1.svalue=[-5, 5]"]
 ---
-test-case: be16 singleton
+test-case: be16 singleton on little-endian
 
 pre: ["r1.type=number", "r1.svalue=6636321", "r1.uvalue=6636321"]
 
+options: ["!big_endian"]
+
 code:
   <start>: |
     r1 = be16 r1 ; 0x654321 -> 0x2143
 
 post: ["r1.type=number", "r1.svalue=8515", "r1.uvalue=8515"]
 ---
-test-case: be32 singleton
+test-case: be16 singleton on big-endian
+
+pre: ["r1.type=number", "r1.svalue=6636321", "r1.uvalue=6636321"]
+
+options: ["big_endian"]
+
+code:
+  <start>: |
+    r1 = be16 r1 ; 0x654321 -> 0x4321
+
+post: ["r1.type=number", "r1.svalue=17185", "r1.uvalue=17185"]
+---
+test-case: be32 singleton on little-endian
 
 pre: ["r1.type=number", "r1.svalue=40926266145", "r1.uvalue=40926266145"]
 
+options: ["!big_endian"]
+
 code:
   <start>: |
     r1 = be32 r1 ; 0x0987654321 -> 0x21436587
 
 post: ["r1.type=number", "r1.svalue=558065031", "r1.uvalue=558065031"]
 ---
-test-case: be64 singleton
+test-case: be32 singleton on big-endian
+
+pre: ["r1.type=number", "r1.svalue=40926266145", "r1.uvalue=40926266145"]
+
+options: ["big_endian"]
+
+code:
+  <start>: |
+    r1 = be32 r1 ; 0x0987654321 -> 0x87654321
+
+post: ["r1.type=number", "r1.svalue=2271560481", "r1.uvalue=2271560481"]
+---
+test-case: be64 singleton on little-endian
 
 pre: ["r1.type=number", "r1.svalue=40926266145", "r1.uvalue=40926266145"]
 
+options: ["!big_endian"]
+
 code:
   <start>: |
     r1 = be64 r1 ; 0x0987654321 -> 0x2143658709000000
 
 post: ["r1.type=number", "r1.svalue=2396871057337221120", "r1.uvalue=2396871057337221120"]
 ---
-test-case: be16 range
+test-case: be64 singleton on big-endian
+
+pre: ["r1.type=number", "r1.svalue=40926266145", "r1.uvalue=40926266145"]
+
+options: ["big_endian"]
+
+code:
+  <start>: |
+    r1 = be64 r1 ; nop
+
+post: ["r1.type=number", "r1.svalue=40926266145", "r1.uvalue=40926266145"]
+---
+test-case: be16 range on little-endian
 
 pre: ["r1.type=number", "r1.svalue=[0, 2]", "r1.uvalue=[0, 2]", "r1.svalue=r1.uvalue"]
 
+options: ["!big_endian"]
+
 code:
   <start>: |
     r1 = be16 r1 ; [0x0000, 0x0002] -> [0x0000, 0x2000] but currently we just lose the range
 
 post: ["r1.type=number"]
 ---
-test-case: le16 singleton
+test-case: be16 range on big-endian
+
+pre: ["r1.type=number", "r1.svalue=[0, 2]", "r1.uvalue=[0, 2]", "r1.svalue=r1.uvalue"]
+
+options: ["big_endian"]
+
+code:
+  <start>: |
+    r1 = be16 r1 ; nop. this could preserve the range but we don't support that yet
+
+post: ["r1.type=number"]
+---
+test-case: le16 singleton on little-endian
 
 pre: ["r1.type=number", "r1.svalue=6636321", "r1.uvalue=6636321"]
 
+options: ["!big_endian"]
+
 code:
   <start>: |
     r1 = le16 r1 ; 0x654321 -> 0x4321
 
 post: ["r1.type=number", "r1.svalue=17185", "r1.uvalue=17185"]
 ---
-test-case: le32 singleton
+test-case: le16 singleton on big-endian
+
+pre: ["r1.type=number", "r1.svalue=6636321", "r1.uvalue=6636321"]
+
+options: ["big_endian"]
+
+code:
+  <start>: |
+    r1 = le16 r1 ; 0x654321 -> 0x2143
+
+post: ["r1.type=number", "r1.svalue=8515", "r1.uvalue=8515"]
+---
+test-case: le32 singleton on little-endian
 
 pre: ["r1.type=number", "r1.svalue=40926266145", "r1.uvalue=40926266145"]
 
+options: ["!big_endian"]
+
 code:
   <start>: |
     r1 = le32 r1 ; 0x0987654321 -> 0x87654321
 
 post: ["r1.type=number", "r1.svalue=2271560481", "r1.uvalue=2271560481"]
 ---
-test-case: le64 singleton
+test-case: le32 singleton on big-endian
 
 pre: ["r1.type=number", "r1.svalue=40926266145", "r1.uvalue=40926266145"]
 
+options: ["big_endian"]
+
 code:
   <start>: |
-    r1 = le64 r1 ; 0x0987654321 -> 0x2143658709000000
+    r1 = le32 r1 ; 0x0987654321 -> 0x21436587
+
+post: ["r1.type=number", "r1.svalue=558065031", "r1.uvalue=558065031"]
+---
+test-case: le64 singleton on little-endian
+
+pre: ["r1.type=number", "r1.svalue=40926266145", "r1.uvalue=40926266145"]
+
+options: ["!big_endian"]
+
+code:
+  <start>: |
+    r1 = le64 r1 ; nop
 
 post: ["r1.type=number", "r1.svalue=40926266145", "r1.uvalue=40926266145"]
 ---
-test-case: le16 range
+test-case: le64 singleton on big-endian
+
+pre: ["r1.type=number", "r1.svalue=40926266145", "r1.uvalue=40926266145"]
+
+options: ["big_endian"]
+
+code:
+  <start>: |
+    r1 = le64 r1 ; 0x0987654321 -> 0x2143658709000000
+
+post: ["r1.type=number", "r1.svalue=2396871057337221120", "r1.uvalue=2396871057337221120"]
+---
+test-case: le16 range on little-endian
+
+pre: ["r1.type=number", "r1.svalue=[0, 2]", "r1.uvalue=[0, 2]", "r1.svalue=r1.uvalue"]
+
+options: ["!big_endian"]
+
+code:
+  <start>: |
+    r1 = le16 r1 ; nop. this could preserve the range but we don't support that yet
+
+post: ["r1.type=number"]
+---
+test-case: le16 range on big-endian
 
 pre: ["r1.type=number", "r1.svalue=[0, 2]", "r1.uvalue=[0, 2]", "r1.svalue=r1.uvalue"]
 
+options: ["!big_endian"]
+
 code:
   <start>: |
-    r1 = le16 r1 ; this could preserve the range but we don't support that yet
+    r1 = le16 r1
 
 post: ["r1.type=number"]
 ---
-test-case: swap16 singleton
+test-case: swap16 singleton on little-endian
+
+pre: ["r1.type=number", "r1.svalue=6636321", "r1.uvalue=6636321"]
+
+options: ["!big_endian"]
+
+code:
+  <start>: |
+    r1 = swap16 r1 ; 0x654321 -> 0x2143
+
+post: ["r1.type=number", "r1.svalue=8515", "r1.uvalue=8515"]
+---
+test-case: swap16 singleton on big-endian
 
 pre: ["r1.type=number", "r1.svalue=6636321", "r1.uvalue=6636321"]
 
+options: ["big_endian"]
+
 code:
   <start>: |
     r1 = swap16 r1 ; 0x654321 -> 0x2143
 
 post: ["r1.type=number", "r1.svalue=8515", "r1.uvalue=8515"]
 ---
-test-case: swap32 singleton
+test-case: swap32 singleton on little-endian
 
 pre: ["r1.type=number", "r1.svalue=40926266145", "r1.uvalue=40926266145"]
 
+options: ["!big_endian"]
+
 code:
   <start>: |
     r1 = swap32 r1 ; 0x0987654321 -> 0x21436587
 
 post: ["r1.type=number", "r1.svalue=558065031", "r1.uvalue=558065031"]
 ---
-test-case: swap64 singleton
+test-case: swap32 singleton on big-endian
 
 pre: ["r1.type=number", "r1.svalue=40926266145", "r1.uvalue=40926266145"]
 
+options: ["big_endian"]
+
+code:
+  <start>: |
+    r1 = swap32 r1 ; 0x0987654321 -> 0x21436587
+
+post: ["r1.type=number", "r1.svalue=558065031", "r1.uvalue=558065031"]
+---
+test-case: swap64 singleton on little-endian
+
+pre: ["r1.type=number", "r1.svalue=40926266145", "r1.uvalue=40926266145"]
+
+options: ["!big_endian"]
+
 code:
   <start>: |
     r1 = swap64 r1 ; 0x0987654321 -> 0x2143658709000000
 
 post: ["r1.type=number", "r1.svalue=2396871057337221120", "r1.uvalue=2396871057337221120"]
 ---
-test-case: swap16 range
+test-case: swap64 singleton on big-endian
+
+pre: ["r1.type=number", "r1.svalue=40926266145", "r1.uvalue=40926266145"]
+
+options: ["big_endian"]
+
+code:
+  <start>: |
+    r1 = swap64 r1 ; 0x0987654321 -> 0x2143658709000000
+
+post: ["r1.type=number", "r1.svalue=2396871057337221120", "r1.uvalue=2396871057337221120"]
+---
+test-case: swap16 range on little-endian
 
 pre: ["r1.type=number", "r1.svalue=[0, 2]", "r1.uvalue=[0, 2]", "r1.svalue=r1.uvalue"]
 
+options: ["!big_endian"]
+
+code:
+  <start>: |
+    r1 = swap16 r1 ; [0x0000, 0x0002] -> [0x0000, 0x2000] but currently we just lose the range
+
+post: ["r1.type=number"]
+---
+test-case: swap16 range on big-endian
+
+pre: ["r1.type=number", "r1.svalue=[0, 2]", "r1.uvalue=[0, 2]", "r1.svalue=r1.uvalue"]
+
+options: ["big_endian"]
+
 code:
   <start>: |
     r1 = swap16 r1 ; [0x0000, 0x0002] -> [0x0000, 0x2000] but currently we just lose the range