RE: [abc] oopsla outline

From: Eric Bodden <eric.bodden@mail.mcgill.ca>
Date: Fri Mar 03 2006 - 00:13:01 GMT

Aprove seems fine:

> * hashcode tm on approve:
> does abc now properly process approve? You mentioned
> earlier that you made it skip some problematic class.
> If that is still so, have you checked that class does
> not contain any hashing-related stuff?

/aprove/VerificationModules/TerminationProcedures/DependencyPairsProcess
or.class

Uses no hashing whatsoever

/aprove/VerificationModules/TerminationProcedures/PoloProcessorInterface
.class

Uses a Map (as interface) but only passes it on without touching it.
Also uses hash sets, but we do not check those at the moment.

/aprove/VerificationModules/TerminationProofs/MRRSccProof.class

Uses hash sets only.

Eric
Received on Fri Mar 03 00:13:24 2006

This archive was generated by hypermail 2.1.8 : Tue Mar 06 2007 - 16:13:27 GMT