---
layout: fc_discuss_archives
title: Message 27 from Frama-C-discuss on November 2010
---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] \at in ACSL assertions
- Subject: [Frama-c-discuss] \at in ACSL assertions
- From: anne.pacalet at inria.fr (Anne Pacalet)
- Date: Mon, 15 Nov 2010 16:56:36 +0100
- In-reply-to: <1289836319.1984.68.camel@guillaume-laptop>
- References: <AANLkTimyk_961c8Xk6_U33TAxabBGSeoaRB+EtM-OiBR@mail.gmail.com> <20101115145125.5bad24be@is010235> <4CE13E87.5030807@adacore.com> <2035721159.552419.1289831625935.JavaMail.root@zmbs3.inria.fr> <1289832872.1984.60.camel@guillaume-laptop> <2038674242.558849.1289835496349.JavaMail.root@zmbs3.inria.fr> <1289836319.1984.68.camel@guillaume-laptop>
Le 15/11/2010 16:51, Guillaume Melquiond a ?crit :
> So I will state my point again and refrain from giving an example. It is
> not obvious to me that \at(v,l) is the value of variable v the last time
> the program reached label l. It could also be any value of v any time
> the program reached l.
Your interpretation looks strange if you consider the annotation :
//@ assert x > \at (y, Here);
Would it means that x is greater than every values y can take
in any execution ?
Best regards,
--
Anne.