---
layout: fc_discuss_archives
title: Message 32 from Frama-C-discuss on April 2014
---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] question about treatment of assigns clauses in WP (Neon)
- Subject: [Frama-c-discuss] question about treatment of assigns clauses in WP (Neon)
- From: jens.gerlach at fokus.fraunhofer.de (Gerlach, Jens)
- Date: Wed, 23 Apr 2014 15:42:05 +0000
- In-reply-to: <mailman.29.1398160925.28562.frama-c-discuss@lists.gforge.inria.fr>
- References: <mailman.29.1398160925.28562.frama-c-discuss@lists.gforge.inria.fr>
Hello Virgile, Pascal, and Patrick,
thanks for your replies!
> the point is
> just to check that all occurrences of *p in assigns are guarded by a
> \valid(p) in requires.
That?s exactly what I mean!
> It'd just act as a consistency check for the
> specification itself, without any reference to an implementation which
> might not even exist in the first place.
>
Jens