From 1a0b3ee907b1fbc8624f80b26e1b9b3d4eb7c29c Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Thu, 27 Feb 2025 19:56:19 -0500 Subject: [PATCH] Add failures due to CAR size overflow in is_fresh --- .../test-fail-none.desc | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-none.desc b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-none.desc index ed2faa39166..e053c7cd3d6 100644 --- a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-none.desc +++ b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-none.desc @@ -1,9 +1,10 @@ CORE dfcc-only main.c ---no-malloc-may-fail --dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check --pointer-overflow-check +--no-malloc-may-fail --dfcc main --enforce-contract foo ^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ CAR size is less than __CPROVER_max_malloc_size: FAILURE$ +^\[__CPROVER_contracts_car_create.assertion.d+\].*CAR size is less than __CPROVER_max_malloc_size: FAILURE$ +^\[__CPROVER_contracts_car_set_insert.assertion.d+\].*CAR size is less than __CPROVER_max_malloc_size: FAILURE$ ^\[foo.assertion.\d+\] line \d+ size is capped: FAILURE$ -^\*\* 2 of \d+ failed ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$