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] Aliasing

Le 6 juillet 2012 10:10, DAHAN Mickael <mickael.dahan at thalesgroup.com> a ?crit :

> Est-ce que certains messages d?erreurs au niveau de la ? console ? font
> r?f?rences au ph?nom?ne d?aliasing ?
> Est-ce qu?il existe des options suppl?mentaires de frama-c concernant
> l?aliasing ?
>

As said by Jens Gerlach, there's nothing in the platform itself
concerning aliasing. It would thus help if you could precise which
plug-in(s) you are trying to use. My best guess would be Jessie, who
computes a partition of the pointers into regions for generating
simpler proof obligations. This is done on a per-function basis making
some assumptions that formals parameters. If these assumption are not
met by a caller, you might see error messages related to aliases. In
that case, you can disable region computation by adding
#pragma SeparationPolicy(none)
to your C sources. See Jessie manual
(http://krakatoa.lri.fr/jessie.html) for more information.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile