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 too
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 is
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 have
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 annotati
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 t
Dear RTEMS developers,
as some of you may be aware, I am leading a task as part of the RTEMS
Qualification activity that explores the use of formal methods to assist with
code verifications.
Some of these techniques work best if annotations are added to source code, but
these annotations are *not
