From: Liam Powell <liam@liampwll.com>
Subject: SPARK and pragma Export
Date: Mon, 11 Jul 2022 03:05:24 -0700 (PDT) [thread overview]
Message-ID: <30c383d6-bdb1-4e01-94a7-623a7532f220n@googlegroups.com> (raw)
I'm wondering exactly how SPARK works with pragma Export, specifically exported procedures that may be called by multiple threads. Is SPARK capable of reasoning about procedures that are called externally, and if so is there a way to inform it about potential simultaneous calls?
reply other threads:[~2022-07-11 10:05 UTC|newest]
Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox