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.
* `trace_word_abs = FUNC_NAMES`: As above, but traces
If that doesn’t help, I’d start removing parts of the function to narrow down where the problematic code is.
> On 14 Apr 2015, at 4:23 pm, Akash Waran <awaran at syr.edu> wrote:
> 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,
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