diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt index b8d2e280542e4eac9613125cd9c987eed033eb6e..3daf5993839c6a94719a95604afacee9328db77c 100644 --- a/src/plugins/e-acsl/headers/header_spec.txt +++ b/src/plugins/e-acsl/headers/header_spec.txt @@ -76,8 +76,8 @@ src/analyses/interval.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/analyses/interval.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/analyses/literal_strings.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/analyses/literal_strings.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL -src/analyses/predicate_normalizer.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL -src/analyses/predicate_normalizer.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL +src/analyses/logic_normalizer.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL +src/analyses/logic_normalizer.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/analyses/lscope.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/analyses/lscope.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/analyses/memory_tracking.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml index 95c9189b0e62dc9954a7b1d94137f3f211996b60..bbc74b118c622dbc23942b3409e8622ba3f86773 100644 --- a/src/plugins/e-acsl/src/analyses/typing.ml +++ b/src/plugins/e-acsl/src/analyses/typing.ml @@ -416,8 +416,8 @@ let rec type_term | TSizeOfStr _ | TAlignOf _ -> let i = Interval.infer t in - (* a constant or an left value directly under a lambda should be a gmp - if the infered context for the lambda is gmp *) + (* a constant or a left value directly under a lambda should be a gmp + if the infered context for the lambda is gmp *) let ty = ty_of_interv ?ctx ~use_gmp_opt:under_lambda i in dup ty