diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml index be5c827b90ec3f24e3731f57629334ef66557946..14660db121ee6b83878b883344b8d5a1abbd7a4f 100644 --- a/src/plugins/wp/MemRegion.ml +++ b/src/plugins/wp/MemRegion.ml @@ -487,9 +487,9 @@ type loc = | Lfld of region * index * F.term * region overlay | Larr of region * index * F.term * F.term list * int * int list (* For Lxxx locations: - - index: start index inside the chunk - - term: additional shift index - - term list: array index from start *) + - index: start index inside the chunk + - term: additional shift index + - term list: array index from start *) (* -------------------------------------------------------------------------- *) (* --- Loc Basics --- *)