Skip to content

Commit

Permalink
Update .skip files
Browse files Browse the repository at this point in the history
  • Loading branch information
@schuessf
schuessf committed Aug 20, 2024
1 parent aba9b93 commit b5508be
Show file tree
Hide file tree
Showing 2 changed files with 55 additions and 16 deletions.
15 changes: 0 additions & 15 deletions trunk/examples/programs/FloatingPoint/regression/c/.skip
View file
Original file line number Diff line number Diff line change
@@ -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
56 changes: 55 additions & 1 deletion trunk/examples/programs/regression/bpl/.skip
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,12 +3,66 @@ 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
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

0 comments on commit b5508be

Please sign in to comment.