Home My Page Projects The Why platform
Summary Activity Forums Tracker Lists Tasks Docs News SCM Files

[#9450] [why backend for pvs] Why generates pvs theory without avoiding pvs keywords

Date:
2010-01-19 17:44
Priority:
3
State:
Open
Submitted by:
Mikhail Pritula (pritmick)
Assigned to:
Nobody (None)
Hardware:
All
Product:
none
Operating System:
All
Component:
none
Version:
none
Severity:
normal
Resolution:
Won't Fix
URL:
Summary:
[why backend for pvs] Why generates pvs theory without avoiding pvs keywords

Detailed description
I have latest why 2.23 and following simple program in C:
/*@ ensures \result == 10;
@*/
int func(void) {
int end = 10;
return end;
}
I run frama-c:
$ frama-c -jessie -jessie-atp simplify keywords.c
[kernel] preprocessing with "gcc -C -E -I. -dD keywords.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir keywords.jessie
[jessie] File keywords.jessie/keywords.jc written.
[jessie] File keywords.jessie/keywords.cloc written.
[jessie] Calling Jessie tool in subdir keywords.jessie
Generating Why function func
[jessie] Calling VCs generator.
why -simplify [...] why/keywords.why
Running Simplify on proof obligations
[...]
then I run
$ cd keywords.jessie && make -f keywords.makefile pvs
WHYLIB=/usr/local/lib/why why -pvs -dir pvs -pvs-preamble "IMPORTING why@jessie"; -split-user-conj -explain -locs keywords.loc /usr/local/lib/why/why/jessie.why why/keywords.why
And then trying to prove simple lemma
% Why obligation from file "keywords.c", line 1, characters 12-25:
func_ensures_default_po_1: LEMMA
true = true IMPLIES
FORALL (result: int32) :
integer_of_int32(result) = 10 IMPLIES
FORALL (end_0: int32) :
end_0 = result IMPLIES
FORALL (return: int32) :
return = end_0 IMPLIES
integer_of_int32(return) = 10
with pvs 4.2 and got an error, connected with variable naming:
func_ensures_default_po_1 :

|-------
{1} TRUE = TRUE IMPLIES
(FORALL (result: int32):
integer_of_int32(result) = 10 IMPLIES
(FORALL (end_0: int32):
end_0 = result IMPLIES
(FORALL (return: int32):
return = end_0 IMPLIES integer_of_int32(return) = 10)))

Rule? (grind)
Found 'END' when expecting 'opsym, `, (, (#, {|, (|, [|, (:, !id!, IF, TRUE, FALSE, [||], (||), {||}, !number!, !string!, LAMBDA, FORALL, EXISTS, {, {:, LET, CASES, COND, or TABLE'
Restoring the state.

So, I suppose there is need to automatically rename that kind of variables to use pvs.
Message  ↓
Date: 2012-04-06 14:08
Sender: Claude Marché

Won't fix in Why 2.xx, but bug remains open so as to check the problem is solved
in the future PVS output of Why3

Date: 2010-11-18 10:58
Sender: Alexey Khoroshilov

The same is true for other PVS keywords. The fill list of PVS 4.2 reserved words is:
AND
ANDTHEN
ARRAY
ASSUMING
ASSUMPTION
AUTO
AUTO_REWRITE-
AUTO_REWRITE+
AXIOM
BEGIN
BUT
BY
CASES
CHALLENGE
CLAIM
CLOSURE
COND
CONJECTURE
CONTAINING
CONVERSION
CONVERSION-
CONVERSION+
COROLLARY
DATATYPE
ELSE
ELSIF
END
ENDASSUMING
ENDCASES
ENDCOND
ENDIF
ENDTABLE
EXISTS
EXPORTING
FACT
FALSE
FORALL
FORMULA
FROM
FUNCTION
HAS_TYPE
IF
IFF
IMPLIES
IMPORTING
IN
INDUCTIVE
JUDGEMENT
LAMBDA
LAW
LEMMA
LET
LIBRARY
MACRO
MEASURE
NONEMPTY_TYPE
NOT
O
OBLIGATION
OF
OR
ORELSE
POSTULATE
PROPOSITION
RECURSIVE
REWRITE
SUBLEMMA
SUBTYPE_OF
SUBTYPES
TABLE
THEN
THEOREM
THEORY
TRUE
TYPE
TYPE+
VAR
WHEN
WHERE
WITH
XOR

Field Old Value Date By
ResolutionNone2012-04-06 14:08marche