From 3d0d4411eb95ab42eb4ec7bcb06fdd30b583d568 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 18 Sep 2024 14:42:30 +0000
Subject: [PATCH] [dev] suggested changes
---
doc/developer/advance.tex | 2 +-
src/kernel_internals/parsing/logic_lexer.mll | 5 ++++-
src/kernel_internals/parsing/logic_parser.mly | 6 ++++++
src/kernel_services/ast_queries/ast_diff.ml | 2 ++
src/kernel_services/ast_queries/cil_const.ml | 5 -----
src/kernel_services/ast_queries/logic_typing.mli | 2 +-
6 files changed, 14 insertions(+), 8 deletions(-)
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index b2d55d76a2..6474f804b2 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -4139,7 +4139,7 @@ The syntax is similar to the general ACSL \verb+import+ annotation, except that
module name is prefixed with the name of the loader extension. For instance:
\begin{lstlisting}[style=c]
-//@ \import Foo: foo::bar::Jazz ;
+//@ import Foo: foo::bar::Jazz ;
\end{lstlisting}
Here, \verb+Foo:+ specifies the name of the \acsl extension responsible for
diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index 61e3a74536..23eec9c8a0 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -114,7 +114,10 @@
"assert", (fun _ -> ASSERT);
"assigns", (fun _ -> ASSIGNS);
"assumes", (fun _ -> ASSUMES);
- "at", (fun _ -> EXT_SPEC_AT);
+ "at",
+ (fun _ ->
+ if !ext_acsl_spec then EXT_SPEC_AT
+ else IDENTIFIER "at");
"axiom", (fun _ -> AXIOM);
"axiomatic", (fun _ -> AXIOMATIC);
"behavior", (fun _ -> BEHAVIOR);
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 83b6fdab5f..ce9c3e2bed 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -567,6 +567,12 @@ lexpr_inner:
| INTER LPAR lexpr_list RPAR { info $sloc (PLinter $3) }
| LBRACE RBRACE
{ info $sloc (PLset []) }
+/* because LONGIDENT can be both a type name or a plain identifier,
+ we can't have a full lexpr here, as there would be an ambiguity
+ in { x | a::b * ...: should a::b be considered as a type (hence
+ we are parsing a comprehension with a binder), or an identifier
+ (hence, we are still parsing an lexpr).
+*/
| LBRACE lexpr_inner RBRACE
{ info $sloc (PLset [$2]) }
| LBRACE lexpr_inner COMMA lexpr_list RBRACE
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index 7fe9adc6ec..7a92019e1c 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -1519,6 +1519,8 @@ let rec gannot_correspondence =
| Daxiomatic(_,l,_,_) | Dmodule(_,l,_,_,_) ->
List.iter gannot_correspondence l
+ (* TODO: for modules, we should check the driver if it exists. But like
+ for lemmas, we don't have an appropriate structure to store the info *)
| Dtype (ti,loc) -> ignore (logic_type_correspondence ~loc ti empty_env)
| Dlemma _ -> ()
(* TODO: we currently do not have any appropriate structure for
diff --git a/src/kernel_services/ast_queries/cil_const.ml b/src/kernel_services/ast_queries/cil_const.ml
index 7bde413189..20033aed2b 100644
--- a/src/kernel_services/ast_queries/cil_const.ml
+++ b/src/kernel_services/ast_queries/cil_const.ml
@@ -193,8 +193,3 @@ let make_logic_type name = {
lt_attr = [] ;
}
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index 41a8bbb82b..aa049e08e0 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -91,7 +91,7 @@ type logic_infos =
(** Functions that can be called when type-checking an extension of ACSL.
- @before Frama-C+dev The following fields have been removed:
+ @before Frama-C+dev The following fields were present:
{[
remove_logic_function : string -> unit;
--
GitLab