--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on May 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] One question about how to use Frama-c



As it can be seen in ACSL manual and in many examples, assigns clauses
for arrays are written as

assigns a[l..h]

- Claude


On 04/30/2015 08:55 PM, Ziqing Luo wrote:
> I've tried using "assigns \forall integer i,j,k ;..." or just "assigns
> a", but none of them works because "assigns" is expecting a left value.

-- 
Claude March?                          | tel: +33 1 69 15 66 08
INRIA Saclay - ?le-de-France           |
Universit? Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |