allow an empty assigns clause

[kroening]

This adds support for an explicit empty assigns clause, denoting a pure
function.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a 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.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[codecov]

Codecov Report

Merging #6177 (7f662a3) into develop (0002950) will increase coverage by 8.08%.
The diff coverage is n/a.

@@             Coverage Diff             @@
##           develop    #6177      +/-   ##
===========================================
+ Coverage    67.40%   75.49%   +8.08%     
===========================================
  Files         1157     1450     +293     
  Lines        95236   158479   +63243     
===========================================
+ Hits         64197   119646   +55449     
- Misses       31039    38833    +7794     

Flag	Coverage Δ
cproversmt2	?
regression	?
unit	?

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files	Coverage Δ
src/util/string_container.cpp	52.94% <0.00%> (-47.06%)	⬇️
src/ansi-c/gcc_types.cpp	41.86% <0.00%> (-46.38%)	⬇️
src/solvers/prop/prop.cpp	42.85% <0.00%> (-41.76%)	⬇️
src/solvers/flattening/boolbv_member.cpp	53.65% <0.00%> (-38.65%)	⬇️
src/cpp/cpp_storage_spec.cpp	65.00% <0.00%> (-35.00%)	⬇️
src/util/cmdline.h	66.66% <0.00%> (-33.34%)	⬇️
src/solvers/strings/array_pool.h	66.66% <0.00%> (-33.34%)	⬇️
src/solvers/strings/string_refinement.h	66.66% <0.00%> (-33.34%)	⬇️
...rs/strings/string_concatenation_builtin_function.h	0.00% <0.00%> (-33.34%)	⬇️
src/ansi-c/c_typecheck_base.cpp	50.54% <0.00%> (-30.35%)	⬇️
... and 1429 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 437675a...7f662a3. Read the comment docs.

[feliperodri]

The semantics of an empty assigns clause should be that the function doesn't change any (global) arguments, right?

[kroening]

Yes!

[martin-cs]

One thing you could do with this is to allow calls to pure functions like these to appear in function contracts. SPARK uses these (expression functions IIRC) to remove the need to duplicate common annotations. Obviously we can use macros but once they need non-trivial control-flow, pure functions are much more preferable.