--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on June 2014 ---
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 |