[Why3-club] how to import NASA libraries?
dragan.stosic at gmail.com
Fri Nov 8 13:21:40 CET 2013
I'd like to import linear_algebra at ellipsoid library in the PVS file
generated by frama-c/why3.
There is predefined set of importing clauses for real,int and
IMPORTING int at Int
IMPORTING int at Abs
IMPORTING int at ComputerDivision
IMPORTING real at Real
% do not edit above this line
If I add IMPORTING linera_algebra at ellipsoid , below " % do not edit above
this line" , type checking will pass successfully.
However, if I restart PVS ( press - EDIT button again ) my changes will be
overwritten and the default PVS will appear.
Is it possible ( through ACSL or providing some parameter from command
line) to specify desired library and to provide IMPORTING library in the
PVS file generated by default?
Thanks in advance
Senior developer at IBM
e-mail: dragan.stosic at gmail.com
e-mail:DRAGANST at ie.ibm.com
IBM Technology Campus
Damastown Industrial Estate
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Why3-club