--- layout: fc_discuss_archives title: Message 15 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 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