add missing intrins from cov

UQ-PAC · Jan 9, 2025 · 3855d2a · 3855d2a
1 parent 8500ec0
commit 3855d2a
Showing 1 changed file with 21 additions and 0 deletions.
diff --git a/libASL/rASL_check.ml b/libASL/rASL_check.ml
@@ -109,16 +109,36 @@ module AllowedIntrinsics: InvChecker = struct
         "FPAdd";
         "FPDiv";
         "FPMul";
+        "FPMulX";
         "FPMulAdd";
+        "FPMulAddH";
         "FPSub";
         "FPSqrt";
+        "FPRSqrtStepFused";
+        "FPCompare";
+        "FPCompareGT";
+        "FPCompareGE";
+        "FPCompareEQ";
+        "FPMax";
+        "FPMin";
+        "FPMaxNum";
+        "FPMinNum";
+        "FPToFixedJS_impl";
+        "FPRecipEstimate";
+        "FPRecipStepFused";
+        "FPRecpX";
+        "BFAdd";
+        "BFMul";
         "FPCompare";
         "FixedToFP";
         "FPToFixed";
         "FPConvert";
+        "FPConvertBF";
         "FPRoundInt";
+        "FPRoundIntN";
         "not_bool";
         "and_bool";
+        "or_bool";
         "cvt_bool_bv";
         "SignExtend";
         "ZeroExtend";
@@ -131,6 +151,7 @@ module AllowedIntrinsics: InvChecker = struct
         "cvt_bits_uint";
         "eor_bits";
         "eq_bits";
+        "ne_bits";
         "ite";
         "mul_bits";
         "not_bits";