allow return statements in summary functions
commit943775e3eb4bde07c338257da38d9b79e5408126
authorSven Verdoolaege <skimo@kotnet.org>
Thu, 2 Mar 2017 13:06:21 +0000 (2 14:06 +0100)
committerSven Verdoolaege <skimo@kotnet.org>
Thu, 9 Mar 2017 09:41:41 +0000 (9 10:41 +0100)
treefd7dc7ba8a49b4e8233fe6faed90f378fad39c61
parent62feeb2f88bb8b253755f8072291eda43e789e95
allow return statements in summary functions

In particular, allow a return statement at the very end
of a summary function.  In principle, it would be possible
to support return statements anywhere inside a summary function,
but then care would have to be taken that any write that might
be skipped because of the return statement is turned into a may-write.

Support for return statements is enable by setting the new
return_root field of PetScan.  This allows PetScan to easily
check that the return statement does indeed appear as the final
statement in return_root.

Signed-off-by: Sven Verdoolaege <skimo@kotnet.org>
scan.cc
scan.h
tests/call8.c [new file with mode: 0644]
tests/call8.scop [new file with mode: 0644]