From c110dec805d2f6aa8af93d8150ff9a658e9bb03e Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Thu, 20 Apr 2023 15:52:13 -0700 Subject: [PATCH] Minor doc fixes --- doc/cprover-manual/memory-primitives.md | 3 +-- .../contracts/doc/user/contracts-quantifiers.md | 2 +- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/doc/cprover-manual/memory-primitives.md b/doc/cprover-manual/memory-primitives.md index 984ecd093ac..350c72471ff 100644 --- a/doc/cprover-manual/memory-primitives.md +++ b/doc/cprover-manual/memory-primitives.md @@ -16,7 +16,7 @@ pointers as having 64 bits. This can be changed by various options (see section Memory is represented in CBMC as a set of objects. Each object represents a contiguous sequence of bytes and is identified via a numeric object ID. For -example, assuming integers of width 4 and chars of with 1, a global integer +example, assuming integers of width 4 and chars of width 1, a global integer variable would correspond to an object of size 4, and memory allocated via `malloc(10)` would correspond to an object of size 10. @@ -273,4 +273,3 @@ programs. 1 Pointers with negative offsets never point to memory objects. Negative values are used internally to detect pointer underflows. - diff --git a/src/goto-instrument/contracts/doc/user/contracts-quantifiers.md b/src/goto-instrument/contracts/doc/user/contracts-quantifiers.md index a384423747c..5f92757123a 100644 --- a/src/goto-instrument/contracts/doc/user/contracts-quantifiers.md +++ b/src/goto-instrument/contracts/doc/user/contracts-quantifiers.md @@ -16,7 +16,7 @@ While quantified expressions with arbitrary Boolean expressions are supported wi Concretely, with the SAT backend, the following syntax must be used for quantifiers: ``` -__CPROVER_forall { *id* *type*; *range* => *boolean expression* } +__CPROVER_forall { *id* *type*; *range* ==> *boolean expression* } __CPROVER_exists { *id* *type*; *range* && *boolean expression* } ```