Commit 62de7356 authored by Julien Signoles's avatar Julien Signoles
Browse files

rename Lfunctions to Logic_functions

parent fff2359b
......@@ -80,7 +80,7 @@ PLUGIN_CMO:= local_config \
quantif \
at_with_lscope \
mmodel_translate \
lfunctions \
logic_functions \
translate \
temporal \
prepare_ast \
......
......@@ -33,8 +33,6 @@ keep_status.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
keep_status.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
label.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
label.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
lfunctions.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
lfunctions.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
license/CEA_LGPL: .ignore
license/LGPLv2.1: .ignore
license/SPARETIMELABS: .ignore
......@@ -43,6 +41,8 @@ literal_strings.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
literal_strings.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
local_config.ml: .ignore
local_config.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
logic_functions.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
logic_functions.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
loops.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
loops.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
lscope.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
......
......@@ -484,7 +484,7 @@ and context_insensitive_term_to_exp kf env t =
| Typing.C_type _ | Typing.Other -> Ctype (Typing.get_typ targ))
targs
in
Lfunctions.generate ~loc env t li (List.rev args) args_lty
Logic_functions.generate ~loc env t li (List.rev args) args_lty
in
e, env, false, "app"
| Tapp(_, _ :: _, _) ->
......@@ -875,9 +875,9 @@ let () =
At_with_lscope.predicate_to_exp_ref := named_predicate_to_exp;
Mmodel_translate.term_to_exp_ref := term_to_exp;
Mmodel_translate.predicate_to_exp_ref := named_predicate_to_exp;
Lfunctions.term_to_exp_ref := term_to_exp;
Lfunctions.predicate_to_exp_ref := named_predicate_to_exp;
Lfunctions.add_cast_ref := add_cast_lfunctions
Logic_functions.term_to_exp_ref := term_to_exp;
Logic_functions.predicate_to_exp_ref := named_predicate_to_exp;
Logic_functions.add_cast_ref := add_cast_lfunctions
(* This function is used by Guillaume.
However, it is correct to use it only in specific contexts. *)
......
......@@ -370,7 +370,7 @@ class e_acsl_visitor prj generate = object (self)
Cil.DoChildrenPost
(fun f ->
(* generate the C functions that correspond to the logic ones *)
Lfunctions.do_visit f;
Logic_functions.do_visit f;
(* extend [main] with forward initialization and put it at end *)
if generate then begin
if not (Global_observer.is_empty () && Literal_strings.is_empty ())
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment