# Exceptional\_Cases aspect

**URL:** https://forum.ada-lang.io/t/exceptional-cases-aspect/602
**Category:** General
**Tags:** spark
**Created:** [December 19, 2023, 6:18pm UTC](https://forum.ada-lang.io/t/exceptional-cases-aspect/602 "2023-12-19T18:18:43Z")
**Posts on this page:** 2
**Page:** 1

<div class="post-metadata">

### Author: ![daniel-larraz](https://forum.ada-lang.io/letter_avatar_proxy/v4/letter/d/5daacb/32.png) [@daniel-larraz](https://forum.ada-lang.io/u/daniel-larraz)
#### Post date: [December 19, 2023, 6:18pm UTC](https://forum.ada-lang.io/t/exceptional-cases-aspect/602/1 "2023-12-19T18:18:43Z")

</div>

Hello,

I would like to use the Exceptional\_Cases aspect described in this [post](https://blog.adacore.com/spark-beyond-normal-termination). However, it seems that the latest version of GNATprove (13.2.1) available on Alire does not include the feature. Does anyone know if there is any community version of GNATprove that supports it?

Thank you,  
Daniel

---

<div class="post-metadata">

### Author: ![JC001](https://forum.ada-lang.io/letter_avatar_proxy/v4/letter/j/e56c9b/32.png) [@JC001](https://forum.ada-lang.io/u/JC001)
#### Post date: [December 19, 2023, 11:24pm UTC](https://forum.ada-lang.io/t/exceptional-cases-aspect/602/2 "2023-12-19T23:24:18Z")

</div>

I’m pretty sure this is only available in the Pro version for now.