diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in index bd124212bf67ea3dce1d4b1e8378e7962599e882..7b2420d6b02530f46fb77977c79d80e1af87a99f 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 1efa7e820b032eca0492f981d46126dca085661e..76a8d109b67ecb592a40905b096765f04af808e0 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 746e6b1fb7070c737c2564a0da829b24d5a3a6f2..f81c8701aad1a93b61e4ff08f0ce7e38d9b4d10e 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