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