[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] pvs batch mode, emacs lisp, and pc-parse
I have two questions, a specific one and a general one. I will start
with the general question.
- Is there some reference which describes the relationship between
the pvs functions such as pc-parse which are available when I am
writing strategies and specific theories and what is available
for use in batch mode?
- The specific question relates to the scenario which led to the
Suppose I have a function which takes some formula represented
as a string, uses pc-parse to get an object, manipulates the
object, and returns some string. This function is known to work
(it was tested with a simple strategy which called the function
and then printed out the returned string).
Now suppose that I want to use that function within the emacs
lisp file which is sent to pvs -batch. Is this possible? What
I have tried is moving the function to a separate file, reading
that file in as a string, concatenating a call to the function
and sending all that to pvs-send-and-wait. This gives an error;
I think due to the call to pc-parse.
Thank you yet again,