diff options
| author | Son Ho | 2022-04-21 12:56:53 +0200 | 
|---|---|---|
| committer | Son Ho | 2022-04-21 12:56:53 +0200 | 
| commit | 86b05d3b39c978c3d3c33868e3846990defe61e9 (patch) | |
| tree | 3236cc165efca3b903a74feacfdd9f398472ab1e /src/PrintPure.ml | |
| parent | 0f2ce5dd56dc1001d5ba7128e6f0ac83ea499267 (diff) | |
Make minor modifications
Diffstat (limited to 'src/PrintPure.ml')
| -rw-r--r-- | src/PrintPure.ml | 6 | 
1 files changed, 5 insertions, 1 deletions
| diff --git a/src/PrintPure.ml b/src/PrintPure.ml index 1c3d396d..8344ee41 100644 --- a/src/PrintPure.ml +++ b/src/PrintPure.ml @@ -226,7 +226,11 @@ let rec projection_to_string (fmt : ast_formatter) (inside : string)  let mplace_to_string (fmt : ast_formatter) (p : mplace) : string =    let name = match p.name with None -> "" | Some name -> name in -  let name = name ^ "^" ^ V.VarId.to_string p.var_id in +  (* We add the "llbc" suffix to the variable index, because meta-places +   * use indices of the variables in the original LLBC program, while +   * regular places use indices for the pure variables: we want to make +   * this explicit, otherwise it is confusing. *) +  let name = name ^ "^" ^ V.VarId.to_string p.var_id ^ "llbc" in    projection_to_string fmt name p.projection  let place_to_string (fmt : ast_formatter) (p : place) : string = | 
