search

Rafael-Baltazar / jmlcute

Generate unit test cases from Java files annotated with JML.
4 stars 0 forks source link

pt.ulisboa.tecnico.TestExceptionNotCaughtBug is not thrown. #7

Open Rafael-Baltazar opened 9 years ago

Rafael-Baltazar commented 9 years ago

DefinitelyNotNullPointerException is not thrown at line 17.

Rafael-Baltazar commented 9 years ago

Printing the following aspect solves the issue. import org.jmlspecs.ajmlrac.runtime.*;

public privileged aspect AspectJMLRac_pt_ulisboa_tecnicoTestExceptionNotCaughtBug { declare precedence: AspectJMLRac, ;

void around (final java.lang.Object o) throws pt.ulisboa.tecnico.TestExceptionNotCaughtBug.DefinitelyNotNullPointerException : execution(static void pt.ulisboa.tecnico.TestExceptionNotCaughtBug.isNull(java.lang.Object)) && args(o) { final java.lang.Object rac$old0; // saving old expressions and old vars related to each spec case rac$old0 = o; try { proceed(o);//executing the method } catch (Throwable rac$e) { if(rac$e instanceof pt.ulisboa.tecnico.TestExceptionNotCaughtBug.DefinitelyNotNullPointerException && o == null) { cute.Cute.Assert((rac$old0 == null)); } if(rac$e instanceof pt.ulisboa.tecnico.TestExceptionNotCaughtBug.DefinitelyNotNullPointerException) { throw (pt.ulisboa.tecnico.TestExceptionNotCaughtBug.DefinitelyNotNullPointerException)rac$e; } } } }