Add verification API call

[thomasspriggs]

• 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/
• 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.

[codecov]

Codecov Report

Base: 78.41% // Head: 78.42% // Increases project coverage by +0.01% 🎉

Coverage data is based on head (2e817d1) compared to base (206cf2a).
Patch coverage: 79.85% of modified lines in pull request are covered.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7443      +/-   ##
===========================================
+ Coverage    78.41%   78.42%   +0.01%     
===========================================
  Files         1659     1660       +1     
  Lines       190382   190387       +5     
===========================================
+ Hits        149280   149314      +34     
+ Misses       41102    41073      -29     

Impacted Files	Coverage Δ
src/ansi-c/c_typecheck_base.h	100.00% <ø> (ø)
src/libcprover-cpp/api.h	100.00% <ø> (ø)
src/solvers/flattening/pointer_logic.cpp	95.06% <ø> (ø)
src/cprover/bv_pointers_wide.cpp	58.28% <26.66%> (+0.58%)	⬆️
unit/libcprover-cpp/api.cpp	77.77% <77.77%> (ø)
src/libcprover-cpp/api.cpp	80.00% <79.48%> (-1.25%)	⬇️
regression/libcprover-cpp/call_bmc.cpp	81.25% <100.00%> (+6.25%)	⬆️
src/ansi-c/c_typecheck_expr.cpp	75.84% <100.00%> (+0.09%)	⬆️
src/libcprover-cpp/options.cpp	100.00% <100.00%> (ø)
src/solvers/flattening/bv_pointers.cpp	86.28% <100.00%> (+0.06%)	⬆️
... and 59 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

☔ View full report at Codecov.
📢 Do you have feedback about the report comment? Let us know in this issue.

[NlightNFotis]

This looks good to me as it stands.

Should this remain as a draft, or should we get this out of draft and in develop?

[NlightNFotis]

The fix for the cpplint issue is to add these lines in src/libcprover-cpp/module_dependencies.txt:

assembler
goto-checker
pointer-analysis

[esteffin]

Looks good to me except for a minor non-blocking comment.

[esteffin]

⛏️
In my opinion this function is a bit too long and complex to be in an API.

Can it be rewritten moving the logics into goto-checker or somewhere else?

[thomasspriggs]

This reflects the complexity of the existing internal APIs. There isn't a whole lot we can do without refactoring the rest of the code base, for which would need buy-in to whatever we come up with from more code owners. If its any consolation, this is a lot easier to go through than cbmc_parse_options.cpp, which is the equivalent for the cbmc command line binary. A lot of what is in this function is also comments, explaining why the calls are needed in the order they are in.

[peterschrammel]

I understand that this is a shim to get something off the ground. However, going forward, I'd generally prefer that the API was developed incrementally in a way to replace functionality in cbmc_parse_options instead of duplicating the code... with all the advantages that come with it (having an API user from the beginning and thus more thoughtfulness about the choices made; full testing on all regression tests; no risk of divergence in duplicated code, etc)