[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.
  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
Dublin 15
-------------- 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