goto-instrument --add-cmd-line-arg: Explicitly set argv (and argc) to user-specified values #6462

vmihalko · 2021-11-17T14:35:55Z

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/

Failed to find anything about --model-argc-argv in doc/cprover-manual/ so I don't know where to document --add-cmd-line-arg

Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

This PR is related to #5965.

martin-cs

I am fine with this but I would like a second opinion from someone who wasn't involved in #5965

@peterschrammel ?

martin-cs · 2021-11-17T15:24:21Z

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1842,7 +1870,7 @@ void goto_instrument_parse_optionst::help()
    HELP_REMOVE_CALLS_NO_BODY
    HELP_REMOVE_CONST_FUNCTION_POINTERS
    " --add-library                add models of C library functions\n"
-    " --model-argc-argv <n>        model up to <n> command line arguments\n"
+    HELP_ARGC_ARGV


Don't worry about fixing this for this particular PR but in general we try to make sure that the code compiles after every commit. That way we can use git bisect more easily.

codecov · 2021-11-17T16:12:40Z

Codecov Report

Merging #6462 (4fa54ba) into develop (8aa6be8) will decrease coverage by 0.64%.
The diff coverage is 97.29%.

❗ Current head 4fa54ba differs from pull request most recent head 805e196. Consider uploading reports for the commit 805e196 to get more accurate results

@@             Coverage Diff             @@
##           develop    #6462      +/-   ##
===========================================
- Coverage    76.62%   75.98%   -0.65%     
===========================================
  Files         1578     1542      -36     
  Lines       181180   165081   -16099     
===========================================
- Hits        138833   125435   -13398     
+ Misses       42347    39646    -2701

Impacted Files	Coverage Δ
...rc/goto-instrument/goto_instrument_parse_options.h	`100.00% <ø> (ø)`
.../goto-instrument/goto_instrument_parse_options.cpp	`68.89% <95.00%> (-0.44%)`	⬇️
src/goto-instrument/model_argc_argv.cpp	`89.13% <100.00%> (+0.52%)`	⬆️
unit/unit_tests.cpp	`0.00% <0.00%> (-100.00%)`	⬇️
src/goto-cc/linker_script_merge.h	`0.00% <0.00%> (-100.00%)`	⬇️
src/goto-instrument/document_properties.cpp	`0.00% <0.00%> (-89.35%)`	⬇️
src/goto-instrument/uninitialized.cpp	`0.00% <0.00%> (-87.76%)`	⬇️
src/analyses/uninitialized_domain.cpp	`0.00% <0.00%> (-81.09%)`	⬇️
src/goto-cc/linker_script_merge.cpp	`0.00% <0.00%> (-79.13%)`	⬇️
src/analyses/uninitialized_domain.h	`0.00% <0.00%> (-55.56%)`	⬇️
... and 1193 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update a0fe71a...805e196. Read the comment docs.

vmihalko · 2021-11-18T09:56:45Z

I just discovered a problem. When arg string has prefix "--" or "-" (e.g. --add-cmd-line-arg "--help") cbmc is interpreting it as another option, but it should be value for option...

TGWDB

I'd like to see some more tests about different kinds of inputs/cases/failures as the current tests are very limited.

Also more explanation/documentation of how these can/cannot be combined, since it appears like --model-argc-argv and --add-cmd-line-arg are mutually exclusive. Which in turns makes me wonder if someone would want to specify unknown command line arguments for some positions (e.g. I want to test my flag, but with any value rather than specifying the value).

TGWDB · 2021-11-19T08:37:06Z

regression/goto-instrument/argc-argv2/test2.desc

+CORE
+main.c
+--model-argc-argv 2
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring


This test only tests that the --model-argc-argv 2 is accepted, I don't think it tests the actual value 2 is used anywhere (this file fails without the flag).

TGWDB · 2021-11-19T08:37:26Z

src/config.inc

@@ -76,7 +76,7 @@ endif
 OSX_IDENTITY="Developer ID Application: Daniel Kroening"

 # Detailed version information
-CBMC_VERSION = 5.43.0
+CBMC_VERSION = 5.44.0


This should not be in this commit (but it's not important).

chrisr-diffblue · 2022-01-24T10:06:34Z

There seems to be four commits that should not be part of this PR (commits authored by others, touching unrelated code such as the version number bump...) - I wonder if a rebase has gone wrong at some point? It would be worth a fresh rebase on top of the latest develop, and if those extra commits are still hanging around at that point, explicitly drop them so that this PR contains only your changes for this feature. That would also make it easier to review :-)

vmihalko requested review from chrisr-diffblue, martin-cs and peterschrammel as code owners November 17, 2021 14:35

martin-cs approved these changes Nov 17, 2021

View reviewed changes

vmihalko force-pushed the add-cmd-line-arg branch from a140c66 to eebce96 Compare November 18, 2021 08:19

vmihalko force-pushed the add-cmd-line-arg branch 2 times, most recently from eebce96 to 4fa54ba Compare November 18, 2021 19:41

vmihalko requested a review from a team as a code owner November 18, 2021 19:41

vmihalko marked this pull request as draft November 18, 2021 21:22

TGWDB reviewed Nov 19, 2021

View reviewed changes

tautschnig assigned vmihalko Nov 19, 2021

vmihalko force-pushed the add-cmd-line-arg branch 2 times, most recently from b3ed165 to dedaee7 Compare January 22, 2022 11:57

vmihalko force-pushed the add-cmd-line-arg branch 14 times, most recently from bba217e to 805e196 Compare January 24, 2022 11:36

vmihalko closed this Jan 24, 2022

vmihalko force-pushed the add-cmd-line-arg branch from 805e196 to a0fe71a Compare January 24, 2022 11:37

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

goto-instrument --add-cmd-line-arg: Explicitly set argv (and argc) to user-specified values #6462

goto-instrument --add-cmd-line-arg: Explicitly set argv (and argc) to user-specified values #6462

Uh oh!

vmihalko commented Nov 17, 2021

Uh oh!

martin-cs left a comment

Uh oh!

martin-cs Nov 17, 2021

Uh oh!

codecov bot commented Nov 17, 2021 •

edited

Loading

Uh oh!

vmihalko commented Nov 18, 2021

Uh oh!

TGWDB left a comment

Uh oh!

TGWDB Nov 19, 2021

Uh oh!

TGWDB Nov 19, 2021

Uh oh!

chrisr-diffblue commented Jan 24, 2022

Uh oh!

Uh oh!

goto-instrument --add-cmd-line-arg: Explicitly set argv (and argc) to user-specified values #6462

goto-instrument --add-cmd-line-arg: Explicitly set argv (and argc) to user-specified values #6462

Uh oh!

Conversation

vmihalko commented Nov 17, 2021

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

martin-cs Nov 17, 2021

Choose a reason for hiding this comment

Uh oh!

codecov bot commented Nov 17, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

vmihalko commented Nov 18, 2021

Uh oh!

TGWDB left a comment

Choose a reason for hiding this comment

Uh oh!

TGWDB Nov 19, 2021

Choose a reason for hiding this comment

Uh oh!

TGWDB Nov 19, 2021

Choose a reason for hiding this comment

Uh oh!

chrisr-diffblue commented Jan 24, 2022

Uh oh!

Uh oh!

codecov bot commented Nov 17, 2021 •

edited

Loading