[Spark2014-discuss] Plans for I/O
Chapin, Peter @ VTC
PChapin at vtc.vsc.edu
Thu Jan 24 18:07:06 CET 2013
Considering that SPARK 2014 allows, even encourages, a lot of mixing of SPARK and non-SPARK code, does it make sense to provide some way for the tools to read flow information and other aspects (post conditions, say) from an auxiliary file prepared by the user? I'm thinking about the case when someone wants to use a third party Ada library and can't reasonably edit the source of the specifications. Perhaps something along the lines of the way shadow files work currently would do the trick.
From: spark2014-discuss-bounces at lists.forge.open-do.org [mailto:spark2014-discuss-bounces at lists.forge.open-do.org] On Behalf Of Arnaud Charlet
Sent: Thursday, January 24, 2013 10:48
To: Johannes Kanig
Cc: spark2014-discuss at lists.forge.open-do.org; Andrew Hawthorn
Subject: Re: [Spark2014-discuss] Plans for I/O
> > We will also need to come up with a way of telling the flow analyser
> > how to represent the Text_IO functions. This could be by adding
> > global and derives annotations to the library functions or building
> > the knowledge into the flow analyser.
> The first option would be preferrable.
Agreed, much more flexible and preferable maintenance wise to be able to add these in the sources directly rather than build into the tool itself.
Project spark2014 discuss mailing list
discuss at spark2014.forge.open-do.org
More information about the Spark2014-discuss