On 12/9/19 2:45 am, Joel Sherrill wrote:
> On Wed, Sep 11, 2019 at 7:59 AM Andrew Butterfield
> wrote:
>>> - Upstream Project not dead
>>
>> Frama-C is still actively maintained and upgraded.
>>
>>> - Wide Host Support
>>> - On other cases, have accepted that not all hosts can run the
On Wed, Sep 11, 2019 at 7:59 AM Andrew Butterfield
wrote:
>
> Hi Joel,
>
> thanks for a very detailed and comprehensive response.
>
> Some of the issues you raise here are very high level,
> for the consortium and community to discuss/agree at a high level.
>
> For now I will just focus on the
Hi Joel,
thanks for a very detailed and comprehensive response.
Some of the issues you raise here are very high level,
for the consortium and community to discuss/agree at a high level.
For now I will just focus on the issue of annotations and the kinds of
tools that might be involved.
I
I don't like to top post but in this case I hope this is OK.
This is a very challenging area from a project integration
perspective. There are a handful
of issues which we will have to figure out how to address. I think
these also apply to other
annotations like requirements and licensing
Dear Chris,
first, thanks for trying to install it !
Frama-C is one of a number of tools we are considering, so it's not a done
deal.
If used, it would only be applied to a small part of the codebase:
typically code that is very critical, but hard to test reliably.
I would expect that
On 6/9/19 9:40 pm, Andrew Butterfield wrote:
> However, if the implementation code contains loops, then we need annotations
> in
> the code at those loops. The following, from the Frama-C ACSL Tutorial
> (https://frama-c.com/acsl_tutorial_index.html) shows the annotations required
> to
> verify
