--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on February 2017 ---
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