ada/SPARKlib
0
0
Fork 0
mirror of https://github.com/AdaCore/SPARKlib.git synced 2026-02-12 13:11:36 -08:00
Code Issues Packages Projects Releases Wiki Activity

Add a precondition to Empty_Vector

Browse Source
This commit is contained in:
Claire Dross
2025-11-20 09:56:36 +01:00
parent 8cdc482317
commit 2b82cbdc48
2 changed files with 3 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
src/full/spark-containers-formal-vectors.ads
View File

@@ -274,6 +274,7 @@ is
function Empty_Vector (Capacity : Count_Type := 10) return Vector
with
Global => null,
Pre => (SPARKlib_Defensive => Capacity in Capacity_Range),
Post =>
(SPARKlib_Full =>
Length (Empty_Vector'Result) = 0

2
tests/665__formal_vectors_test/test.out
View File

@@ -600,6 +600,8 @@ test_gen.adb:23:10: info: precondition proved (CVC5: 5 VC), in call inlined at t
test_gen.adb:23:10: info: precondition proved (CVC5: 5 VC), in call inlined at test_gen.adb:88, in instantiation at test.adb:14
test_gen.adb:23:10: info: precondition proved (CVC5: 5 VC), in call inlined at test_gen.adb:97, in instantiation at test.adb:11
test_gen.adb:23:10: info: precondition proved (CVC5: 5 VC), in call inlined at test_gen.adb:97, in instantiation at test.adb:14
test_gen.adb:28:21: info: precondition proved (CVC5: 2 VC), in instantiation at test.adb:11
test_gen.adb:28:21: info: precondition proved (CVC5: 2 VC), in instantiation at test.adb:14
test_gen.adb:30:07: info: precondition proved (CVC5: 1 VC), in instantiation at test.adb:11
test_gen.adb:30:07: info: precondition proved (CVC5: 1 VC), in instantiation at test.adb:14
test_gen.adb:31:07: info: precondition proved (CVC5: 1 VC), in instantiation at test.adb:11