From b5508be56f28f915f4b912be8eb78f30c7ec3f68 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Tue, 20 Aug 2024 10:47:48 +0200 Subject: [PATCH] Update .skip files --- .../programs/FloatingPoint/regression/c/.skip | 15 ----- trunk/examples/programs/regression/bpl/.skip | 56 ++++++++++++++++++- 2 files changed, 55 insertions(+), 16 deletions(-) diff --git a/trunk/examples/programs/FloatingPoint/regression/c/.skip b/trunk/examples/programs/FloatingPoint/regression/c/.skip index c90385358dc..ecc7d7e059b 100644 --- a/trunk/examples/programs/FloatingPoint/regression/c/.skip +++ b/trunk/examples/programs/FloatingPoint/regression/c/.skip @@ -1,18 +1,3 @@ // Timeout -BvaddWithThreeArguments.c AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml TIMEOUT -SAS09-Float.c AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml TIMEOUT SAS09-Float.c AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf AutomizerC.xml TIMEOUT ctrans-float-rounding.c AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf AutomizerC.xml TIMEOUT -cbmc_float4_PART1.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml TIMEOUT - -// MathSAT does not support quantifiers -ctrans-float-rounding.c AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR -cbmc_float-no-simp1.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR -cbmc_float-to-double2.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR -cbmc_float12.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR -cbmc_float13.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR -cbmc_float19.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR -cbmc_float20_Part1.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR -cbmc_float20_Part3.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR -cbmc_float6.i AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR -QuantifiedFloatInvariant.c AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float_Const.epf AutomizerC.xml EXCEPTION_OR_ERROR diff --git a/trunk/examples/programs/regression/bpl/.skip b/trunk/examples/programs/regression/bpl/.skip index 592e468dc0b..198a9ebe130 100644 --- a/trunk/examples/programs/regression/bpl/.skip +++ b/trunk/examples/programs/regression/bpl/.skip @@ -3,8 +3,54 @@ BugLiveVariables03-Safe.bpl AutomizerBpl-FPandBP.epf AutomizerBpl.xml TIMEOUT BugNestedSsaWithPendingContexts.bpl AutomizerBpl-forwardPredicates.epf AutomizerBpl.xml TIMEOUT BugNoPredecessorOfReturnTransition.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml TIMEOUT nestedWhileSimple-Safe.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml TIMEOUT +array10_pattern_simplified.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT +BitwiseOperations01.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml TIMEOUT +BitwiseOperations02.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml TIMEOUT +bitwiseOrUnsigned.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml TIMEOUT +builtin_ffs.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml TIMEOUT +Acsl01-EnsuresLocal-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT +Acsl03-EnsuresGlobal-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT +Tschingelhorn-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT +ShortCircuit-SideEffect-DoStatement-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT +ShortCircuit-SideEffect-ForStatement-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT +StructPositiveSum-Safe.c AutomizerC-forwardPredicates.epf AutomizerC.xml TIMEOUT +StructPositiveSum-Safe.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml TIMEOUT +StructPositiveSum-Safe.c AutomizerC-BitvectorTranslation.epf AutomizerC.xml TIMEOUT +StructPositiveSum-Safe.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml TIMEOUT +StructPositiveSum-Safe.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml TIMEOUT -// Overapproximation +// Unknown, overapproximation of bitwise operations (for integer translation) +bitwiseOrUnsigned.c AutomizerC-forwardPredicates.epf AutomizerC.xml UNKNOWN +bitwiseOrUnsigned.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml UNKNOWN +bitwiseOrUnsigned.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN +bitwiseOrUnsigned.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml UNKNOWN +bitwiseOrUnsigned.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml UNKNOWN +bitwiseOrUnsigned.c KojakC-Reach-32Bit-Default.epf KojakC.xml UNKNOWN +bitwiseOrUnsignedMinimal.c AutomizerC-forwardPredicates.epf AutomizerC.xml UNKNOWN +bitwiseOrUnsignedMinimal.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml UNKNOWN +bitwiseOrUnsignedMinimal.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN +bitwiseOrUnsignedMinimal.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml UNKNOWN +bitwiseOrUnsignedMinimal.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml UNKNOWN +bitwiseOrUnsignedMinimal.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml UNKNOWN +bitwiseOrUnsignedMinimal.c KojakC-Reach-32Bit-Default.epf KojakC.xml UNKNOWN +builtin_ffs.c AutomizerC-forwardPredicates.epf AutomizerC.xml UNKNOWN +builtin_ffs.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml UNKNOWN +builtin_ffs.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN +builtin_ffs.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml UNKNOWN +builtin_ffs.c BlockEncodingV2AutomizerC-forwardPredicates.epf BlockEncodingV2AutomizerC.xml UNKNOWN +builtin_ffs.c BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf BlockEncodingV2AutomizerC.xml UNKNOWN +builtin_ffs.c KojakC-Reach-32Bit-Default.epf KojakC.xml UNKNOWN +BitwiseOperations02.c AutomizerC-forwardPredicates.epf AutomizerC.xml UNKNOWN +BitwiseOperations02.c AutomizerC-forwardPredicates_const.epf AutomizerC.xml UNKNOWN +BitwiseOperations02.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN +BitwiseOperations02.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml UNKNOWN +BitwiseOperations02.c KojakC-Reach-32Bit-Default.epf KojakC.xml UNKNOWN + +// Unknown, unable to decide satisfiability of path constraint +array10_pattern_simplified.c AutomizerC-nestedInterpolants.epf AutomizerC.xml UNKNOWN +array10_pattern_simplified.c AutomizerC-nestedInterpolants_const.epf AutomizerC.xml UNKNOWN + +// Overapproximation, we expect unknown for Automizer Overapproximation.bpl AutomizerBpl-nestedInterpolants.epf AutomizerBpl.xml UNKNOWN Overapproximation.bpl AutomizerBpl-forwardPredicates.epf AutomizerBpl.xml UNKNOWN Overapproximation.bpl AutomizerBpl-FPandBP.epf AutomizerBpl.xml UNKNOWN @@ -12,3 +58,11 @@ Overapproximation.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml UNKNOWN // The solver is unable to evaluate the formula, PDR cannot handle this BugLiveVariables04-Safe.bpl PdrAutomizerBpl.epf PdrAutomizerBpl.xml EXCEPTION_OR_ERROR + +// We are unable to backtranslate @diff from SMT to Boogie +BugLiveVariables03-Safe.bpl AutomizerBpl-nestedInterpolants.epf AutomizerBpl.xml EXCEPTION_OR_ERROR +BugLiveVariables04-Safe.bpl AutomizerBpl-nestedInterpolants.epf AutomizerBpl.xml EXCEPTION_OR_ERROR + +// Const is only supported for infinite index sort in SMTInterpol +ConstArray.bpl AutomizerBpl-nestedInterpolants.epf AutomizerBpl.xml EXCEPTION_OR_ERROR +ConstArray.bpl AutomizerBpl-nestedInterpolants.epf PdrAutomizerBpl.xml EXCEPTION_OR_ERROR