--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on July 2012 ---
[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