--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on February 2017 ---
Hi, following an advice of Loic Correnson (https://bts.frama-c.com/view.php?id=2278#c6355), I'm trying to give some additional lemmas to Alt-Ergo via a driver file. In a first attempt I * added '*-wp-driver drv*' to my Frama-C command line, * put a line '*altergo.file += "my_lemmas.mlw";*' into the file '*drv*', and * put '*axiom shift_zero: forall a:addr. shift(a,0) = a*' into the file '*my_lemmas.mlw*'. This worked fine, except that Alt-Ergo complained about the unknown type '*addr*'. To remedy this, I added '*altergo.file += "/net/u/bub/.opam/system/share/frama-c/wp/ergo/Memory.mlw";*' at the beginning of file '*drv*', since the file at that absolute path defines the '*addr*' type. However, Frama-C interpreted this path as a relative one, even though it begins with a '*/*', and consequently didn't find the file. Therefore, I added instead '*altergo.file += "../../../../.opam/system/share/frama-c/wp/ergo/Memory.mlw";*', which is the relative path of that file. This made Alt-Ergo complain about '*addr*' being defined twice. Intercepting its input file revealed that it contains, after some introductory stuff, * a copy of '*Memory.mlw*' (I guess due to my first '*+=*' directive in '*drv*'), * a copy of '*my_lemmas.mlw*' (I guess due to my second '*+=*'), * another copy of '*Memory.mlw*' (I guess by default), followed by more theories and the goal. I wonder why the user-requested driver parts are inserted just in the middle of Alt-Ergo's input file. At this location, it is impossible to add the definition of '*addr*' by a '*+=*' driver directive. Therefore, I added instead '*library my_lemmas: memory*' at the beginning of file '*drv*', inspired by the syntax of '*/net/u/bub/.opam/system/share/frama-c/wp/wp.driver*', and noting that there '*ergo/Memory.mlw*' is added under '*library memory:*'. This appeared to work fine, except that my lemma didn't help Alt-Ergo. However, when I made a syntax error during extending '*my_lemmas.mlw*', I noticed that now this file isn't considered at all by Frama-C/Alt-Ergo. The latter phenomenon can easily be reproduced by running '*frama-c -wp -wp-driver errDrv foo.c*' on the attached files. Frama-C apparently just checks the file name syntax, but doesn't check the existence of the file, let alone include it somewhere. I read Sect.2.3.10 '*Linking ACSL Symbols to External Libraries*' of the Wp manual, but I didn't find a solution for my problems there. Maybe somebody can help. Thanks in advance! Best regards Jochen Burghardt -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170216/37482403/attachment.html> -------------- next part -------------- library bar: altergo.file += "some/non/existent.path"; -------------- next part -------------- A non-text attachment was scrubbed... Name: foo.c Type: text/x-csrc Size: 40 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170216/37482403/attachment.c>