We are working towards addressing these teething problems, but while we are still operating on those, we have to accept some compromises in the architecture of the code while we are iterating or stabilising several of the new or refactored parts.
Be advised that some constructs may pop up in some limited locations in the codebase that may appear questionable. We are only asking for some patience while we are working out the best way to refactor them into an architecture that is more cohesive with the long term vision for the platform.
From our end, we will do our best to avoid any spillover effects to other areas of the codebase, and to avoid introducing any behavioural regressions while we are implementing the above plan. Any constructs that may feature "questionable" changes to parts will be marked as such and be followed with an explanation as to why the decision was made.
-Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/adr/homebrew-tap-instructions.html b/adr/homebrew-tap-instructions.html index 45df00a3785..7542c086ab6 100644 --- a/adr/homebrew-tap-instructions.html +++ b/adr/homebrew-tap-instructions.html @@ -131,7 +131,7 @@Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/adr/index.html b/adr/index.html index f4b1abd3d72..d9f63e8fbc7 100644 --- a/adr/index.html +++ b/adr/index.html @@ -76,7 +76,7 @@Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/adr/release-process.html b/adr/release-process.html index 6f432ffee67..66f493aca1d 100644 --- a/adr/release-process.html +++ b/adr/release-process.html @@ -111,7 +111,7 @@Originally we wanted to automate this part, but we were limited by the fact that we needed to update src/config.inc before doing the release, and that couldn't be done in an automated fashion, as any update needs to go through a PR, and gets stuck on code-owners approvals, making the whole process more manual than intended.
Following this original limitation, we decided to settle on doing manual releases every two weeks, but having the process being initiated by a developer manually making the change to src/config.inc, and after that has been merged, mark that specific commit as with a version tag, and push that version tag to Github. At that point, the rest of the process is automated.
The change to the current implementation was part of https://github.com/diffblue/cbmc/pull/5517.
-Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/adr/symex-ready-goto.html b/adr/symex-ready-goto.html index 500de9b8f60..67d006f2c51 100644 --- a/adr/symex-ready-goto.html +++ b/adr/symex-ready-goto.html @@ -81,7 +81,7 @@stop_on_fail_verifier_with_fault_localizationt,stop_on_fail_verifiert.Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/api/index.html b/api/index.html index 8e49db62817..b2ab873274c 100644 --- a/api/index.html +++ b/api/index.html @@ -68,7 +68,7 @@Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/assets/index.html b/assets/index.html index 732c9332edc..03934d3ae96 100644 --- a/assets/index.html +++ b/assets/index.html @@ -83,7 +83,7 @@Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/assets/md_xml_spec.html b/assets/md_xml_spec.html index 87cdddf15ff..2c1e1e36811 100644 --- a/assets/md_xml_spec.html +++ b/assets/md_xml_spec.html @@ -410,7 +410,7 @@SSA steps are sorted by clocks and the following steps are skipped: PHI, GUARD assignments; shared-read, shared-write, constraint, spawn, atomic-begin, atomic-end.
-Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/background-concepts.html b/background-concepts.html index 85ca90f401f..150930b3bd3 100644 --- a/background-concepts.html +++ b/background-concepts.html @@ -624,7 +624,7 @@In the CPROVER framework, the term verification condition is used in a somewhat non-standard way. Let a program and a set of assertions be given. We transform the program into an (acyclic) SSA (i.e., an SSA with all loops unrolled a finite number of times) and turn it into a logical formula, as described above. Note that in this case, the formula will also contain information about what the program does after the assertion is reached: this part of the formula, is, in fact, irrelevant for deciding whether the program can satisfy the assertion or not. The verification condition is the part of the formula that only covers the program execution until the line that checks the assertion has been executed, with everything that comes after it removed.
-Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/cbmc-architecture.html b/cbmc-architecture.html index 3c64be7d432..6082745cbb7 100644 --- a/cbmc-architecture.html +++ b/cbmc-architecture.html @@ -132,7 +132,7 @@To be documented.
-Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/central-data-structures.html b/central-data-structures.html index e74ee5f3581..4bc7d333710 100644 --- a/central-data-structures.html +++ b/central-data-structures.html @@ -157,7 +157,7 @@ireps are the underlying data structure used to implement many of the data structures in CBMC and the assorted tools. These include the exprt, typet, codet and source_locationt classes. This is a tree data structure where each node is expected to contain a string/ID and may have child nodes stored in both a sequence of child nodes and a map of strings/IDs to child nodes. This enables the singular irept data structure to be used to model graphs such as ASTs, CFGs, etc.
The classes extending irept define how the higher level concepts are mapped onto the underlying tree data structure. For this reason it is usually advised that the member functions of the sub-classes should be used to access the data held, rather than the member functions of the base irept class. This aids potential future restructuring and associates accesses of the data with the member functions which have the doxygen explaining what the data is.
The strings/IDs held within irept are of type irep_idt. These can be converted to std::string using the id2string function. There is a mechanism provided for casting expressions and types in src/util/expr_cast.h. In depth documentation of the irept class itself can be found in src/util/irep.h.
Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/code-walkthrough.html b/code-walkthrough.html index 331cf5c9b52..3c92214e9e4 100644 --- a/code-walkthrough.html +++ b/code-walkthrough.html @@ -129,7 +129,7 @@See analyses and pointer-analysis.
-Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/compilation-and-development.html b/compilation-and-development.html index 50efabb2787..1df480fe848 100644 --- a/compilation-and-development.html +++ b/compilation-and-development.html @@ -182,7 +182,7 @@gprof <path-to-binary> <path-to-gmon.out> and redirect the output to a file. This will take a while to run - e.g. 12 minutes for test-gen run on a trivial function.
The output file will now be a large text file. There are two sections: the "flat profile", which ignores context, and just tells you how much time was spent in each function; and the "call graph", which includes context, and tells you how much time was spent within each call stack. For more information see online tutorials, like https://ftp.gnu.org/old-gnu/Manuals/gprof-2.9.1/html_chapter/gprof_5.html
-Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/contributing_documentation.html b/contributing_documentation.html index 88f4293d48f..7e783fcd07c 100644 --- a/contributing_documentation.html +++ b/contributing_documentation.html @@ -100,7 +100,7 @@When you contribute a module mymodule.c to the source code, there are probably at least two kinds of documentation you want to contribute. One is user documentation to help people use your feature. One is developer documentation to help people debug or extend your work. We recommend that you put files mymodule-user.md and mymodule-developer.md next to mymodule.c in the repository. Then you can use the \page and \subpage mechanism described above into the appropriate parts of the user guide and developer guide.
When you contribute documentation, it may not be clear whether it should go into the user guide or the developer guide. We recommend that you put into the user guide everything a user needs to know to use the tool. For example, put a description of the CBMC memory model into the user guide. Then the developer guide can link to that description of the memory model in the user guide, and say, "This is the memory model, and this is how we implement the memory model."
-Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/cprover-manual/index.html b/cprover-manual/index.html index 7ae2cad85b6..9ade97bf8b0 100644 --- a/cprover-manual/index.html +++ b/cprover-manual/index.html @@ -100,7 +100,7 @@Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/cprover-manual/md_api.html b/cprover-manual/md_api.html index 0135ac189e0..168dcebd924 100644 --- a/cprover-manual/md_api.html +++ b/cprover-manual/md_api.html @@ -240,7 +240,7 @@Asynchronous threads are created by preceding an instruction with a label with the prefix **__CPROVER_ASYNC_**.
-Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/cprover-manual/md_cbmc_assertions.html b/cprover-manual/md_cbmc_assertions.html index c99aabab44d..8e7929605c7 100644 --- a/cprover-manual/md_cbmc_assertions.html +++ b/cprover-manual/md_cbmc_assertions.html @@ -103,7 +103,7 @@Future CPROVER releases will support explicit quantifiers with a syntax that resembles Spec#:
Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/cprover-manual/md_cbmc_tutorial.html b/cprover-manual/md_cbmc_tutorial.html index 8bbe2800091..e556b9cca2e 100644 --- a/cprover-manual/md_cbmc_tutorial.html +++ b/cprover-manual/md_cbmc_tutorial.html @@ -220,7 +220,7 @@We also have a list of interesting applications of CBMC.
-Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/cprover-manual/md_cbmc_unwinding.html b/cprover-manual/md_cbmc_unwinding.html index b17b65d7084..fa33fca4a2d 100644 --- a/cprover-manual/md_cbmc_unwinding.html +++ b/cprover-manual/md_cbmc_unwinding.html @@ -147,7 +147,7 @@The loop-based unwinding bound is not always appropriate. In particular, it is often difficult to control the size of the generated formula when using the --unwind option. The option:
--depth nr
specifies an unwinding bound in terms of the number of instructions that are executed on a given path, irrespective of the number of loop iterations. Note that CBMC uses the number of instructions in the control-flow graph as the criterion, not the number of instructions in the source code.
-Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/cprover-manual/md_goto_analyzer.html b/cprover-manual/md_goto_analyzer.html index bff5b79c96c..6df16152879 100644 --- a/cprover-manual/md_goto_analyzer.html +++ b/cprover-manual/md_goto_analyzer.html @@ -150,7 +150,7 @@goto-analyzer supports a number of other options for the C/C++ frontend, the platform, displaying program representations and instrumentation. These all function exactly the same as CBMC does.
It also supports specific analyses which do not fit into the configurable scheme above. At the time of writing this is just --taint which performs a configurable taint analysis.
Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/cprover-manual/md_goto_cc.html b/cprover-manual/md_goto_cc.html index 4e0cdbad868..ed43f38fae9 100644 --- a/cprover-manual/md_goto_cc.html +++ b/cprover-manual/md_goto_cc.html @@ -158,7 +158,7 @@Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/cprover-manual/md_goto_harness.html b/cprover-manual/md_goto_harness.html index e04d85935f0..cc2dfb24768 100644 --- a/cprover-manual/md_goto_harness.html +++ b/cprover-manual/md_goto_harness.html @@ -399,7 +399,7 @@Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/cprover-manual/md_installation.html b/cprover-manual/md_installation.html index ea831fb2ecc..2a745df2104 100644 --- a/cprover-manual/md_installation.html +++ b/cprover-manual/md_installation.html @@ -97,7 +97,7 @@The installation instructions for the Eclipse Plugin, including the link to the download site, are available here. This includes a short tutorial on the Eclipse plugin.
-Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/cprover-manual/md_introduction.html b/cprover-manual/md_introduction.html index 81d4ccc3a67..e0edf1cf376 100644 --- a/cprover-manual/md_introduction.html +++ b/cprover-manual/md_introduction.html @@ -82,7 +82,7 @@CBMC implements a technique called Bounded Model Checking (BMC). In BMC, the transition relation for a complex state machine and its specification are jointly unwound to obtain a Boolean formula, which is then checked for satisfiability by using an efficient SAT procedure. If the formula is satisfiable, a counterexample is extracted from the output of the SAT procedure. If the formula is not satisfiable, the program can be unwound more to determine if a longer counterexample exists.
In many engineering domains, real-time guarantees are a strict requirement. An example is software embedded in automotive controllers. As a consequence, the loop constructs in these types of programs often have a strict bound on the number of iterations. CBMC is able to formally verify such bounds by means of unwinding assertions. Once this bound is established, CBMC is able to prove the absence of errors.
A more detailed description of how to apply CBMC to verify programs is in our CBMC Tutorial.
-Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/cprover-manual/md_jbmc_user_manual.html b/cprover-manual/md_jbmc_user_manual.html index 8e0a4e61810..54a68229d1d 100644 --- a/cprover-manual/md_jbmc_user_manual.html +++ b/cprover-manual/md_jbmc_user_manual.html @@ -196,7 +196,7 @@JBMC has a wealth of other options that can either constrain the model (to cope with complexity issues), or output more relevant information. The list of all available options is printed by running:
$ jbmc --help -
Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/cprover-manual/md_memory_primitives.html b/cprover-manual/md_memory_primitives.html index e154576eac7..90a4271aed0 100644 --- a/cprover-manual/md_memory_primitives.html +++ b/cprover-manual/md_memory_primitives.html @@ -182,7 +182,7 @@When an assert(false) statement before the assume has the property status SATISFIED, but is followed by an assert(false) statement after the assume statement that has status FAILED, this is an indication that this specific assume statement (on the line reported) is one that is emptying the search space for model checking.
Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/cprover-manual/md_modeling_floating_point.html b/cprover-manual/md_modeling_floating_point.html index 7943c9b70fb..fa34e1d3d7d 100644 --- a/cprover-manual/md_modeling_floating_point.html +++ b/cprover-manual/md_modeling_floating_point.html @@ -92,7 +92,7 @@CPROVER also has support for fixed-point types. The --fixedbv flag switches float, double, and long double to fixed-point types. The length of these types is platform specific. The upper half of each type is the integer component and the lower half is the fractional part.
Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/cprover-manual/md_modeling_mmio.html b/cprover-manual/md_modeling_mmio.html index 9f642c8e813..290af757ef7 100644 --- a/cprover-manual/md_modeling_mmio.html +++ b/cprover-manual/md_modeling_mmio.html @@ -89,7 +89,7 @@will return the value 2 upon any access at address 0x1000, and return a non-deterministic value in all other cases.
-Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/cprover-manual/md_modeling_nondeterminism.html b/cprover-manual/md_modeling_nondeterminism.html index 144395f33a0..f9847141cee 100644 --- a/cprover-manual/md_modeling_nondeterminism.html +++ b/cprover-manual/md_modeling_nondeterminism.html @@ -89,7 +89,7 @@It may be necessary to check parts of a program independently. Nondeterminism can be used to over-approximate the behavior of a part of the system which is not being checked. Rather than calling a complex or unrelated function, a nondeterministic stub is used. However, separate calls to the function can return different results, even for the same inputs.
If the function output only depends on its inputs, this can introduce spurious errors. To avoid this problem, functions whose names begin with the prefix __CPROVER_uninterpreted_ are treated as uninterpreted functions. Their value is non-deterministic but different invocations will return the same value if their inputs are the same. Note that uninterpreted functions are not supported by all back-end solvers.
Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/cprover-manual/md_modeling_pointers.html b/cprover-manual/md_modeling_pointers.html index efccc816583..e98f6c29ef6 100644 --- a/cprover-manual/md_modeling_pointers.html +++ b/cprover-manual/md_modeling_pointers.html @@ -95,7 +95,7 @@It is frequently desired to validate an open program (a fragment of a program). Some variables are left undefined. When an undefined pointer is dereferenced, CBMC assumes that the pointer points to a separate object of appropriate type with unbounded size. The object is assumed not to alias with any other object. This assumption may obviously be wrong in specific extensions of the program.
-Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/cprover-manual/md_properties.html b/cprover-manual/md_properties.html index b633d105474..e5dda0b044c 100644 --- a/cprover-manual/md_properties.html +++ b/cprover-manual/md_properties.html @@ -302,7 +302,7 @@Note that no attempt to follow the next pointer is made. If an array of unknown (or 0) size is encountered, a diagnostic is emitted and the array is not further examined.
Some care must be taken when choosing the regular expressions for globals and functions. Names starting with __ are reserved for internal purposes; For example, replacing functions or setting global variables with the __CPROVER prefix might make analysis impossible. To avoid doing this by accident, negative lookahead can be used. For example, (?!__).* matches all names not starting with __.
Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/cprover-manual/md_smt2_incr.html b/cprover-manual/md_smt2_incr.html index 4b61c6f4b73..eb2a93462ca 100644 --- a/cprover-manual/md_smt2_incr.html +++ b/cprover-manual/md_smt2_incr.html @@ -209,7 +209,7 @@Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/cprover-manual/md_static_functions.html b/cprover-manual/md_static_functions.html index b49158e4171..29fbde51c9f 100644 --- a/cprover-manual/md_static_functions.html +++ b/cprover-manual/md_static_functions.html @@ -153,7 +153,7 @@ The solution is to use the --mangle-suffix option to goto-cc. This allows you to specify a different suffix for name-mangling. By specifying a custom, different suffix for each of the two files, the mangled names are unique and the files can be successfully linked.
More examples are in regression/goto-cc-file-local.
Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/cprover-manual/md_test_suite.html b/cprover-manual/md_test_suite.html index 2c83b9e3629..7803ebe4511 100644 --- a/cprover-manual/md_test_suite.html +++ b/cprover-manual/md_test_suite.html @@ -212,7 +212,7 @@__CPROVER_cover statement Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/cprover-manual/md_unsound_options.html b/cprover-manual/md_unsound_options.html index a0bd0ceea10..62d255ff0a2 100644 --- a/cprover-manual/md_unsound_options.html +++ b/cprover-manual/md_unsound_options.html @@ -106,7 +106,7 @@Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/cprover-manual/md_visual_studio.html b/cprover-manual/md_visual_studio.html index aad3de5b27b..3751eddf685 100644 --- a/cprover-manual/md_visual_studio.html +++ b/cprover-manual/md_visual_studio.html @@ -79,7 +79,7 @@Note that the recent versions of goto-cc also support file names with non-ASCII (Unicode) characters on Windows platforms.
-Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/cprover-manual/shadow-memory.html b/cprover-manual/shadow-memory.html index 67c3f146ad7..26660ba6db9 100644 --- a/cprover-manual/shadow-memory.html +++ b/cprover-manual/shadow-memory.html @@ -232,7 +232,7 @@Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/developer_guide.html b/developer_guide.html index ed38e08a9b7..fdcdf264345 100644 --- a/developer_guide.html +++ b/developer_guide.html @@ -116,7 +116,7 @@Please contribute documentation when you find mistakes or missing information to help us improve this developer guide.
-Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/folder-walkthrough.html b/folder-walkthrough.html index 4c6f4d5e272..6f933100006 100644 --- a/folder-walkthrough.html +++ b/folder-walkthrough.html @@ -164,7 +164,7 @@There are module_dependencies.txt files in each directory, which are checked by the linter. Where directories in module_dependencies.txt are marked with comments such as 'dubious' or 'should go away', these dependencies have generally not been included in the diagram.
Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/goto-program-transformations.html b/goto-program-transformations.html index 7bd57f498f8..d405d5324c8 100644 --- a/goto-program-transformations.html +++ b/goto-program-transformations.html @@ -214,7 +214,7 @@This includes several slicing passes as specified by various slicing command line options. The reachability slicer is enabled by the --reachability-slice command line option. The implementation of this pass is called via the reachability_slicer(goto_modelt &, message_handlert &) function. The full slicer is enabled by the --full-slice command line option. The implementation of this pass is called via the full_slicer(goto_modelt &, message_handlert &) function.
Predecessor pass is Label Properties .
-Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/group__module__hidden.html b/group__module__hidden.html index 6b4768d6850..1eea56c8ed6 100644 --- a/group__module__hidden.html +++ b/group__module__hidden.html @@ -92,7 +92,7 @@Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
The CBMC release page gives instructions for installing CBMC on MacOS, Ubuntu, Windows, and Docker.
-Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
The way the goto-symex subfolder is structured, the different dispatching functions are usually in their own file, designated by the instruction's name. As an example, you can find the code for the function goto_symext::symex_goto in symex_goto.cpp
The output of symex is an symex_target_equationt which consists of equalities between different expressions in the program. You can visualise it as a data structure that serialises to this: (a = 5 ∨ a = 3) ∧ (b = 3) ∧ (c = 4) ∧ ... that describe assignments and conditions for a range of possible executions of a program that cover a range of potential paths within it.
This is a high-level overview of symex and goto-program instructions. For more information (and a more robust introduction), please have a look at Symbolic Execution.
-Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/memory-bounds-checking.html b/memory-bounds-checking.html index 9e6f3d92114..5a73b0fc69c 100644 --- a/memory-bounds-checking.html +++ b/memory-bounds-checking.html @@ -120,7 +120,7 @@Here the verification condition generated for the pointer dereference should fail: for p1 in *p1, __CPROVER_POINTER_OFFSET will evaluate to 1 (owing to the increment p1++, and __CPROVER_OBJECT_SIZE will also evaluate to 1. Consequently, the less-than comparison in the verification condition evaluates to false.
Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/other-tools.html b/other-tools.html index e71b5da4a1d..fb945e5cd85 100644 --- a/other-tools.html +++ b/other-tools.html @@ -130,7 +130,7 @@DeltaCheck?: Ajitha’s slicing tool, aimed at locating changes and differential verification. In the old project CVS.There are tools based on the CPROVER framework from other research groups which are not listed here.
-Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/reference_guide.html b/reference_guide.html index 3405231d53e..3ab0a8ef5f1 100644 --- a/reference_guide.html +++ b/reference_guide.html @@ -109,7 +109,7 @@Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/satabs.html b/satabs.html index 18fc11eaa80..6e7e73b5e80 100644 --- a/satabs.html +++ b/satabs.html @@ -348,7 +348,7 @@ SATABS runs for quite a while and will eventually give up, telling us that its upper bound for abstraction refinement iterations has been exceeded. This is not exactly the result we were hoping for, and we could now increase the bound for iterations with help of the --iterations command line switch of SATABS.
Before we do this, let us investigate why SATABS has failed to provide a useful result. The function strcpy contains a loop that counts from 1 to the length of the input string. Predicate abstraction, the mechanism SATABS is based on, is unable to detect such loops and will therefore unroll the loop body as often as necessary. The array home has MAX_LEN elements, and MAX_LEN is defined to be 512 in aeon.h. Therefore, SATABS would have to run through at least 512 iterations, only to verify (or reject) one of the more than 300 properties! Does this fact defeat the purpose of static verification?
We can make the job easier: after reducing the value of MAX_LEN in aeon.h to a small value, say to 10, SATABS provides a counterexample trace that demonstrates how the buffer overflow be reproduced. If you use the Eclipse plugin (as described here), you can step through this counterexample. The trace contains the string that is returned by getenv.
Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/tutorial.html b/tutorial.html index f4a168a776d..fb13a1ae4e0 100644 --- a/tutorial.html +++ b/tutorial.html @@ -192,7 +192,7 @@Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700
diff --git a/user_guide.html b/user_guide.html index 6512a832e76..62503b0b125 100644 --- a/user_guide.html +++ b/user_guide.html @@ -117,7 +117,7 @@Please contribute documentation when you find mistakes or missing information to help us improve this user guide.
-Last modified: 2024-09-29 16:08:10 -0400
+Last modified: 2024-10-22 05:58:08 -0700