From e676ab5c4960648c8fe4d529783ea0a6d7e13e4c Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@cea.fr>
Date: Wed, 15 Sep 2021 13:00:01 +0200
Subject: [PATCH] [e-acsl] rename problematic file
---
src/plugins/e-acsl/Makefile.in | 2 +-
src/plugins/e-acsl/headers/header_spec.txt | 4 ++--
.../e-acsl/src/code_generator/{genassigns.ml => assigns.ml} | 0
.../src/code_generator/{genassigns.mli => assigns.mli} | 0
src/plugins/e-acsl/src/code_generator/logic_functions.ml | 6 +++---
5 files changed, 6 insertions(+), 6 deletions(-)
rename src/plugins/e-acsl/src/code_generator/{genassigns.ml => assigns.ml} (100%)
rename src/plugins/e-acsl/src/code_generator/{genassigns.mli => assigns.mli} (100%)
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index bd124212bf6..7b2420d6b02 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -82,7 +82,7 @@ SRC_CODE_GENERATOR:= \
assert \
rational \
typed_number \
- genassigns \
+ assigns \
logic_functions \
loops \
quantif \
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index 1efa7e820b0..76a8d109b67 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -87,6 +87,8 @@ src/analyses/typing.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/analyses/typing.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/assert.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/assert.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/assigns.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/assigns.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/at_with_lscope.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/at_with_lscope.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/contract.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
@@ -94,8 +96,6 @@ src/code_generator/contract.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/contract_types.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/env.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/env.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/genassigns.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
-src/code_generator/genassigns.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/global_observer.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/global_observer.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/gmp.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
diff --git a/src/plugins/e-acsl/src/code_generator/genassigns.ml b/src/plugins/e-acsl/src/code_generator/assigns.ml
similarity index 100%
rename from src/plugins/e-acsl/src/code_generator/genassigns.ml
rename to src/plugins/e-acsl/src/code_generator/assigns.ml
diff --git a/src/plugins/e-acsl/src/code_generator/genassigns.mli b/src/plugins/e-acsl/src/code_generator/assigns.mli
similarity index 100%
rename from src/plugins/e-acsl/src/code_generator/genassigns.mli
rename to src/plugins/e-acsl/src/code_generator/assigns.mli
diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
index 746e6b1fb70..f81c8701aad 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -214,13 +214,13 @@ let generate_kf ~loc fname env ret_ty params_ty li =
List.fold_left2 add env li.l_profile params
in
let assigns_from =
- try Some (Genassigns.get_assigns_from ~loc env li.l_profile li.l_var_info)
- with Genassigns.NoAssigns -> None
+ try Some (Assigns.get_assigns_from ~loc env li.l_profile li.l_var_info)
+ with Assigns.NoAssigns -> None
in
let assigned_var =
Logic_const.new_identified_term
(if res_as_extra_arg then
- Logic_utils.expr_to_term (Genassigns.get_gmp_integer ~loc ret_vi)
+ Logic_utils.expr_to_term (Assigns.get_gmp_integer ~loc ret_vi)
else
Logic_const.tresult fundec.svar.vtype)
in
--
GitLab