Email Gateway (Aug 22 2022 at 09:11): Email Gateway (Aug 22 2022 at 09:11):From: Akash Waran <awaran@syr.edu>
?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
Email Gateway (Aug 22 2022 at 09:12):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
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
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.
Last updated: Apr 26 2024 at 08:19 UTC