Also with the current implementation of the lib #define oldof
CONTRACT_OLDOF won't work...The only reason is doesn't work is because
the name oldof is used by the library.
If I use #define myoldof CONTRACT_OLDOF
it works fine.
My bad for not investigating the root cause of the errors I was getting. Then I'll fix this so users that don't like CONTRACT_OLDOF can just do #define oldof CONTRACT_OLDOF ans use oldof within the postcondition code :)
Also document that this #define is now possible if you don't like the macro name (but the lib can't do it by default bc of macro naming conventions).
Log in to post a comment.
