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

Hi Jochen,

Le 16/02/2017 à 17:11, Jochen Burghardt a écrit :
 >
 > * put 'axiom shift_zero: forall a:addr. shift(a,0) = a' into the file 'my_lemmas.mlw'.
 > [A great investigation]

> 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.
>

Indeed this section have been written for people to link there own symbols, not strengthen the 
builtin definition given by WP. However you were on the right track.

Your last problem is that a library is loaded only if the symbol linked in the library are used.

The solution is (when you know it) simple, if you want to add axioms to the library `memory` you can 
do it directly! :)

```
library memory:
     altergo.file += "my_lemmas.mlw";
```


Note the use of "+=" which adds a new file to load to the one already provided by WP.

Best,

-- 
François