* SPARK and pragma Export
@ 2022-07-11 10:05 Liam Powell
0 siblings, 0 replies; only message in thread
From: Liam Powell @ 2022-07-11 10:05 UTC (permalink / 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?
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-07-11 10:05 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-07-11 10:05 SPARK and pragma Export Liam Powell
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox