public String hackInv ( ARecordDeclIR type ) { if ( type . getInvariant ( ) != null ) { AFuncDeclIR invFunc = ( AFuncDeclIR ) type . getInvariant ( ) ; StringBuilder sb = new StringBuilder ( ) ; sb . append ( "inv " ) ; sb . append ( invFunc . getFormalParams ( ) . get ( 0 ) . getPattern ( ) . toString ( ) ) ; sb . append ( " == " ) ; sb . append ( invFunc . getName ( ) ) ; sb . append ( "(" ) ; sb . append ( "&" ) ; sb . append ( invFunc . getFormalParams ( ) . get ( 0 ) . getPattern ( ) . toString ( ) ) ; sb . append ( ")" ) ; return sb . toString ( ) ; } return "" ; }
FIXME Unhack invariant extraction for namedt ypes