--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on February 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] using Alt-ergo driver files



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>