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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/adr/homebrew-tap-instructions.html b/adr/homebrew-tap-instructions.html index 70c73def981..503026a9d25 100644 --- a/adr/homebrew-tap-instructions.html +++ b/adr/homebrew-tap-instructions.html @@ -131,7 +131,7 @@Last modified: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/adr/index.html b/adr/index.html index af1d6dc4267..422b312405a 100644 --- a/adr/index.html +++ b/adr/index.html @@ -76,7 +76,7 @@Last modified: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/adr/release-process.html b/adr/release-process.html index 83e97d0ac10..c5964b34f1a 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/adr/symex-ready-goto.html b/adr/symex-ready-goto.html index a9364ee0a17..1851e6c3fbd 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/api/index.html b/api/index.html index 56118a69390..4bec6fd751a 100644 --- a/api/index.html +++ b/api/index.html @@ -68,7 +68,7 @@Last modified: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
Last modified: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/assets/index.html b/assets/index.html index eef3d1ec459..2ea20f4c328 100644 --- a/assets/index.html +++ b/assets/index.html @@ -83,7 +83,7 @@Last modified: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/assets/md_xml_spec.html b/assets/md_xml_spec.html index 5814a9952b1..f26871ea175 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/background-concepts.html b/background-concepts.html index 698c0e8dc8b..98ea42c4cb4 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/cbmc-architecture.html b/cbmc-architecture.html index 537fddb347f..6f901a0ae84 100644 --- a/cbmc-architecture.html +++ b/cbmc-architecture.html @@ -132,7 +132,7 @@To be documented.
-Last modified: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/central-data-structures.html b/central-data-structures.html index 2386927c934..7337e7b6fca 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/classsimplify__exprt.html b/classsimplify__exprt.html index c1c587e66e5..2416fc4c6fd 100644 --- a/classsimplify__exprt.html +++ b/classsimplify__exprt.html @@ -1553,7 +1553,7 @@Definition at line 320 of file simplify_expr_boolean.cpp.
+Definition at line 324 of file simplify_expr_boolean.cpp.
diff --git a/code-walkthrough.html b/code-walkthrough.html index 80507272c93..a91528c12fd 100644 --- a/code-walkthrough.html +++ b/code-walkthrough.html @@ -129,7 +129,7 @@See analyses and pointer-analysis.
-Last modified: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/compilation-and-development.html b/compilation-and-development.html index 84cb9b0bebc..6d21197767a 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/contributing_documentation.html b/contributing_documentation.html index 43ee09d0392..7e2ca7979d4 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/cprover-manual/index.html b/cprover-manual/index.html index b1974a63da2..e9923c6a0e8 100644 --- a/cprover-manual/index.html +++ b/cprover-manual/index.html @@ -100,7 +100,7 @@Last modified: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/cprover-manual/md_api.html b/cprover-manual/md_api.html index 49766cbf9b9..e3c2213a284 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/cprover-manual/md_cbmc_assertions.html b/cprover-manual/md_cbmc_assertions.html index 40d205e2159..8f0864daefc 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/cprover-manual/md_cbmc_tutorial.html b/cprover-manual/md_cbmc_tutorial.html index 41d20dd007f..a245f37c44f 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/cprover-manual/md_cbmc_unwinding.html b/cprover-manual/md_cbmc_unwinding.html index 89445110cbb..d0e4ab5c3ed 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/cprover-manual/md_goto_analyzer.html b/cprover-manual/md_goto_analyzer.html index 3adbf014e92..e2ff2d4a8ae 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/cprover-manual/md_goto_cc.html b/cprover-manual/md_goto_cc.html index 5cdcaccd5f5..59bf447242c 100644 --- a/cprover-manual/md_goto_cc.html +++ b/cprover-manual/md_goto_cc.html @@ -160,7 +160,7 @@Last modified: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/cprover-manual/md_goto_harness.html b/cprover-manual/md_goto_harness.html index 8ad0c13f2ba..bd02f8d9107 100644 --- a/cprover-manual/md_goto_harness.html +++ b/cprover-manual/md_goto_harness.html @@ -399,7 +399,7 @@Last modified: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/cprover-manual/md_installation.html b/cprover-manual/md_installation.html index 33dc835697b..93bc86f296f 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/cprover-manual/md_introduction.html b/cprover-manual/md_introduction.html index 31155be7ec1..dd25c5d8be9 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/cprover-manual/md_jbmc_user_manual.html b/cprover-manual/md_jbmc_user_manual.html index 6444e218dbd..cbd75896ff9 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/cprover-manual/md_memory_primitives.html b/cprover-manual/md_memory_primitives.html index 2b295122b03..68e79621cca 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/cprover-manual/md_modeling_floating_point.html b/cprover-manual/md_modeling_floating_point.html index de9fd113f70..072cdb972ea 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/cprover-manual/md_modeling_mmio.html b/cprover-manual/md_modeling_mmio.html index 45ac55aed8d..63d4228144d 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/cprover-manual/md_modeling_nondeterminism.html b/cprover-manual/md_modeling_nondeterminism.html index f3b67d86eb0..e76a929cd23 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/cprover-manual/md_modeling_pointers.html b/cprover-manual/md_modeling_pointers.html index 9837a877e7a..806e7819e0a 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/cprover-manual/md_properties.html b/cprover-manual/md_properties.html index bc8a8b76e90..20fc623f962 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/cprover-manual/md_smt2_incr.html b/cprover-manual/md_smt2_incr.html index b09e5df5acc..c4c8ecb9e34 100644 --- a/cprover-manual/md_smt2_incr.html +++ b/cprover-manual/md_smt2_incr.html @@ -209,7 +209,7 @@Last modified: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/cprover-manual/md_static_functions.html b/cprover-manual/md_static_functions.html index da65678577e..f3a7365d968 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/cprover-manual/md_test_suite.html b/cprover-manual/md_test_suite.html index f9c9beca231..4895bfd9a78 100644 --- a/cprover-manual/md_test_suite.html +++ b/cprover-manual/md_test_suite.html @@ -212,7 +212,7 @@__CPROVER_cover statement Last modified: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/cprover-manual/md_unsound_options.html b/cprover-manual/md_unsound_options.html index f010925a99c..e6d9e1de3b3 100644 --- a/cprover-manual/md_unsound_options.html +++ b/cprover-manual/md_unsound_options.html @@ -105,7 +105,7 @@Last modified: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/cprover-manual/md_visual_studio.html b/cprover-manual/md_visual_studio.html index a6ccd2b5bbf..b6bb56726f1 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/cprover-manual/shadow-memory.html b/cprover-manual/shadow-memory.html index bf0355d0b6b..a92a731c3f3 100644 --- a/cprover-manual/shadow-memory.html +++ b/cprover-manual/shadow-memory.html @@ -232,7 +232,7 @@Last modified: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/developer_guide.html b/developer_guide.html index 4778cc5f5e9..d183050c151 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/folder-walkthrough.html b/folder-walkthrough.html index b23e4a29bad..e484a2381c1 100644 --- a/folder-walkthrough.html +++ b/folder-walkthrough.html @@ -166,7 +166,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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/goto-program-transformations.html b/goto-program-transformations.html index 833b6e52dc8..d78e2e6f900 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 &) function.
Predecessor pass is Label Properties .
-Last modified: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/group__module__hidden.html b/group__module__hidden.html index 387eacadce6..081ef89b8fa 100644 --- a/group__module__hidden.html +++ b/group__module__hidden.html @@ -92,7 +92,7 @@Last modified: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
Last modified: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
The CBMC release page gives instructions for installing CBMC on MacOS, Ubuntu, Windows, and Docker.
-Last modified: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/memory-bounds-checking.html b/memory-bounds-checking.html index d0b95374e72..35e9a0a0350 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/other-tools.html b/other-tools.html index 9b4b134a46a..db4977fc121 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/reference_guide.html b/reference_guide.html index b9f82c6c8c6..811ea7ff655 100644 --- a/reference_guide.html +++ b/reference_guide.html @@ -109,7 +109,7 @@Last modified: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/satabs.html b/satabs.html index 52986bcf256..07aca33f285 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/simplify__expr_8cpp_source.html b/simplify__expr_8cpp_source.html index c74169eacff..0e254aa2fa6 100644 --- a/simplify__expr_8cpp_source.html +++ b/simplify__expr_8cpp_source.html @@ -3379,7 +3379,7 @@Last modified: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100
diff --git a/user_guide.html b/user_guide.html index e09893fcd55..6066bc159ae 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: 2023-10-11 20:45:19 +0100
+Last modified: 2023-10-12 11:36:32 +0100