From 9a8649cc9f67b8a9ccde2e91e7fc428308f4ecc3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lb@leliobrun.net>
Date: Wed, 1 Mar 2023 19:12:02 +0900
Subject: [PATCH] allow renaming variables named 'set' in ghost declarations
---
src/backends/C/c_backend_spec.ml | 6 ++++--
1 file changed, 4 insertions(+), 2 deletions(-)
diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index e05efb06..ac33eed2 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -1928,7 +1928,9 @@ let sanitize_expr = function
let sanitize_predicate = function
| Transition (st, f, inst, i, vs, r, mf, mfinsts) ->
Transition (st, f, inst, i, List.map sanitize_expr vs, r, mf, mfinsts)
- | p ->
+ | GhostAssign (x, v) ->
+ GhostAssign (sanitize_var_decl x, sanitize_value v)
+ | (Reset _ | MemoryPack _ | MemoryPackBase _) as p ->
p
let rec sanitize_formula = function
@@ -1954,7 +1956,7 @@ let rec sanitize_formula = function
ExistsMem (m, sanitize_formula f1, sanitize_formula f2)
| Value v ->
Value (sanitize_value v)
- | f ->
+ | (True | False | StateVarPack _ | MemoryPackToplevel _) as f ->
f
and sanitize_formulae fs = List.map (fun spec -> sanitize_formula spec) fs
--
GitLab