daikon icon indicating copy to clipboard operation
daikon copied to clipboard

Published 20 hours ago • verified publisher icon codespecs

Exception exit support

Open markro49 opened this issue 7 years ago • 5 comments

I have completed an upstream merge of Philipp Hirch's changes to add exception exit ppts to chicory output files. I think there might be a little more common code in chicory/Instrument and dcomp/DCIstrument that can be merged, but that can wait until latter.

markro49 avatar Jul 17 '17 14:07 markro49

Should have mentioned that this subsumes https://github.com/codespecs/daikon/pull/56. That pull request will be deleted/closed as part of this work.

markro49 avatar Jul 17 '17 14:07 markro49

still need to update doc files

markro49 avatar Jul 28 '17 17:07 markro49

As we discussed, I have completed this work and it is ready for review.

markro49 avatar Aug 02 '17 02:08 markro49

A few high-level questions:

foo():::ENTER is the point at the entry to procedure foo(). The invariants at that point are the preconditions for the foo() method, properties that are always true when the procedure is invoked.

Are these normal preconditions or overall preconditions?

Is there a way to determine exceptional preconditions for a given :::EXCEPTION program point? A user may want to know, what are the preconditions (the properties upon entry to the routine) that lead to this particular exception.

The Daikon manual (section 5.2) doesn't mention EXCEPTIONUNCAUGHT program points, but it should.

mernst avatar Aug 03 '17 18:08 mernst

The build is failing, which indicates I broke something. Sorry about that. I'll look into it this evening.

mernst avatar Aug 01 '18 18:08 mernst