Re: [isabelle] error encountered while parsing in autocorres



Without the function it’s hard to say, but this should not usually occur (i.e. it’s a problem in AutoCorres, probably a missing case somewhere).

This particular exception seems to be thrown only during word abstraction and heap abstraction.

To narrow down which of these it is, I’d try combinations of

autocorres [skip_word_abs, no_heap_abs = FUN_NAME]

These options from the README.md file may also be useful:

  * `trace_heap_lift = FUNC_NAMES`: Trace the _heap abstraction_
    process for each of the given functions. The traces
    are stored in the Isabelle theory and can be quite large.
    See `tests/examples/TraceDemo.thy`.

  * `trace_word_abs = FUNC_NAMES`: As above, but traces
    _word abstraction_.

If that doesn’t help, I’d start removing parts of the function to narrow down where the problematic code is.

Cheers,
Gerwin

> On 14 Apr 2015, at 4:23 pm, Akash Waran <awaran at syr.edu> wrote:
>
> ?Hi,
>
>
> I was trying to parse my function in isabelle. The c-parser was able to parse it without issue, however autocorres spit out an "TRACE_SOLVE_TAC_FAIL" exception. What does this error mean and how would I go about debugging it?
>
>
> Note : The function that failed is pretty complex and hence I didn't include it.
>
>
> Thanks and Regards,
>
> Akash


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.