Contents:
Todo
Need to describe __return_val and __old
(The original entry is located in /data2/autobuild/linux/gpuverify/Documentation/advanced_features.rst, line 115.)
Todo
Say that this should be used with extreme care
(The original entry is located in /data2/autobuild/linux/gpuverify/Documentation/advanced_features.rst, line 121.)
Todo
This will explain:
(The original entry is located in /data2/autobuild/linux/gpuverify/Documentation/advanced_features.rst, line 127.)
Todo
__write_implies, etc. Be sure to comment on byte-level reasoning issue.
(The original entry is located in /data2/autobuild/linux/gpuverify/Documentation/advanced_features.rst, line 139.)
Todo
Simple example of barrier invariant usage
(The original entry is located in /data2/autobuild/linux/gpuverify/Documentation/advanced_features.rst, line 206.)
Todo
Show how UFs can be used to model operations abstractly
(The original entry is located in /data2/autobuild/linux/gpuverify/Documentation/advanced_features.rst, line 211.)
Todo
Show (currently hacky) way of providing a procedure spec without body
(The original entry is located in /data2/autobuild/linux/gpuverify/Documentation/advanced_features.rst, line 216.)
Todo
Give example use of --boogie-opt
(The original entry is located in /data2/autobuild/linux/gpuverify/Documentation/advanced_features.rst, line 222.)
Todo
Describe how an external .bpl file can be used.
(The original entry is located in /data2/autobuild/linux/gpuverify/Documentation/advanced_features.rst, line 227.)
Todo
Add link to the paper with this title.
(The original entry is located in /data2/autobuild/linux/gpuverify/Documentation/basic_usage.rst, line 300.)
Todo
Give small example illustrating how drastic this can be.
(The original entry is located in /data2/autobuild/linux/gpuverify/Documentation/basic_usage.rst, line 400.)
Todo
Justify why it can be useful (performance)
(The original entry is located in /data2/autobuild/linux/gpuverify/Documentation/basic_usage.rst, line 402.)
Todo
is z3 available?
(The original entry is located in /data2/autobuild/linux/gpuverify/Documentation/trouble_shooting.rst, line 23.)
Todo
correct python version?
(The original entry is located in /data2/autobuild/linux/gpuverify/Documentation/trouble_shooting.rst, line 25.)
Todo
correct mono version if on Linux?
(The original entry is located in /data2/autobuild/linux/gpuverify/Documentation/trouble_shooting.rst, line 27.)
Todo
do you have write permission for the current directory?
(The original entry is located in /data2/autobuild/linux/gpuverify/Documentation/trouble_shooting.rst, line 29.)
Todo
Short circuit evaluation in invariants and pre-postcondition
(The original entry is located in /data2/autobuild/linux/gpuverify/Documentation/trouble_shooting.rst, line 31.)
Todo
Byte-level reads and writes
(The original entry is located in /data2/autobuild/linux/gpuverify/Documentation/trouble_shooting.rst, line 33.)