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] using Alt-ergo driver files

  • Subject: [Frama-c-discuss] using Alt-ergo driver files
  • From: jochen.burghardt at fokus.fraunhofer.de (Jochen Burghardt)
  • Date: Thu, 16 Feb 2017 17:11:13 +0100
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>