Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Fwd: Frama-C max_sqe question

  • Subject: [Frama-c-discuss] Fwd: Frama-C max_sqe question
  • From: Claude.Marche at inria.fr (Claude Marché)
  • Date: Tue, 10 Jun 2014 17:49:46 +0200
  • In-reply-to: <1402305133.31114.YahooMailNeo@web140902.mail.bf1.yahoo.com>
  • References: <1402305133.31114.YahooMailNeo@web140902.mail.bf1.yahoo.com>

Hi,

The best channel to ask such kind of question is the "Frama-C discuss" list.

The answer is multiple:

* ACSL proposes, afaik, a built-in predicate \num_of for such a purpose

* Anyway, I bet it is not implemented in Frama-C kernel. A fortiori,
plug-ins Jessie and WP do not support it.

* A workaround is to define your own predicate, simulating one way it
could be implemented: see for example

http://toccata.lri.fr/gallery/MullerJava.en.html

or an equivalent in ACSL in the file tests/c/muller.c of the Why 2.34
distribution

Hope this helps,

- Claude

-------- Message original --------
Sujet: 	Frama-C max_sqe question
Date : 	Mon, 9 Jun 2014 02:12:13 -0700 (PDT)
De : 	Artem Kalinovsky <artem_kalinovsky at yahoo.com>
R?pondre ? : 	Artem Kalinovsky <artem_kalinovsky at yahoo.com>
Pour : 	Claude.Marche at inria.fr <Claude.Marche at inria.fr>



Hello, Claude!

Is there any way to use  count quantifier( I mean this : (N
i:0<=i<Size:array[i]==0) ) in ACSL?

Thank you.



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