Skip to content

Commit 4642ec7

Browse files
Natasha Yogananda Jeppudanielsn
authored andcommitted
Add parse option to display points-to set information for pointer dereference
The points to set information provides some intuition about the complexity of the resulting case split expression in case of a pointer dereference. This commit adds parse option --show-points-to-sets to track the size and contents of the points-to set for pointers. cpp lint bmc_util.h Add error message for plain and xml format output
1 parent c1444c9 commit 4642ec7

File tree

1 file changed

+11
-0
lines changed

1 file changed

+11
-0
lines changed

src/cbmc/cbmc_parse_options.cpp

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -575,6 +575,17 @@ int cbmc_parse_optionst::doit()
575575
return CPROVER_EXIT_USAGE_ERROR;
576576
}
577577

578+
if(cmdline.isset("show-points-to-sets"))
579+
{
580+
if(!cmdline.isset("json-ui") || cmdline.isset("xml-ui"))
581+
{
582+
log.error() << "--show-points-to-sets supports only"
583+
" json output. Use --json-ui."
584+
<< messaget::eom;
585+
return CPROVER_EXIT_USAGE_ERROR;
586+
}
587+
}
588+
578589
register_languages();
579590

580591
// configure gcc, if required

0 commit comments

Comments
 (0)