From 3855d2a51f122974103b8de01c6b42c7705dd869 Mon Sep 17 00:00:00 2001 From: Alistair Michael Date: Thu, 9 Jan 2025 17:34:23 +1000 Subject: [PATCH] add missing intrins from cov --- libASL/rASL_check.ml | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/libASL/rASL_check.ml b/libASL/rASL_check.ml index ee524dc1..994c3f01 100644 --- 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";