[dev] suggested changes

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

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);

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

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

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:
-*)

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;