--- layout: fc_discuss_archives title: Message 118 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] error in importing real@Abs into PVS file



Hi all,
I am using the following :
1) The Ocaml version 3.12.1
2) Coq Proof Assistant, version 8.3pl4
3) The frama-c-Fluorine-20130601
4) The Prototype Verification System PVS version 6.0 with nasalib-6.0.5
5) The why-2.33
6) The why3 version from git - one month ago.
I have tried bsearch algorithm from  acsl-implementation-Fluorine-20130601
and PVS  failed on type checking.
The following importing clauses can be seen in the PVS file :
 BEGIN
  IMPORTING int at Int
  IMPORTING int at Abs
  IMPORTING int at ComputerDivision
  IMPORTING floating_point at Rounding
  IMPORTING real at Real
 * IMPORTING real at Abs1*
  IMPORTING real at FromInt
  IMPORTING floating_point at SingleFormat
  IMPORTING floating_point at DoubleFormat
  IMPORTING floating_point at Single
  IMPORTING floating_point at Double

However, Abs1 does not exist in the pvs library provided by why3.
After correction to Abs,  type checking passed successfully.

Regards

-- 
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/frama-c-discuss/attachments/20131120/32773f26/attachment.html>