[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
      above question.

      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,

    Erika Rice