[Why3-club] how to import NASA libraries?

Dragan 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
floating_point libraries.
 BEGIN
  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


-- 
Dragan Stosic
Senior developer at IBM
phone: 085-773-1050
e-mail: dragan.stosic at gmail.com
e-mail:DRAGANST at ie.ibm.com
IBM Technology Campus
Damastown Industrial Estate
Mulhuddart
Dublin 15
Ireland
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20131108/99f3377c/attachment.html>


More information about the Why3-club mailing list