diff --git a/Changelog b/Changelog
index 478dd8edf059309754ecfc9d2a7a635c8090a58a..c1b67abf0b0f40a3056a28457e74e6b9d5accf65 100644
--- a/Changelog
+++ b/Changelog
@@ -56,6 +56,9 @@ Open Source Release 29.0 (Copper)
use array > SIZE_MAX by changing its status (default is error).
- Eva [2024-04-26] Improve builtins memcpy, memmove and memset when
arguments are imprecise.
+- Kernel [2024-04-22] Support for ACSL modules.
+o! Dev [2024-04-22] Move functions for finding logic types, functions,
+ predicates and constructors from Logic_typing to Logic_env.
o Dev [2024-04-22] Remove frama-c-build-scripts.sh; add a section in
the user manual about how to manually replace it.
-! Kernel [2024-04-19] Change format of custom_defs field in machdep schema
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 0858a650b5b9ed5ab10b845468d977b3f62b5b82..6474f804b2d7876369e55c274f7b676670cd69f1 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -3910,15 +3910,20 @@ different flavors, determined by the \scodeidx{Cil\_types}{ext\_code\_annot\_con
An extension is characterized by its introducing keyword \texttt{kw}, or
\texttt{loop kw} for a loop extension. Having the same keyword for two distinct
extensions is not possible, especially if they belong to different categories,
-as this would lead to ambiguities in the parser. It is advised to prefix the
+as this would lead to ambiguities in the parser.
+
+Moreover, when writing extended ACSL annotations, it is advised to prefix the
keyword with the plug-in that registers it, for example
-\lstinline{\wp::strategy}, by doing this, one assures that when the plug-in that
+\lstinline{\wp::strategy}. By doing this, one ensures that when the plug-in that
registers the extension is not available, the extension will be ignored (with a
-warning) and the parsing will continue.
+warning) and the parsing will continue. Note however that the plug-in name is
+\emph{not} part of the extension name, so that two different plug-ins cannot
+register an extension with the same keyword.
-Once an extension is registered a clause of the form \verb|kw e1,...,en;|, where each \verb|ei| can be
-any syntactically valid ACSL term or predicate, will be treated by the parser as belonging to the
-extension \verb|kw|.
+Once an extension is registered with keyword \lstinline|kw|,
+a clause of the form \verb|kw e1,...,en;|,
+where each \verb|ei| can be any syntactically valid ACSL term or predicate,
+will be treated by the parser as belonging to the extension \verb|kw|.
Contract extension clauses must occur after \verb|assumes| and \verb|requires| clauses if any, but
can be freely mixed with other behavior clauses (post-conditions, \verb|assigns|, \verb|frees| and
@@ -3983,6 +3988,8 @@ registered by one of the following functions, depending on its category.
\scodeidx{Acsl\_extension}{register\_code\_annot\_next\_both}
\item \texttt{Acsl\_extension.register\_code\_annot\_next\_both}%
\scodeidx{Acsl\_extension}{register\_code\_annot\_next\_loop}
+\item \texttt{Acsl\_extension.register\_module\_importer}%
+\scodeidx{Acsl\_extension}{register\_module\_importer}
\end{itemize}
Each function takes the following mandatory arguments:
@@ -3992,10 +3999,13 @@ Each function takes the following mandatory arguments:
\item \texttt{kw} the name of the extension,
\item \texttt{typer} the type-checking function itself.
\item \texttt{status}, a boolean flag indicating whether the extended
- annotation may have a validity status, and
-
+ annotation may have a validity status.
\end{itemize}
+The last function has a different behavior and is used to load external
+\acsl modules with the \verb+import+ clause. It is treated at the end
+of the section (see p.~\pageref{par:ext-modules}).
+
During type-checking, the list \verb|[e1;...;en]| will be given to \verb|typer|,
together with the current typing environment (which allows discriminating
between contract and loop extensions and will have the appropriate logic labels
@@ -4112,7 +4122,98 @@ version in the interface:
\includegraphics[width=\textwidth]{examples/acsl_extension_ext_types/acsl_extension_ext_types}
+\paragraph{External Modules.}
+\label{par:ext-modules}
+
+Finally, let us introduce how to extend \acsl
+modules with external module importers. A typical usage is to import logical
+definitions from other languages, e.g. \textsf{Coq} or \textsf{Why3}, as regular
+\acsl module definitions. From the user point the view, this takes the form
+of an extended \verb+import+ clause:
+
+\begin{lstlisting}
+//@ import <loader>: <module-name> [ \as <alias-name> ];
+\end{lstlisting}
+
+The syntax is similar to the general ACSL \verb+import+ annotation, except that the
+module name is prefixed with the name of the loader extension. For instance:
+
+\begin{lstlisting}[style=c]
+//@ import Foo: foo::bar::Jazz ;
+\end{lstlisting}
+
+Here, \verb+Foo:+ specifies the name of the \acsl extension responsible for
+importing the module, and \verb+foo::bar::Jazz+ is the name of the module
+to be imported.
+
+To define such an external module loader, a plug-in shall call the
+\scodeidxdef{Acsl\_extension}{register\_module\_importer}
+\verb+Acsl_extension.register_module_importer+ with a suitable loader function.
+The loader function is responsible for resolving the module name and defining
+the associated \acsl logic types, functions and predicates. Here is an example
+of such a loader function:
+
+\scodeidx{Logic\_typing}{module\_builder}
+\begin{lstlisting}[language=OCaml]
+open Cil_types
+open Logic_typing
+
+let loader (ctxt: module_builder) (loc: location) (path: string list) =
+ begin
+ (* in the example above, path is ["foo","bar","Jazz"] *)
+ (* ... read some file .. *)
+ let p : location = ... in
+ let t = Cil.make_logic_type "t" in
+ (* ... configure type t ... *)
+ let q : location = ... in
+ let f = Cil.make_logic_info "f" in
+ (* ... configure function f ... *)
+ ctxt.add_logic_type p t ;
+ ctxt.add_logic_function q f ;
+ (* ... *)
+ end
+
+let () = Acsl_extension.register_module_importer "Foo" loader
+\end{lstlisting}
+Added types and functions shall use local names, as in the example above.
+After importation, the imported declarations will be accessible through
+their full-name identifier, for instance \verb+foo::bar::Jazz:f+
+in the example above.
+
+As explained in the \framac source documentation, module importers might be
+invoked multiple times by the kernel, e.g. when a given module is imported from
+different source files. Although the loader itself can use memoization
+techniques to save time, the module builder shall be populated on every call.
+
+When printing the internal AST from \framac command line using \verb+-print+
+option, externally imported modules are listed with one single clause for each,
+with no aliasing in order to avoid any ambiguity. For instance:
+\begin{ccode}
+//@ import MyLoader: foo::bar::Jazz \as _ ;
+\end{ccode}
+
+Alternatively, you can debug the logical definitions actually imported by any
+driver by using \verb+-print+ with the \verb+printer:imported-modules+ debugging
+key:
+\begin{frama-c-commands}
+> frama-c ... -print -kernel-message-key printer:imported-modules
+\end{frama-c-commands}
+
+With this option, the contents of the imported modules are printed like regular
+module definitions, with only a comment to mention the origin of the plug-in:
+\begin{ccode}
+/*@ // import MyLoader:
+ module foo::bar::Jazz {
+ ...
+ }
+ */
+\end{ccode}
+
+Notice that, when using the \verb+printer:imported-modules+ message key, the
+resulting file will still compile and type-check, but the plug-in extension will
+no more be aware of the external nature of those modules, and it will probably
+\emph{not} work as with the original specification.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/doc/developer/changes.tex b/doc/developer/changes.tex
index ff75abc257c07627c32d9314b764e75c4c368331..3078a799fa5df6e2a568cf6e72e3c820ddd08438 100644
--- a/doc/developer/changes.tex
+++ b/doc/developer/changes.tex
@@ -5,7 +5,12 @@
This chapter summarizes the major changes in this documentation between each
\framac release, from newest to oldest.
-%\section*{Frama-C+dev}
+\section*{Frama-C+dev}
+\begin{itemize}
+ \item \textbf{ACSL Extension}:
+ Document new \verb+register_module_importer+ extension.
+\end{itemize}
+
\section*{29.0 (Copper)}
\begin{itemize}
diff --git a/doc/userman/user-acsl.tex b/doc/userman/user-acsl.tex
index 9da27d2c8d42b8632a4a59898c58a93c5ba374e1..871d7c0d7f9592819fe510bd8bedae027d205d12 100644
--- a/doc/userman/user-acsl.tex
+++ b/doc/userman/user-acsl.tex
@@ -1,6 +1,6 @@
-\chapter{ACSL extensions} % here we do not use the macro (avoids a warning)
+\chapter{ACSL Extensions} % here we do not use the macro (avoids a warning)
\label{cha:acsl-extensions}
-\section{Extension syntaxes}
+\section{Extension Syntaxes}
\label{acsl:syntax}
When a plug-in registers an extension, it can be used in \acsl annotations
@@ -14,9 +14,9 @@ extensions coming from an unloaded plug-in can be ignored this way. For
example, if \Eva is not loaded, \lstinline|\eva::unroll _| annotations will be
ignored with a warning, whereas \lstinline|unroll _| cannot be identified as
being supported by Eva, which means that it can only be treated as a user
-error.
+error.
-\section{Handling indirect calls with \texttt{calls}}
+\section{Handling Indirect Calls with \texttt{calls}}
\label{acsl:calls}
In order to help plug-ins support indirect calls (i.e. calls through
@@ -33,6 +33,79 @@ indicates that the pointer \lstinline|f| can point to any one of
It is in particular used by the WP plug-in (see \cite{wp} for more information).
+\section{Importing External Module Definitions}
+\label{acsl:modules}
+
+Support for \acsl modules has been introduced in \nextframacversion.
+Module definitions can be nested. Inside a module \verb+A+,
+a sub-module \verb+B+ will actually defines the module \verb+A::B+, and so on.
+
+Notice than for long identifiers like \verb+A::B::C+ to be valid, no space is
+allowed around the \verb+:+ characters, and \verb+A+, \verb+B+, \verb+C+ must be
+regular \acsl identifiers, i.e.~they shall only consist of upper case or lower case letters, digits,
+underscores, and must start with a letter.
+
+Inside module \verb+M+ declaration, where \verb+M+ it the long identifier of the
+module being declared, a logic declaration \verb+a+ will actually define the
+symbol \verb+M::a+. You shall always use the complete name of an identifier to
+avoid ambiguities in your specifications. However, in order to ease reading, it
+is also possible to use shortened names instead.
+
+The rules for shortening long identifiers generalize to any depth of nested
+modules. We only illustrate them in a simple case. Consider for instance a logic
+declaration \verb+a+ in module \verb+A::B+, depending on the context, it is possible to shorten
+its name as follows:
+\begin{itemize}
+\item Everywhere, you can use \verb+A::B::a+;
+\item Inside module \verb+A+, you can use \verb+B::a+;
+\item Inside module \verb+A::B+, you can use \verb+a+;
+\item After annotation \lstinline[language=ACSL]|import A::B|, you can use \verb+B::a+;
+\item After annotation \lstinline[language=ACSL]|import A::B as C|, you can use \verb+C::a+;
+\end{itemize}
+
+You may also use local \lstinline[language=ACSL]+import+ annotations inside
+module definitions, in
+which case the introduced aliases will be only valid until the end of the module
+scope.
+
+Depending on dedicated plug-in support, you may also import modules definitions
+from external specifications, generally from an external proof assistant like
+\textsf{Coq} or \textsf{Why3}. The \acsl extended syntax for importing external
+specifications is as follows:
+
+\begin{lstlisting}[language=ACSL]
+import <Driver>: <ModuleName> [ as <Name> ];
+\end{lstlisting}
+
+This is a generalization of the regular \acsl \lstinline[language=ACSL]|import|
+clause just mentioned above. The \verb+<Driver>+ name identifies the kind of external
+specifications to be loaded. Drivers are defined by dedicated plug-in support
+only, and you shall consult the documentation of each plug-in to known which
+drivers are available.
+
+The \verb+<ModuleName>+ identifies both the name of the imported module and the
+external specification to be imported, with a \verb+<Driver>+ dependent meaning.
+
+The alias name \verb+<Name>+, if provided, has the same meaning than when
+importing regular module names (just described above) in the current scope.
+
+When importing \emph{external} specifications, depending on the \verb+<Driver>+
+used, it is possible to have logic identifiers with an extended lexical format:
+\begin{itemize}
+\item \verb+M::(op)+ where \verb+M+ is a regular module identifier, and
+ \verb+op+ any combination of letters, digits, operators, brackets, braces,
+ underscores and quotes. For instance, \verb+map::Map::([<-])+ is a syntactically
+ valid identifier, and \verb+number::Complex::(<=)(a,b)+ is a syntactically valid
+ expression.
+\item \verb+M::X+ where \verb+M+ is a regular module identifier and
+ \verb+X+ any combination of letters, digits, underscores and quotes.
+ For instance, \verb+Foo::bar'jazz+ is a syntactically valid identifier.
+\end{itemize}
+
+There is currently no support for external specification drivers from the
+standard distribution of \FramaC, although external plug-ins might define some
+using the extension API, consult the plug-in developer manual for details.
+
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "userman"
diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index b308690922f1154fc8a5764082fd762654768e66..e26ee6db53ace34dbbb9cf36f9337dfc23c916f8 100644
--- a/doc/userman/user-changes.tex
+++ b/doc/userman/user-changes.tex
@@ -18,6 +18,8 @@ release. First we list changes of the last release.
\texttt{-kernel-warn-key typing:implicit-function-declaration}),
and \texttt{-warn-decimal-float} (replaced by
\texttt{-kernel-warn-key parser:decimal-float}).
+\item \textbf{ACSL extensions:} introduced support for ACSL modules
+ and external module loading via dedicated plug-ins.
\end{itemize}
\section*{29.0 (Copper)}
diff --git a/src/kernel_internals/parsing/logic_lexer.mli b/src/kernel_internals/parsing/logic_lexer.mli
index 5dc9212955a2fdb48b9339192eb237ab24eeedc9..3db9e486f79e3227d2ce4e9278c4198cea0f2bf0 100644
--- a/src/kernel_internals/parsing/logic_lexer.mli
+++ b/src/kernel_internals/parsing/logic_lexer.mli
@@ -45,6 +45,7 @@ val spec : Logic_ptree.spec parse
val ext_spec : Lexing.lexbuf -> Logic_ptree.ext_spec
(** ACSL extension for parsing external spec file.
- Here, the tokens "/*" and "*/" are accepted by the lexer
- as unnested C comments into the external ACSL specifications.
+ Modifies tokens as follows:
+ - C-comments [/* ... */] can be used and can be nested
+ - ["module"] keyword is interpreted as [EXT_SPEC_MODULE]
*)
diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index 445ecb3af1c68ec02aac544802e0469b9cb2efec..2a3d39798e18687011a636abef7796f41e013112 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -39,6 +39,8 @@
exception Error of (int * int) * string
+ let ext_acsl_spec = ref false
+
let loc lexbuf = (lexeme_start lexbuf, lexeme_end lexbuf)
let lex_error lexbuf s =
@@ -104,6 +106,7 @@
let identifier, is_acsl_keyword =
let all_kw = Hashtbl.create 37 in
let type_kw = Hashtbl.create 3 in
+ let ext_acsl_kw kw s _ = if !ext_acsl_spec then kw else IDENTIFIER s in
List.iter
(fun (i,t) -> Hashtbl.add all_kw i t;)
[
@@ -112,8 +115,7 @@
"assert", (fun _ -> ASSERT);
"assigns", (fun _ -> ASSIGNS);
"assumes", (fun _ -> ASSUMES);
- "at", (fun _ -> EXT_AT);
- (* ACSL extension for external spec file *)
+ "at", ext_acsl_kw EXT_SPEC_AT "at";
"axiom", (fun _ -> AXIOM);
"axiomatic", (fun _ -> AXIOMATIC);
"behavior", (fun _ -> BEHAVIOR);
@@ -126,8 +128,7 @@
"complete", (fun _ -> COMPLETE);
"const", (fun _ -> CONST);
"continues", (fun _ -> CONTINUES);
- "contract", (fun _ -> CONTRACT);
- (* ACSL extension for external spec file *)
+ "contract", ext_acsl_kw EXT_SPEC_CONTRACT "contract";
"decreases", (fun _ -> DECREASES);
"disjoint", (fun _ -> DISJOINT);
"double", (fun _ -> DOUBLE);
@@ -136,27 +137,26 @@
"enum", (fun _ -> ENUM);
"exits", (fun _ -> EXITS);
"frees", (fun _ -> FREES);
- "function", (fun _ -> FUNCTION);
- (* ACSL extension for external spec file *)
+ "function", ext_acsl_kw EXT_SPEC_FUNCTION "function";
"float", (fun _ -> FLOAT);
"for", (fun _ -> FOR);
"global", (fun _ -> GLOBAL);
"if", (fun _ -> IF);
- "inductive", (fun _ -> INDUCTIVE);
- "include", (fun _ -> INCLUDE);
- (* ACSL extension for external spec file *)
+ "import", (fun _ -> IMPORT);
+ "inductive", (fun _ -> INDUCTIVE);
+ "include", ext_acsl_kw EXT_SPEC_INCLUDE "include";
"int", (fun _ -> INT);
"invariant", (fun _ -> INVARIANT);
"label", (fun _ -> LABEL);
"lemma", (fun _ -> LEMMA);
- "let", (fun _ -> EXT_LET);
+ "let", ext_acsl_kw EXT_SPEC_LET "let";
(* ACSL extension for external spec file *)
"logic", (fun _ -> LOGIC);
"long", (fun _ -> LONG);
"loop", (fun _ -> LOOP);
"model", (fun _ -> MODEL);
(* ACSL extension for model fields *)
- "module", (fun _ -> MODULE);
+ "module", (fun _ -> if !ext_acsl_spec then EXT_SPEC_MODULE else MODULE);
(* ACSL extension for external spec file *)
"predicate", (fun _ -> PREDICATE);
"reads", (fun _ -> READS);
@@ -218,6 +218,7 @@
"\\allocation", ALLOCATION;
"\\allocable", ALLOCABLE;
"\\automatic", AUTOMATIC;
+ "\\as", AS;
"\\at", AT;
"\\base_addr", BASE_ADDR;
"\\block_length", BLOCK_LENGTH;
@@ -266,6 +267,9 @@
else IDENTIFIER s
end
+ let longident lexbuf =
+ let s = lexeme lexbuf in LONGIDENT s
+
(* Update lexer buffer. *)
let update_line_pos lexbuf line =
let pos = lexbuf.Lexing.lex_curr_p in
@@ -279,8 +283,6 @@
let pos = lexbuf.Lexing.lex_curr_p in
lexbuf.Lexing.lex_curr_p <- { pos with Lexing.pos_fname = file }
- let accept_c_comments_into_acsl_spec = ref false
-
let hack_merge_tokens current next =
match (current,next) with
| CHECK, REQUIRES -> true, CHECK_REQUIRES
@@ -350,8 +352,18 @@ let rE = ['E''e']['+''-']? rD+
let rP = ['P''p']['+''-']? rD+
let rFS = ('f'|'F'|'l'|'L'|'d'|'D')
let rIS = ('u'|'U'|'l'|'L')*
+let rOP = [
+ '=' '<' '>' '~'
+ '+' '-' '*' '/' '\\' '%'
+ '!' '$' '&' '?' '@' '^' '.' ':' '|' '#'
+ '_' '\''
+ 'a'-'z' 'A'-'Z' '0'-'9'
+ '[' ']' '{' '}'
+]
let comment_line = "//" [^'\n']*
let rIdentifier = rL (rL | rD)*
+let xIdentifier = rL (rL | rD | "'")*
+let opIdentifier = (rL | rD | rOP)+
(* Do not forget to update also the corresponding chr rule if you add
a supported escape sequence here. *)
@@ -370,7 +382,7 @@ rule token = parse
| comment_line '\n' { Lexing.new_line lexbuf; token lexbuf }
| comment_line eof { token lexbuf }
| "*/" { lex_error lexbuf "unexpected block-comment closing" }
- | "/*" { if !accept_c_comments_into_acsl_spec
+ | "/*" { if !ext_acsl_spec
then comment lexbuf
else lex_error lexbuf "unexpected block-comment opening"
}
@@ -381,6 +393,8 @@ rule token = parse
check_ext_plugin (fst cabsloc) plugin tok
}
| '\\' rIdentifier { bs_identifier lexbuf }
+ | ( rIdentifier "::")+ xIdentifier { longident lexbuf }
+ | ( rIdentifier "::")+ "(" opIdentifier ")" { longident lexbuf }
| rIdentifier {
let loc = Lexing.(lexeme_start_p lexbuf, lexeme_end_p lexbuf) in
let cabsloc = Cil_datatype.Location.of_lexing_loc loc in
@@ -611,14 +625,11 @@ and comment = parse
let spec = parse_from_position Logic_parser.spec
- let ext_spec lexbuf = try
- accept_c_comments_into_acsl_spec := true ;
- let r = Logic_parser.ext_spec token lexbuf in
- accept_c_comments_into_acsl_spec := false ;
- r
- with exn ->
- accept_c_comments_into_acsl_spec := false ;
- raise exn
+ let ext_spec lexbuf =
+ ext_acsl_spec:=true;
+ let finally() = ext_acsl_spec:=false in
+ let work () = Logic_parser.ext_spec token lexbuf in
+ Fun.protect ~finally work
type 'a parse = Filepath.position * string -> (Filepath.position * 'a) option
@@ -626,9 +637,3 @@ and comment = parse
let buf = Buffer.create 16 in
chr buf lexbuf
}
-
-(*
-Local Variables:
-compile-command: "make -C ../../.. byte"
-End:
-*)
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 4e8987cc60448820622a9b4d855f9b9e4d432edf..ce9c3e2bedab3ff85e5b869b53f5050a32189c99 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -86,6 +86,21 @@
| (Lt|Le), (Unknown|Less) -> Less, true
| _ -> sense, false
+ let module_types : string list ref Stack.t = Stack.create ()
+
+ let push_typename t =
+ Logic_env.add_typename t ;
+ try
+ let r = Stack.top module_types in r := t :: !r
+ with Stack.Empty -> ()
+
+ let push_module_types () =
+ Stack.push (ref []) module_types
+
+ let pop_module_types () =
+ let r = Stack.pop module_types in
+ List.iter Logic_env.remove_typename !r
+
let type_variables_stack = Stack.create ()
let enter_type_variables_scope l =
@@ -252,9 +267,9 @@
/* Otherwise, the token will not be usable inside a contract. */
/*****************************************************************************/
-%token MODULE FUNCTION CONTRACT INCLUDE EXT_AT EXT_LET
-/* ACSL extension for external spec file */
-%token <string> IDENTIFIER TYPENAME IDENTIFIER_EXT
+%token EXT_SPEC_MODULE EXT_SPEC_FUNCTION EXT_SPEC_CONTRACT EXT_SPEC_INCLUDE
+%token EXT_SPEC_AT EXT_SPEC_LET
+%token <string> LONGIDENT IDENTIFIER TYPENAME IDENTIFIER_EXT
%token <bool*string> STRING_LITERAL
%token <string> INT_CONSTANT
%token <string> FLOAT_CONSTANT
@@ -263,7 +278,7 @@
%token LPAR RPAR IF ELSE COLON COLON2 COLONCOLON DOT DOTDOT DOTDOTDOT
%token INT INTEGER REAL BOOLEAN BOOL FLOAT LT GT LE GE EQ NE COMMA ARROW EQUAL
%token FORALL EXISTS IFF IMPLIES AND OR NOT SEPARATED
-%token TRUE FALSE OLD AT RESULT
+%token TRUE FALSE OLD AS AT RESULT
%token BLOCK_LENGTH BASE_ADDR OFFSET VALID VALID_READ VALID_INDEX VALID_RANGE
%token OBJECT_POINTER VALID_FUNCTION
%token ALLOCATION STATIC REGISTER AUTOMATIC DYNAMIC UNALLOCATED
@@ -278,7 +293,8 @@
%token <string> EXT_CODE_ANNOT EXT_GLOBAL EXT_GLOBAL_BLOCK EXT_CONTRACT
%token EXITS BREAKS CONTINUES RETURNS
%token VOLATILE READS WRITES
-%token LOGIC PREDICATE INDUCTIVE AXIOMATIC AXIOM LEMMA LBRACE RBRACE
+%token LOGIC PREDICATE INDUCTIVE AXIOM LEMMA LBRACE RBRACE
+%token AXIOMATIC MODULE IMPORT
%token GHOST MODEL CASE
%token VOID CHAR SIGNED UNSIGNED SHORT LONG DOUBLE STRUCT ENUM UNION
%token BSUNION INTER
@@ -528,13 +544,13 @@ lexpr_inner:
| RESULT { info $sloc PLresult }
| SEPARATED LPAR ne_lexpr_list RPAR
{ info $sloc (PLseparated $3) }
-| full_identifier LPAR ne_lexpr_list RPAR
+| symbol_identifier LPAR ne_lexpr_list RPAR
{ info $sloc (PLapp ($1, [], $3)) }
-| full_identifier LBRACE ne_label_args RBRACE LPAR ne_lexpr_list RPAR
+| symbol_identifier LBRACE ne_label_args RBRACE LPAR ne_lexpr_list RPAR
{ info $sloc (PLapp ($1, $3, $6)) }
-| full_identifier LBRACE ne_label_args RBRACE
+| symbol_identifier LBRACE ne_label_args RBRACE
{ info $sloc (PLapp ($1, $3, [])) }
-| full_identifier { info $sloc (PLvar $1) }
+| symbol_identifier { info $sloc (PLvar $1) }
| PI { info $sloc (PLvar "\\pi") }
| lexpr_inner GTGT lexpr_inner { info $sloc (PLbinop ($1, Brshift, $3))}
| lexpr_inner LTLT lexpr_inner { info $sloc (PLbinop ($1, Blshift, $3))}
@@ -549,18 +565,28 @@ lexpr_inner:
| EMPTY { info $sloc PLempty }
| BSUNION LPAR lexpr_list RPAR { info $sloc (PLunion $3) }
| INTER LPAR lexpr_list RPAR { info $sloc (PLinter $3) }
-| LBRACE lexpr_list RBRACE
- { info $sloc (PLset ($2)) }
-| LBRACE lexpr PIPE binders RBRACE
+| 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
+ { info $sloc (PLset ($2 :: $4)) }
+| LBRACE lexpr_inner PIPE binders RBRACE
{ info $sloc (PLcomprehension ($2,$4,None)) }
-| LBRACE lexpr PIPE binders SEMICOLON lexpr RBRACE
+| LBRACE lexpr_inner PIPE binders SEMICOLON lexpr RBRACE
{ info $sloc (PLcomprehension ($2,$4,Some $6)) }
/* Aggregated object initialization */
| LBRACE field_init RBRACE
{ info $sloc (PLinitField($2)) }
| LBRACE array_init RBRACE
{ info $sloc (PLinitIndex($2)) }
-| LBRACE lexpr WITH update RBRACE
+| LBRACE lexpr_inner WITH update RBRACE
{ List.fold_left
(fun a (path,upd_val) -> info $sloc (PLupdate(a,path,upd_val))) $2 $4 }
/*
@@ -653,7 +679,7 @@ binders_reentrance:
;
decl_spec:
-| type_spec(typename) var_spec { ($1, let (modif, name) = $2 in (modif $1, name)) }
+| type_spec(typesymbol) var_spec { ($1, let (modif, name) = $2 in (modif $1, name)) }
;
var_spec:
@@ -731,10 +757,15 @@ logic_type_gen(tname):
typename:
| name = TYPENAME { name }
+;
+
+typesymbol:
+| name = TYPENAME { name }
+| name = LONGIDENT { name }
/* TODO treat the case of an ACSL keyword that is also a typedef */
;
-logic_type: logic_type_gen(typename) { $1 }
+logic_type: logic_type_gen(typesymbol) { $1 }
cv:
CONST { cv_const }
@@ -742,16 +773,16 @@ cv:
| BSGHOST { cv_ghost }
;
-type_spec_cv(tname):
- type_spec(tname) cv_after { $2 $1 }
-| cv type_spec_cv(tname) { LTattribute ($2, $1) }
+type_spec_cv:
+ type_spec(TYPENAME) cv_after { $2 $1 }
+| cv type_spec_cv { LTattribute ($2, $1) }
cv_after:
/* empty */ { fun t -> t }
| cv cv_after { fun t -> $2 (LTattribute (t,$1)) }
cast_logic_type:
- | type_spec_cv(TYPENAME) abs_spec_cv_option { $2 $1 }
+ | type_spec_cv abs_spec_cv_option { $2 $1 }
;
logic_rt_type:
@@ -872,6 +903,11 @@ ne_logic_type_list(tname):
| l = separated_nonempty_list(COMMA,logic_type_gen(tname)) { l }
;
+symbol_identifier:
+| id = full_identifier { id }
+| name = LONGIDENT { name }
+;
+
full_identifier:
| id = identifier { id }
| ADMIT { "admit" }
@@ -879,7 +915,6 @@ full_identifier:
| ASSERT { "assert" }
| ASSIGNS { "assigns" }
| ASSUMES { "assumes" }
-| EXT_AT { "at" }
| AXIOM { "axiom" }
| AXIOMATIC { "axiomatic" }
| BEHAVIOR { "behavior" }
@@ -887,19 +922,16 @@ full_identifier:
| CHECK { "check" }
| COMPLETE { "complete" }
| CONTINUES { "continues" }
-| CONTRACT { "contract" }
| DECREASES { "decreases" }
| DISJOINT { "disjoint" }
| ENSURES { "ensures" }
| EXITS { "exits" }
| FREES { "frees" }
-| FUNCTION { "function" }
| GLOBAL { "global" }
+| IMPORT { "import" }
| INDUCTIVE { "inductive" }
-| INCLUDE { "include" }
| INVARIANT { "invariant" }
| LEMMA { "lemma" }
-| EXT_LET { "let" }
| LOGIC { "logic" }
| LOOP { "loop" }
| MODEL { "model" }
@@ -910,6 +942,12 @@ full_identifier:
| TERMINATES { "terminates" }
| TYPE { "type" }
| VARIANT { "variant" }
+| EXT_SPEC_MODULE { "module" }
+| EXT_SPEC_FUNCTION { "function" }
+| EXT_SPEC_CONTRACT { "contract" }
+| EXT_SPEC_INCLUDE { "include" }
+| EXT_SPEC_AT { "at" }
+| EXT_SPEC_LET { "let" }
| id = EXT_CODE_ANNOT { id }
| id = EXT_CONTRACT { id }
| id = EXT_GLOBAL { id }
@@ -939,9 +977,10 @@ ext_global_clauses:
ext_global_clause:
| decl { Ext_decl (loc_decl $sloc $1) }
-| EXT_LET any_identifier EQUAL lexpr SEMICOLON { Ext_macro (false, $2, $4) }
-| GLOBAL EXT_LET any_identifier EQUAL lexpr SEMICOLON { Ext_macro (true, $3, $5) }
-| INCLUDE string SEMICOLON { let b,s = $2 in Ext_include(b,s, loc $sloc) }
+| GLOBAL
+ EXT_SPEC_LET any_identifier EQUAL lexpr SEMICOLON { Ext_macro (true, $3, $5) }
+| EXT_SPEC_LET any_identifier EQUAL lexpr SEMICOLON { Ext_macro (false, $2, $4) }
+| EXT_SPEC_INCLUDE string SEMICOLON { let b,s = $2 in Ext_include(b,s, loc $sloc) }
;
ext_global_specs_opt:
@@ -1020,15 +1059,15 @@ ext_identifier:
;
ext_module_markup:
-| MODULE ext_identifier COLON { $2 }
+| EXT_SPEC_MODULE ext_identifier COLON { $2 }
;
ext_function_markup:
-| FUNCTION ext_identifier COLON { $2, loc $sloc }
+| EXT_SPEC_FUNCTION ext_identifier COLON { $2, loc $sloc }
;
ext_contract_markup:
-| CONTRACT ext_identifier_opt COLON { $2 }
+| EXT_SPEC_CONTRACT ext_identifier_opt COLON { $2 }
;
stmt_markup:
@@ -1042,7 +1081,7 @@ stmt_markup_attr:
;
ext_at_stmt_markup:
-| EXT_AT stmt_markup_attr COLON { $2 }
+| EXT_SPEC_AT stmt_markup_attr COLON { $2 }
;
/*** function and statement contracts ***/
@@ -1182,8 +1221,8 @@ ne_decreases:
;
variant:
-| lexpr FOR any_identifier { ($1, Some $3) }
-| lexpr { ($1, None) }
+| lexpr FOR full_identifier { ($1, Some $3) }
+| lexpr { ($1, None) }
;
simple_clauses:
@@ -1453,8 +1492,8 @@ loop_grammar_extension:
}
;
-/*** code annotations ***/
+/*** code annotations ***/
beg_code_annotation:
| FOR {}
| ASSERT {}
@@ -1589,14 +1628,14 @@ poly_id_type:
| full_identifier
{ enter_type_variables_scope []; ($1,[]) }
| full_identifier LT ne_tvar_list GT
- { enter_type_variables_scope $3; ($1,$3) }
+ { enter_type_variables_scope $3; ($1,$3) }
;
/* we need to recognize the typename as soon as it has been declared,
so that it can be used in data constructors in the type definition itself
*/
poly_id_type_add_typename:
-| poly_id_type { let (id,_) = $1 in Logic_env.add_typename id; $1 }
+| poly_id_type { push_typename (fst $1) ; $1 }
;
poly_id:
@@ -1647,6 +1686,16 @@ logic_def:
LDlemma (id, labels, tvars, toplevel_pred Admit $4) }
| AXIOMATIC any_identifier LBRACE logic_decls RBRACE
{ LDaxiomatic($2,$4) }
+| MODULE push_module_name LBRACE logic_decls RBRACE
+ { pop_module_types () ; LDmodule($2,$4) }
+| IMPORT mId = module_name SEMICOLON
+ { LDimport(None,mId,None) }
+| IMPORT mId = module_name AS id = IDENTIFIER SEMICOLON
+ { LDimport(None,mId,Some id) }
+| IMPORT drv = IDENTIFIER COLON mId = module_name SEMICOLON
+ { LDimport(Some drv,mId,None) }
+| IMPORT drv = IDENTIFIER COLON mId = module_name AS id = IDENTIFIER SEMICOLON
+ { LDimport(Some drv,mId,Some id) }
| TYPE poly_id_type_add_typename EQUAL typedef SEMICOLON
{ let (id,tvars) = $2 in
exit_type_variables_scope ();
@@ -1654,6 +1703,15 @@ logic_def:
}
;
+module_name:
+| IDENTIFIER { $1 }
+| LONGIDENT { $1 }
+;
+
+push_module_name:
+| module_name { push_module_types () ; $1 }
+;
+
deprecated_logic_decl:
/* OBSOLETE: logic function declaration */
| LOGIC logic_rt_type poly_id opt_parameters SEMICOLON
@@ -1672,7 +1730,7 @@ deprecated_logic_decl:
/* OBSOLETE: type declaration */
| TYPE poly_id_type SEMICOLON
{ let (id,tvars) = $2 in
- Logic_env.add_typename id;
+ Logic_env.add_typename id ; (* not in a module! *)
exit_type_variables_scope ();
let source = pos $symbolstartpos in
obsolete "logic type declaration" ~source ~now:"an axiomatic block";
@@ -1710,8 +1768,8 @@ logic_decl:
/* type declaration */
| TYPE poly_id_type SEMICOLON
{ let (id,tvars) = $2 in
- Logic_env.add_typename id;
exit_type_variables_scope ();
+ push_typename id;
LDtype(id,tvars,None) }
/* axiom */
| AXIOM poly_id COLON lexpr SEMICOLON
@@ -1822,12 +1880,14 @@ any_identifier:
identifier_or_typename:
| TYPENAME { $1 }
+| LONGIDENT { $1 }
| full_identifier { $1 }
-
+;
identifier_or_typename_full: /* allowed as C field names */
| is_acsl_typename { $1 }
-| identifier_or_typename { $1 }
+| TYPENAME { $1 }
+| full_identifier { $1 }
;
identifier: /* part included into 'identifier_or_typename', but duplicated to avoid parsing conflicts */
@@ -1901,7 +1961,7 @@ post_cond:
is_acsl_spec:
| post_cond { snd $1 }
-| EXT_CONTRACT { $1 }
+| EXT_CONTRACT { $1 }
| ASSIGNS { "assigns" }
| ALLOCATES { "allocates" }
| FREES { "frees" }
@@ -1917,8 +1977,8 @@ is_acsl_spec:
is_acsl_decl_or_code_annot:
| EXT_CODE_ANNOT { $1 }
-| EXT_GLOBAL { $1 }
-| EXT_GLOBAL_BLOCK { $1 }
+| EXT_GLOBAL { $1 }
+| EXT_GLOBAL_BLOCK { $1 }
| IDENTIFIER_EXT { $1 }
| ASSUMES { "assumes" }
| ASSERT { "assert" }
@@ -1941,6 +2001,8 @@ is_acsl_decl_or_code_annot:
| AXIOM { "axiom" }
| VARIANT { "variant" }
| AXIOMATIC { "axiomatic" }
+| MODULE { "module" }
+| IMPORT { "import" }
;
is_acsl_typename:
@@ -1949,12 +2011,12 @@ is_acsl_typename:
;
is_ext_spec:
-| CONTRACT { "contract" }
-| FUNCTION { "function" }
-| MODULE { "module" }
-| INCLUDE { "include" }
-| EXT_AT { "at" }
-| EXT_LET { "let" }
+| EXT_SPEC_MODULE { "module" }
+| EXT_SPEC_FUNCTION { "function" }
+| EXT_SPEC_CONTRACT { "contract" }
+| EXT_SPEC_INCLUDE { "include" }
+| EXT_SPEC_AT { "at" }
+| EXT_SPEC_LET { "let" }
;
keyword:
@@ -1975,6 +2037,7 @@ bs_keyword:
| ALLOCATION { () }
| AUTOMATIC { () }
| AT { () }
+| AS { () }
| BASE_ADDR { () }
| BLOCK_LENGTH { () }
| BSGHOST { () }
@@ -2013,6 +2076,7 @@ bs_keyword:
wildcard:
| any_identifier { () }
+| LONGIDENT { () }
| bs_keyword { () }
| AMP { () }
| AND { () }
@@ -2077,9 +2141,3 @@ any:
;
%%
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 2b0b61cf1781ef85b9a34defc8e405abc08675d2..7a28e4670df8c333f4595f31f9522f61eb8a9809 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -2739,7 +2739,7 @@ let makeGlobalVarinfo (isadef: bool) (vi: varinfo) : varinfo * bool =
prototypes. Logic specifications refer to the varinfo in this table. *)
begin
match vi.vtype with
- | TFun (_,Some formals , _, _ ) ->
+ | TFun (_,Some formals , _, _) ->
(try
let old_formals_env = getFormalsDecl oldvi in
List.iter2
@@ -3584,14 +3584,6 @@ struct
include Logic_labels
- include Logic_env
-
- let add_logic_function =
- add_logic_function_gen Logic_utils.is_same_logic_profile
-
- let remove_logic_info =
- remove_logic_info_gen Logic_utils.is_same_logic_profile
-
let integral_cast = integral_cast
(* This function raises a non-recoverable when [-kernel-warn-key annot-error]
@@ -6487,7 +6479,7 @@ and doExp local_env
*)
if not isSpecialBuiltin && not are_ghost then begin
warn_no_proto f;
- let typ = TFun (resType, Some [], false, attrs) in
+ let typ = TFun (resType, Some [], false,attrs) in
Cil.update_var_type f typ;
end
| None, _ (* TODO: treat function pointers. *)
@@ -9612,27 +9604,27 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
dl;
empty
- | Cabs.GLOBANNOT (decl) when isglobal ->
- begin
- List.iter
- (fun decl ->
- let loc = convLoc decl.Logic_ptree.decl_loc in
- let<> UpdatedCurrentLoc = loc in
- try
- let tdecl = Ltyping.annot decl in
+ | Cabs.GLOBANNOT decls when isglobal ->
+ List.iter
+ (fun decl ->
+ let loc = convLoc decl.Logic_ptree.decl_loc in
+ let<> UpdatedCurrentLoc = loc in
+ try
+ match Ltyping.annot decl with
+ | None -> ()
+ | Some tdecl ->
let attr = fc_stdlib_attribute [] in
let tdecl =
List.fold_left
(Fun.flip Logic_utils.add_attribute_glob_annot) tdecl attr
in
cabsPushGlobal (GAnnot(tdecl,Current_loc.get ()))
- with LogicTypeError ((source,_),msg) ->
- Kernel.warning
- ~wkey:Kernel.wkey_annot_error ~source
- "%s. Ignoring global annotation" msg
- )
- decl;
- end;
+ with LogicTypeError ((source,_),msg) ->
+ Kernel.warning
+ ~wkey:Kernel.wkey_annot_error ~source
+ "%s. Ignoring global annotation" msg
+ )
+ decls;
empty
| Cabs.GLOBANNOT _ | Cabs.PRAGMA _ | Cabs.GLOBASM _ | Cabs.FUNDEF _ ->
@@ -10424,9 +10416,3 @@ let convFile (path, f) =
(* export function without internal `relaxed' argument. *)
let areCompatibleTypes t1 t2 = areCompatibleTypes t1 t2
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index 61b53f17a3c1c0a7674d056dcaa7efc433e8a981..1ef46b685b7ea640fac086d71229c8f65a397055 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -643,7 +643,7 @@ let lfEq = LogicMerging.create_eq_table 111 (* Logic functions *)
let ltEq = PlainMerging.create_eq_table 111 (* Logic types *)
let lcEq = PlainMerging.create_eq_table 111 (* Logic constructors *)
-let laEq = PlainMerging.create_eq_table 111 (* Axiomatics *)
+let laEq = PlainMerging.create_eq_table 111 (* Axiomatics & Modules *)
let llEq = PlainMerging.create_eq_table 111 (* Lemmas *)
let lvEq = VolatileMerging.create_eq_table 111
@@ -858,6 +858,9 @@ let rec global_annot_without_irrelevant_attributes ga =
| Daxiomatic(n,l,attr,loc) ->
Daxiomatic(n,List.map global_annot_without_irrelevant_attributes l,
drop_attributes_for_merge attr,loc)
+ | Dmodule(n,l,attr,drv,loc) ->
+ Dmodule(n,List.map global_annot_without_irrelevant_attributes l,
+ drop_attributes_for_merge attr,drv,loc)
| Dlemma (id,labs,typs,st,attr,loc) ->
Dlemma (id,labs,typs,st,drop_attributes_for_merge attr,loc)
| Dtype (lti,loc) ->
@@ -893,7 +896,11 @@ let rec global_annot_pass1 g =
if Option.is_some wvi then process_term_kind (x,W))
hs
| Daxiomatic(id,decls,_,l) ->
- ignore (PlainMerging.getNode laEq laSyn !currentFidx id (id,decls)
+ ignore (PlainMerging.getNode laEq laSyn !currentFidx id (id,decls,None)
+ (Some (l,!currentDeclIdx)));
+ List.iter global_annot_pass1 decls
+ | Dmodule(id,decls,_,drv,l) ->
+ ignore (PlainMerging.getNode laEq laSyn !currentFidx id (id,decls,drv)
(Some (l,!currentDeclIdx)));
List.iter global_annot_pass1 decls
| Dfun_or_pred (li,l) ->
@@ -1436,17 +1443,17 @@ let matchLogicCtor oldfidx oldpi fidx pi =
"invalid multiple logic constructors declarations %s" pi.ctor_name
(* ignores irrelevant attributes such as __fc_stdlib *)
-let matchLogicAxiomatic oldfidx (oldid,_ as oldnode) fidx (id,_ as node) =
+let matchLogicAxiomatic oldfidx (oldid,_,_ as oldnode) fidx (id,_,_ as node) =
let oldanode = PlainMerging.getNode laEq laSyn oldfidx oldid oldnode None in
let anode = PlainMerging.getNode laEq laSyn fidx id node None in
if oldanode != anode then begin
- let _, oldax = oldanode.ndata in
+ let _, oldax, odrv = oldanode.ndata in
let oldaidx = oldanode.nfidx in
- let _, ax = anode.ndata in
+ let _, ax, drv = anode.ndata in
let aidx = anode.nfidx in
let ax = List.map global_annot_without_irrelevant_attributes ax in
let oldax = List.map global_annot_without_irrelevant_attributes oldax in
- if Logic_utils.is_same_axiomatic oldax ax then begin
+ if Logic_utils.is_same_axiomatic oldax ax && odrv = drv then begin
if oldaidx < aidx then
anode.nrep <- oldanode.nrep
else
@@ -2194,7 +2201,22 @@ class renameInlineVisitorClass = object(self)
end
let renameInlinesVisitor = new renameInlineVisitorClass
-let rec logic_annot_pass2 ~in_axiomatic g a =
+type context = Toplevel of global | InAxiomatic | InModule
+
+let errorContext context toplevel =
+ Kernel.abort ~current:true "%s not allowed inside %s" toplevel context
+
+let checkContext ~toplevel = function
+ | Toplevel _ -> ()
+ | InAxiomatic -> errorContext "axiomatic" toplevel
+ | InModule -> errorContext "module" toplevel
+
+let pushGlobal ?toplevel = function
+ | Toplevel g -> mergePushGlobals (visitCilGlobal renameVisitor g)
+ | InAxiomatic -> Option.iter (errorContext "axiomatic") toplevel
+ | InModule -> Option.iter (errorContext "module") toplevel
+
+let rec logic_annot_pass2 context a =
let open Current_loc.Operators in
let<> UpdatedCurrentLoc = Cil_datatype.Global_annotation.loc a in
match a with
@@ -2202,8 +2224,7 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
begin
match LogicMerging.findReplacement true lfEq !currentFidx li with
| None ->
- if not in_axiomatic then
- mergePushGlobals (visitCilGlobal renameVisitor g);
+ pushGlobal context ;
Logic_utils.add_logic_function li;
| Some _ -> ()
(* FIXME: should we perform same actions
@@ -2213,27 +2234,23 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
begin
match PlainMerging.findReplacement true ltEq !currentFidx t.lt_name with
| None ->
- if not in_axiomatic then
- mergePushGlobals (visitCilGlobal renameVisitor g);
- let def =
- (PlainMerging.find_eq_table ltEq (!currentFidx,t.lt_name)).ndata
- in
+ pushGlobal context ;
+ let node = PlainMerging.find_eq_table ltEq (!currentFidx,t.lt_name) in
+ let def = node.ndata in
Logic_env.add_logic_type t.lt_name def;
- (match def.lt_def with
- | Some (LTsum l) ->
- List.iter (fun c -> Logic_env.add_logic_ctor c.ctor_name c) l
- | Some (LTsyn _)
- | None -> ()
- )
+ begin
+ match def.lt_def with
+ | Some (LTsum l) ->
+ List.iter (fun c -> Logic_env.add_logic_ctor c.ctor_name c) l
+ | Some (LTsyn _) | None -> ()
+ end
| Some _ -> ()
end
| Dinvariant (li, _) ->
begin
match LogicMerging.findReplacement true lfEq !currentFidx li with
| None ->
- if in_axiomatic then Kernel.abort ~current:true
- "nested axiomatics are not allowed in ACSL";
- mergePushGlobals (visitCilGlobal renameVisitor g);
+ pushGlobal ~toplevel:"invariant" context ;
Logic_utils.add_logic_function
(LogicMerging.find_eq_table lfEq (!currentFidx,li)).ndata
| Some _ -> ()
@@ -2242,9 +2259,7 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
begin
match LogicMerging.findReplacement true lfEq !currentFidx n with
| None ->
- let g = visitCilGlobal renameVisitor g in
- if not in_axiomatic then
- mergePushGlobals g;
+ pushGlobal context ;
Logic_utils.add_logic_function
(LogicMerging.find_eq_table lfEq (!currentFidx,n)).ndata
| Some _ -> ()
@@ -2275,9 +2290,8 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
(!currentFidx,(mf'.mi_name,mf'.mi_base_type))
my_node';
end;
- if not in_axiomatic then begin
- mergePushGlobals [GAnnot (Dmodel_annot(mf',l),l)];
- end;
+ checkContext ~toplevel:"model annotation" context ;
+ mergePushGlobal (GAnnot (Dmodel_annot(mf',l),l)) ;
Logic_env.add_model_field
(ModelMerging.find_eq_table
mfEq (!currentFidx,(mf'.mi_name,mf'.mi_base_type))).ndata;
@@ -2286,9 +2300,7 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
| Dlemma (n, _, _, _, _, _) ->
begin
match PlainMerging.findReplacement true llEq !currentFidx n with
- None ->
- if not in_axiomatic then
- mergePushGlobals (visitCilGlobal renameVisitor g)
+ None -> pushGlobal context
| Some _ -> ()
end
| Dvolatile(vi, rd, wr, attr, loc) ->
@@ -2335,28 +2347,37 @@ let rec logic_annot_pass2 ~in_axiomatic g a =
let no_drop, full_representative, only_reads, only_writes =
List.fold_left check_one_location (true,[],[],[]) vi
in
- if no_drop then mergePushGlobals (visitCilGlobal renameVisitor g)
+ if no_drop then pushGlobal ~toplevel:"volatile" context
else begin
+ checkContext ~toplevel:"volatile" context;
push_volatile full_representative rd wr;
if Option.is_some rd then push_volatile only_reads rd None;
if Option.is_some wr then push_volatile only_writes None wr
end
| Daxiomatic(n, l, _, _) ->
+ begin
+ match PlainMerging.findReplacement true laEq !currentFidx n with
+ | None ->
+ pushGlobal context ;
+ List.iter (logic_annot_pass2 InAxiomatic) l
+ | Some _ -> ()
+ end
+ | Dmodule(n, l, _, _, _) ->
begin
match PlainMerging.findReplacement true laEq !currentFidx n with
None ->
- if in_axiomatic then Kernel.abort ~current:true
- "nested axiomatics are not allowed in ACSL";
- mergePushGlobals (visitCilGlobal renameVisitor g);
- List.iter (logic_annot_pass2 ~in_axiomatic:true g) l
+ pushGlobal context ;
+ List.iter (logic_annot_pass2 InModule) l
| Some _ -> ()
end
| Dextended(ext, _, _) ->
- (match ExtMerging.findReplacement true extEq !currentFidx ext with
- | None -> mergePushGlobals (visitCilGlobal renameVisitor g);
- | Some _ -> ())
+ begin
+ match ExtMerging.findReplacement true extEq !currentFidx ext with
+ | None -> pushGlobal context
+ | Some _ -> ()
+ end
-let global_annot_pass2 g a = logic_annot_pass2 ~in_axiomatic:false g a
+let global_annot_pass2 g a = logic_annot_pass2 (Toplevel g) a
(* sm: First attempt at a semantic checksum for function bodies.
* Ideally, two function's checksums would be equal only when their
diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index db1b59e51d962777c8b56d9aee89a83b27ae068d..94d46e207b81500931182d815ab84594a64f5992 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -1690,7 +1690,7 @@ let rec remove_declared_global_annot logic_vars = function
| Dvolatile _ | Dtype _ | Dlemma _ | Dmodel_annot _
| Dextended _ ->
logic_vars
- | Daxiomatic (_,l,_, _) ->
+ | Daxiomatic (_,l,_,_) | Dmodule (_,l,_,_,_) ->
List.fold_left remove_declared_global_annot logic_vars l
let remove_declared_global c_vars logic_vars = function
@@ -1806,7 +1806,8 @@ let logic_info_of_global s =
let rec check_one acc = function
| Dfun_or_pred(li,_) | Dinvariant(li,_) | Dtype_annot(li,_) ->
check_logic_info li acc
- | Daxiomatic (_,l, _, _) -> List.fold_left check_one acc l
+ | Daxiomatic (_,l, _, _) | Dmodule (_,l, _, _, _) ->
+ List.fold_left check_one acc l
| Dtype _ | Dvolatile _ | Dlemma _ | Dmodel_annot _
| Dextended _
-> acc
diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml
index e144f4363dab7a06b41b6e72937efaf958a754b0..b29782e0d6ccd48ac59fba7baeb9ecfcef499a44 100644
--- a/src/kernel_services/ast_data/cil_types.ml
+++ b/src/kernel_services/ast_data/cil_types.ml
@@ -1800,6 +1800,8 @@ and global_annotation =
* attributes * location
(** associated terms, reading function, writing function *)
| Daxiomatic of string * global_annotation list * attributes * location
+ (** last string option is the external importer responsible for the module *)
+ | Dmodule of string * global_annotation list * attributes * string option * location
| Dtype of logic_type_info * location (** declaration of a logic type. *)
| Dlemma of
string * logic_label list * string list *
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index 1e5f0f1fdd9386c51f91aed243da5b9cc0b87773..d609dca1c2bb1e3d0a3f18f341d3ca9569974c43 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -123,6 +123,12 @@ and identified_axiomatic = {
iax_attrs : attributes;
}
+and identified_module = {
+ im_name : string;
+ im_props : identified_property list;
+ im_attrs : attributes;
+}
+
and identified_lemma = {
il_name : string;
il_labels : logic_label list;
@@ -161,6 +167,7 @@ and identified_property =
| IPPredicate of identified_predicate
| IPExtended of identified_extended
| IPAxiomatic of identified_axiomatic
+ | IPModule of identified_module
| IPLemma of identified_lemma
| IPBehavior of identified_behavior
| IPComplete of identified_complete
@@ -234,7 +241,7 @@ let get_kinstr = function
| IPFrom {if_kinstr=ki}
| IPReachable {ir_kinstr=ki}
| IPDecrease {id_kinstr=ki} -> ki
- | IPAxiomatic _
+ | IPAxiomatic _ | IPModule _
| IPLemma _ -> Kglobal
| IPOther {io_loc} -> ki_of_o_loc io_loc
| IPExtended {ie_loc} -> ki_of_e_loc ie_loc
@@ -261,7 +268,7 @@ let get_kf = function
| IPFrom {if_kf=kf}
| IPDecrease {id_kf=kf}
| IPPropertyInstance {ii_kf=kf} -> Some kf
- | IPAxiomatic _
+ | IPAxiomatic _ | IPModule _
| IPLemma _ -> None
| IPReachable {ir_kf} -> ir_kf
| IPExtended {ie_loc} -> kf_of_loc_e ie_loc
@@ -271,9 +278,9 @@ let get_kf = function
let get_ir p =
let get_pp = function
| IPPredicate {ip_kind = PKRequires _ | PKAssumes _ | PKTerminates }
- | IPAxiomatic _ | IPLemma _ | IPComplete _ | IPDisjoint _ | IPCodeAnnot _
- | IPAllocation _ | IPDecrease _ | IPPropertyInstance _ | IPOther _
- | IPTypeInvariant _ | IPGlobalInvariant _
+ | IPAxiomatic _ | IPModule _ | IPLemma _ | IPComplete _ | IPDisjoint _
+ | IPCodeAnnot _ | IPAllocation _ | IPDecrease _ | IPPropertyInstance _
+ | IPOther _ | IPTypeInvariant _ | IPGlobalInvariant _
-> Before
| IPPredicate _ | IPAssigns _ | IPFrom _ | IPExtended _ | IPBehavior _
-> After
@@ -302,6 +309,7 @@ let rec get_names = function
| IPPredicate ip -> (Logic_const.pred_of_id_pred ip.ip_pred).pred_name
| IPExtended { ie_ext = {ext_name = name} }
| IPAxiomatic { iax_name = name }
+ | IPModule { im_name = name }
| IPLemma { il_name = name }
| IPBehavior { ib_bhv = {b_name = name} }
| IPTypeInvariant { iti_name = name }
@@ -355,6 +363,10 @@ let rec location = function
(match iax_props with
| [] -> Cil_datatype.Location.unknown
| p :: _ -> location p)
+ | IPModule {im_props} ->
+ (match im_props with
+ | [] -> Cil_datatype.Location.unknown
+ | p :: _ -> location p)
| IPLemma {il_loc} -> il_loc
| IPExtended {ie_ext={ext_loc}} -> ext_loc
| IPOther {io_loc} -> loc_of_loc_o io_loc
@@ -388,6 +400,7 @@ let get_behavior = function
| IPAssigns {ias_bhv=Id_loop _}
| IPFrom {if_bhv=Id_loop _}
| IPAxiomatic _
+ | IPModule _
| IPExtended _
| IPLemma _
| IPCodeAnnot _
@@ -423,6 +436,7 @@ let get_for_behaviors = function
end
| IPAxiomatic _
+ | IPModule _
| IPExtended _
| IPLemma _
| IPComplete _
@@ -457,7 +471,7 @@ let rec has_status = function
| IPCodeAnnot {ica_ca={annot_content}} -> has_status_ca annot_content
| IPPropertyInstance {ii_ip} -> has_status ii_ip
| IPOther _ | IPReachable _
- | IPAxiomatic _ | IPBehavior _
+ | IPAxiomatic _ | IPModule _ | IPBehavior _
| IPDisjoint _ | IPComplete _
| IPAssigns _ | IPFrom _
| IPAllocation _ | IPDecrease _ | IPLemma _
@@ -482,6 +496,7 @@ let rec pretty_ip fmt = function
Cil_printer.pp_identified_predicate ip_pred
| IPExtended {ie_ext} -> Cil_printer.pp_extended fmt ie_ext
| IPAxiomatic {iax_name} -> Format.fprintf fmt "axiomatic@ %s" iax_name
+ | IPModule {im_name} -> Format.fprintf fmt "module@ %s" im_name
| IPLemma {il_name; il_pred} ->
Format.fprintf fmt "%a@ %s"
Cil_printer.pp_lemma_kind il_pred.tp_kind il_name
@@ -546,7 +561,8 @@ let rec hash_ip =
in
function
| IPPredicate {ip_pred=x} -> Hashtbl.hash (1, x.ip_id)
- | IPAxiomatic {iax_name=x} -> Hashtbl.hash (3, (x:string))
+ | IPAxiomatic {iax_name=x}
+ | IPModule {im_name=x} -> Hashtbl.hash (3, (x:string))
| IPLemma {il_name=x} -> Hashtbl.hash (4, (x:string))
| IPCodeAnnot {ica_ca=ca} -> Hashtbl.hash (5, ca.annot_id)
| IPComplete {ic_kf=f; ic_kinstr=ki; ic_bhvs=y; ic_active=x} ->
@@ -637,6 +653,7 @@ include Datatype.Make_with_collections
| IPExtended {ie_ext={ext_id=i1}}, IPExtended {ie_ext={ext_id=i2}} ->
Datatype.Int.equal i1 i2
| IPAxiomatic {iax_name=s1}, IPAxiomatic {iax_name=s2}
+ | IPModule {im_name=s1}, IPModule {im_name=s2}
| IPTypeInvariant {iti_name=s1}, IPTypeInvariant {iti_name=s2}
| IPGlobalInvariant {igi_name=s1}, IPGlobalInvariant {igi_name=s2}
| IPLemma {il_name=s1}, IPLemma {il_name=s2} ->
@@ -676,7 +693,7 @@ include Datatype.Make_with_collections
IPPropertyInstance {ii_kf=kf2;ii_stmt=s2;ii_ip=ip2} ->
Kernel_function.equal kf1 kf2 &&
Stmt.equal s1 s2 && equal ip1 ip2
- | (IPPredicate _ | IPExtended _ | IPAxiomatic _ | IPLemma _
+ | (IPPredicate _ | IPExtended _ | IPAxiomatic _ | IPModule _ | IPLemma _
| IPCodeAnnot _ | IPComplete _ | IPDisjoint _ | IPAssigns _
| IPFrom _ | IPDecrease _ | IPBehavior _ | IPReachable _
| IPAllocation _ | IPOther _ | IPPropertyInstance _
@@ -736,6 +753,7 @@ include Datatype.Make_with_collections
else
n
| IPAxiomatic {iax_name=s1}, IPAxiomatic {iax_name=s2}
+ | IPModule {im_name=s1}, IPModule {im_name=s2}
| IPTypeInvariant {iti_name=s1}, IPTypeInvariant {iti_name=s2}
| IPGlobalInvariant {igi_name=s1}, IPGlobalInvariant {igi_name=s2}
| IPLemma {il_name=s1}, IPLemma {il_name=s2} ->
@@ -754,7 +772,7 @@ include Datatype.Make_with_collections
if c <> 0 then c else compare ip1 ip2
| (IPPredicate _ | IPExtended _ | IPCodeAnnot _ | IPBehavior _ | IPComplete _ |
IPDisjoint _ | IPAssigns _ | IPFrom _ | IPDecrease _ |
- IPReachable _ | IPAxiomatic _ | IPLemma _ |
+ IPReachable _ | IPAxiomatic _ | IPModule _ | IPLemma _ |
IPOther _ | IPAllocation _ | IPPropertyInstance _ |
IPTypeInvariant _ | IPGlobalInvariant _) as x, y ->
let nb = function
@@ -762,19 +780,20 @@ include Datatype.Make_with_collections
| IPAssigns _ -> 2
| IPDecrease _ -> 3
| IPAxiomatic _ -> 5
- | IPLemma _ -> 6
- | IPCodeAnnot _ -> 7
- | IPComplete _ -> 8
- | IPDisjoint _ -> 9
- | IPFrom _ -> 10
- | IPBehavior _ -> 11
- | IPReachable _ -> 12
- | IPAllocation _ -> 13
- | IPOther _ -> 14
- | IPPropertyInstance _ -> 15
- | IPTypeInvariant _ -> 16
- | IPGlobalInvariant _ -> 17
- | IPExtended _ -> 18
+ | IPModule _ -> 6
+ | IPLemma _ -> 7
+ | IPCodeAnnot _ -> 8
+ | IPComplete _ -> 9
+ | IPDisjoint _ -> 10
+ | IPFrom _ -> 11
+ | IPBehavior _ -> 12
+ | IPReachable _ -> 13
+ | IPAllocation _ -> 14
+ | IPOther _ -> 15
+ | IPPropertyInstance _ -> 16
+ | IPTypeInvariant _ -> 17
+ | IPGlobalInvariant _ -> 18
+ | IPExtended _ -> 19
in
Datatype.Int.compare (nb x) (nb y)
@@ -793,6 +812,7 @@ module Ordered_by_function = Datatype.Make_with_collections(
let cmp_kind p1 p2 =
let nb = function
| IPAxiomatic _ -> 1
+ | IPModule _ -> 2
| IPLemma _ -> 3
| IPTypeInvariant _ -> 4
| IPGlobalInvariant _ -> 5
@@ -822,6 +842,7 @@ module Ordered_by_function = Datatype.Make_with_collections(
let rec cmp_same_kind p1 p2 =
match (p1,p2) with
| IPAxiomatic { iax_name = n1 }, IPAxiomatic { iax_name = n2 }
+ | IPModule { im_name = n1 }, IPModule { im_name = n2 }
| IPLemma { il_name = n1 }, IPLemma { il_name = n2 }
| IPTypeInvariant { iti_name = n1 }, IPTypeInvariant { iti_name = n2 }
| IPGlobalInvariant { igi_name = n1 },
@@ -910,7 +931,8 @@ let rec short_pretty fmt p = match p with
| IPExtended {ie_ext={ext_name}} -> Format.pp_print_string fmt ext_name
| IPLemma {il_name=n}
| IPTypeInvariant {iti_name=n} | IPGlobalInvariant {igi_name=n}
- | IPAxiomatic {iax_name=n} -> Format.pp_print_string fmt n
+ | IPAxiomatic {iax_name=n} | IPModule {im_name=n} ->
+ Format.pp_print_string fmt n
| IPBehavior {ib_kf; ib_bhv={b_name}} ->
Format.fprintf fmt "behavior %s in function %a"
b_name Kernel_function.pretty ib_kf
@@ -1031,6 +1053,11 @@ let rec pretty_debug fmt = function
Cil_types_debug.pp_string iax_name
(Cil_types_debug.pp_list pretty_debug) iax_props
Cil_types_debug.pp_attributes iax_attrs
+ | IPModule {im_name; im_props; im_attrs} ->
+ Format.fprintf fmt "IPModule(%a,%a,%a)"
+ Cil_types_debug.pp_string im_name
+ (Cil_types_debug.pp_list pretty_debug) im_props
+ Cil_types_debug.pp_attributes im_attrs
| IPLemma {il_name; il_labels; il_args; il_pred; il_attrs; il_loc} ->
Format.fprintf fmt "IPLemma(%a,%a,%a,%a,%a,%a)"
Cil_types_debug.pp_string il_name
@@ -1218,7 +1245,7 @@ struct
| IPReachable {ir_kf=Some kf; ir_kinstr=Kstmt s; ir_program_point=After} ->
[ K kf ; A "reachable_after" ; S s ]
- | IPAxiomatic _ -> []
+ | IPAxiomatic _ | IPModule _ -> []
| IPLemma {il_name=name; il_pred=p} ->
let a = Cil_printer.ident_of_lemma p.tp_kind in
[ A a ; A name ; P p.tp_statement ]
@@ -1493,6 +1520,9 @@ let ip_of_global_annotation a =
| Daxiomatic(iax_name, l, iax_attrs, _) ->
let iax_props = List.fold_left aux [] l in
IPAxiomatic {iax_name; iax_props; iax_attrs} :: (iax_props @ acc)
+ | Dmodule(im_name, l, im_attrs, _, _) ->
+ let im_props = List.fold_left aux [] l in
+ IPModule {im_name; im_props; im_attrs} :: (im_props @ acc)
| Dlemma(il_name, il_labels, il_args, il_pred, il_attrs, il_loc) ->
ip_lemma {il_name; il_labels; il_args; il_pred; il_attrs; il_loc} :: acc
| Dinvariant(l, igi_loc) ->
@@ -1529,9 +1559,3 @@ let ip_of_global_annotation_single a = match ip_of_global_annotation a with
| ip :: _ ->
(* the first one is the good one, see ip_of_global_annotation *)
Some ip
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli
index f957ff21d99f3e8d5abbc80724f86eebd5427c3e..caff84ad582905ad276a77da8d418315737e77e5 100644
--- a/src/kernel_services/ast_data/property.mli
+++ b/src/kernel_services/ast_data/property.mli
@@ -154,6 +154,12 @@ and identified_axiomatic = {
iax_attrs : attributes;
}
+and identified_module = {
+ im_name : string;
+ im_props : identified_property list;
+ im_attrs : attributes;
+}
+
and identified_lemma = {
il_name : string;
il_labels : logic_label list;
@@ -195,6 +201,7 @@ and identified_property = private
| IPPredicate of identified_predicate
| IPExtended of identified_extended
| IPAxiomatic of identified_axiomatic
+ | IPModule of identified_module
| IPLemma of identified_lemma
| IPBehavior of identified_behavior
| IPComplete of identified_complete
@@ -548,9 +555,3 @@ sig
(** returns the basename of the property. *)
end
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/ast_data/property_status.ml b/src/kernel_services/ast_data/property_status.ml
index 9edd052f73c7d3b92e52182c388f71f2313f4ae0..68a3b6b494fe0f93968fef7272277da1b6564bf9 100644
--- a/src/kernel_services/ast_data/property_status.ml
+++ b/src/kernel_services/ast_data/property_status.ml
@@ -405,7 +405,7 @@ let rec register ppt =
Property.pretty ppt
Project.pretty (Project.current ());
if Status.mem ppt then
- Kernel.fatal "trying to register twice property `%a'.\n\
+ Kernel.fatal "trying to register twice property @[<hov 2>'%a'@].@\n\
That is forbidden (kernel invariant broken)."
Property.pretty ppt;
let h = Emitter_with_properties.Hashtbl.create 7 in
@@ -525,7 +525,7 @@ and unsafe_emit_and_get e ~hyps ~auto ppt ?(distinct=false) s =
| Property.IPPredicate _ | Property.IPCodeAnnot _ | Property.IPComplete _
| Property.IPDisjoint _ | Property.IPAssigns _ | Property.IPFrom _
| Property.IPAllocation _ | Property.IPDecrease _ | Property.IPBehavior _
- | Property.IPAxiomatic _ | Property.IPLemma _
+ | Property.IPAxiomatic _ | Property.IPModule _ | Property.IPLemma _
| Property.IPTypeInvariant _ | Property.IPGlobalInvariant _
| Property.IPExtended _ ->
Kernel.fatal "unregistered property %a" Property.pretty ppt
@@ -693,7 +693,7 @@ and get_status ?(must_register=true) ppt =
| Property.IPPredicate _ | Property.IPCodeAnnot _ | Property.IPComplete _
| Property.IPDisjoint _ | Property.IPAssigns _ | Property.IPFrom _
| Property.IPDecrease _ | Property.IPAllocation _
- | Property.IPAxiomatic _ | Property.IPLemma _
+ | Property.IPAxiomatic _ | Property.IPModule _ | Property.IPLemma _
| Property.IPTypeInvariant _ | Property.IPGlobalInvariant _ ->
Kernel.fatal "trying to get status of unregistered property `%a'.\n\
That is forbidden (kernel invariant broken)."
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 1f1ea2fcb0cdaf437cda8ffc33285e3eaff6e061..783dad28f08bafc654b9b847330959e21c3eb1a1 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1263,9 +1263,9 @@ class cil_printer () = object (self)
method builtin_logic_info fmt bli =
fprintf fmt "%a" self#varname bli.bl_name
- method logic_type_info fmt s = fprintf fmt "%a" self#varname s.lt_name
+ method logic_type_info fmt s = self#logic_name fmt s.lt_name
- method logic_ctor_info fmt ci = fprintf fmt "%a" self#varname ci.ctor_name
+ method logic_ctor_info fmt ci = self#logic_name fmt ci.ctor_name
method initinfo fmt io =
match io.init with
@@ -2399,7 +2399,7 @@ class cil_printer () = object (self)
if Kernel.Unicode.get () then Utf8_logic.real else "real"
in
Format.fprintf fmt "%s%t" res pname
- | Ltype ({ lt_name = name},[]) when name = Utf8_logic.boolean->
+ | Ltype ({ lt_name = name},[]) when name = Utf8_logic.boolean ->
let res =
if Kernel.Unicode.get () then Utf8_logic.boolean else "boolean"
in
@@ -2415,7 +2415,7 @@ class cil_printer () = object (self)
fprintf fmt "@[@[<2>{@ %a@]}@]%a%t"
(Pretty_utils.pp_list ~sep:",@ " (self#logic_type None)) args
(self#logic_type None) rt pname
- | Lvar s -> fprintf fmt "%a%t" self#varname s pname
+ | Lvar s -> fprintf fmt "%s%t" s pname
method private name fmt s =
if needs_quote s then Format.fprintf fmt "\"%s\"" s
@@ -2537,7 +2537,7 @@ class cil_printer () = object (self)
(Pretty_utils.pp_list
~sep:",@ " ~pre:"@[<hov>" ~suf:"@]@;" self#term_node) l
| _ ->
- fprintf fmt "%a%a" self#varname ci.ctor_name
+ fprintf fmt "%a%a" self#logic_name ci.ctor_name
(Pretty_utils.pp_list ~pre:"(@[" ~suf:"@])" ~sep:",@ " self#term)
args)
| TLval lv -> fprintf fmt "%a" (self#term_lval_prec current_level) lv
@@ -2719,6 +2719,16 @@ class cil_printer () = object (self)
method term_lhost fmt (lh:term_lhost) =
self#term_lval fmt (lh, TNoOffset)
+ val module_stack : string Stack.t = Stack.create ()
+
+ method logic_name fmt a =
+ try
+ let prefix = Stack.top module_stack in
+ let shortname = Extlib.string_del_prefix prefix a in
+ self#varname fmt @@ Option.value ~default:a shortname
+ with Stack.Empty ->
+ self#varname fmt a
+
method logic_info fmt li = self#logic_var fmt li.l_var_info
method logic_var fmt v =
@@ -2729,7 +2739,7 @@ class cil_printer () = object (self)
| Some v -> Format.fprintf fmt "vid:%d, " v.vid);
Format.fprintf fmt "lvid:%d */" v.lv_id
end;
- self#varname fmt v.lv_name
+ self#logic_name fmt v.lv_name
method quantifiers fmt l =
Pretty_utils.pp_list ~sep:",@ "
@@ -3306,7 +3316,7 @@ class cil_printer () = object (self)
let old_lab = current_label in
fprintf fmt "@[<hv 2>@[<hov 1>%a %a%a%a:@]@ %t%a;@]@\n"
self#pp_lemma_kind pred.tp_kind
- self#varname name
+ self#logic_name name
self#labels labels
self#polyTypePrms tvars
(* pretty printing of lemma statement is done inside an environment
@@ -3320,7 +3330,7 @@ class cil_printer () = object (self)
| Dtype (ti,_) ->
fprintf fmt "@[<hv 2>@[%a %a%a%a;@]@\n"
self#pp_acsl_keyword "type"
- self#varname ti.lt_name self#polyTypePrms ti.lt_params
+ self#logic_name ti.lt_name self#polyTypePrms ti.lt_params
(fun fmt -> function
| None -> fprintf fmt "@]"
| Some d -> fprintf fmt " =@]@ %a" self#logic_type_def d)
@@ -3405,11 +3415,34 @@ class cil_printer () = object (self)
| Daxiomatic(id,decls,_attr, _) ->
(* attributes are meant to be purely internal for now. *)
fprintf fmt "@[<v 2>@[%a %s {@]@\n%a}@]@\n"
- self#pp_acsl_keyword "axiomatic"
- id
+ self#pp_acsl_keyword "axiomatic" id
(Pretty_utils.pp_list ~pre:"@[<v 0>" ~suf:"@]@\n" ~sep:"@\n"
self#global_annotation)
decls
+ | Dmodule(id, _, _, Some drv, _)
+ when not Kernel.(is_debug_key_enabled dkey_print_imported_modules) ->
+ fprintf fmt "@[<hov 2>%a %s: %s %a _ ;@]@\n"
+ self#pp_acsl_keyword "import" drv id
+ self#pp_acsl_keyword "\\as"
+ | Dmodule(id, decls, _attr, driver, _) ->
+ begin
+ (* attributes are meant to be purely internal for now. *)
+ fprintf fmt "@[<v 2>@[" ;
+ if Kernel.(is_debug_key_enabled dkey_print_imported_modules) then
+ Option.iter (fprintf fmt "// import %s:@\n") driver ;
+ fprintf fmt "%a %a {@]"
+ self#pp_acsl_keyword "module" self#logic_name id ;
+ try
+ Stack.push (id ^ "::") module_stack ;
+ fprintf fmt "@\n%a}@]@\n"
+ (Pretty_utils.pp_list ~pre:"@[<v 0>" ~suf:"@]@\n" ~sep:"@\n"
+ self#global_annotation)
+ decls ;
+ ignore @@ Stack.pop module_stack ;
+ with err ->
+ ignore @@ Stack.pop module_stack ;
+ raise err
+ end
| Dextended (e,_attr,_) -> self#extended fmt e
method logic_type_def fmt = function
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index 12e2557c25673e2f412019ae8ad0207db1f2a6f4..28e5f9448921c6a07afd5f6ef8cc835e82c7a3fb 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -971,6 +971,10 @@ and pp_global_annotation fmt = function
Format.fprintf fmt "Daxiomatic(%a,%a,%a,%a)" pp_string string
(pp_list pp_global_annotation) global_annotation_list
pp_attributes attributes pp_location location
+ | Dmodule(string,global_annotation_list,attributes,driver,location) ->
+ Format.fprintf fmt "Dmodule(%a,%a,%a,%a,%a)" pp_string string
+ (pp_list pp_global_annotation) global_annotation_list
+ pp_attributes attributes (pp_option pp_string) driver pp_location location
| Dtype(logic_type_info,location) ->
Format.fprintf fmt "Dtype(%a,%a)" pp_logic_type_info logic_type_info pp_location location
| Dlemma(string,logic_label_list,string_list,predicate,attributes,location) ->
diff --git a/src/kernel_services/ast_printing/description.ml b/src/kernel_services/ast_printing/description.ml
index ab7ccf849a401267dd85d551593fafb5c2775f68..b827571399fcef999bf410cf17b82740927dad98 100644
--- a/src/kernel_services/ast_printing/description.ml
+++ b/src/kernel_services/ast_printing/description.ml
@@ -228,6 +228,7 @@ let rec pp_prop kfopt kiopt kloc fmt = function
| IPTypeInvariant {iti_name=s} -> Format.fprintf fmt "Type invariant '%s'" s
| IPGlobalInvariant {igi_name=s} -> Format.fprintf fmt "Global invariant '%s'" s
| IPAxiomatic {iax_name=s} -> Format.fprintf fmt "Axiomatic '%s'" s
+ | IPModule {im_name=s} -> Format.fprintf fmt "Module '%s'" s
| IPOther {io_name=s;io_loc=le} ->
Format.fprintf fmt "%a%a" pp_capitalize s (pp_other_loc kfopt kiopt kloc) le
| IPPredicate {ip_kind; ip_kf; ip_kinstr=Kglobal; ip_pred} ->
@@ -497,7 +498,8 @@ let loop_order = function
let rec ip_order = function
| IPAxiomatic {iax_name=a} -> [I 0;S a]
- | IPLemma {il_name=a} -> [I 1;S a]
+ | IPModule {im_name=a} -> [I 1;S a]
+ | IPLemma {il_name=a} -> [I 2;S a]
| IPOther {io_name=s;io_loc=OLContract kf} -> [I 3;F kf;S s]
| IPOther {io_name=s;io_loc=OLStmt (kf, stmt)} -> [I 4;F kf;K (Kstmt stmt);S s]
| IPOther {io_name=s;io_loc=OLGlob _} -> [I 5; S s]
diff --git a/src/kernel_services/ast_printing/logic_print.ml b/src/kernel_services/ast_printing/logic_print.ml
index aeba051d5cd8d428079a2888c9794c4bc94ddbf6..1baf4f4f3d24ae5afca9c1fcf72f2d4c5b073b7d 100644
--- a/src/kernel_services/ast_printing/logic_print.ml
+++ b/src/kernel_services/ast_printing/logic_print.ml
@@ -75,8 +75,7 @@ let rec print_logic_type name fmt typ =
| LTenum s -> fprintf fmt "enum@ %s%t" s pname
| LTstruct s -> fprintf fmt "struct@ %s%t" s pname
| LTnamed (s,l) ->
- fprintf fmt "%s%a%t"
- s
+ fprintf fmt "%s%a%t" s
(pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@]>"
(print_logic_type None)) l
pname
@@ -370,9 +369,18 @@ let rec print_decl fmt d =
(pp_list ~pre:"{@[" ~sep:",@ " ~suf:"@]}" pp_print_string) labels
(pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@>}" pp_print_string) tvar
print_lexpr body.tp_statement
- | LDaxiomatic (s,d) ->
- fprintf fmt "@[<2>axiomatic@ %s@ {@\n%a@]@\n}" s
- (pp_list ~sep:"@\n" print_decl) d
+ | LDaxiomatic (name,ds) ->
+ fprintf fmt "@[<2>axiomatic@ %s@ {@\n%a@]@\n}" name
+ (pp_list ~sep:"@\n" print_decl) ds
+ | LDmodule (name,ds) ->
+ fprintf fmt "@[<2>module@ %s@ {@\n%a@]@\n}" name
+ (pp_list ~sep:"@\n" print_decl) ds
+ | LDimport (drv,mId,asId) ->
+ fprintf fmt "@[<2>import" ;
+ Option.iter (fprintf fmt "@ %s:") drv ;
+ fprintf fmt "@ %s" mId ;
+ Option.iter (fprintf fmt "@ \\as %s") asId ;
+ fprintf fmt ";@]@\n}"
| LDinvariant (s,e) ->
fprintf fmt "@[<2>invariant@ %s:@ %a;@]" s print_lexpr e
| LDtype_annot ty -> print_type_annot fmt ty
@@ -483,8 +491,3 @@ let print_code_annot fmt ca =
print_behaviors bhvs
(if is_loop then " loop " else "")
print_extension e
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/ast_printing/printer_api.ml b/src/kernel_services/ast_printing/printer_api.ml
index 7a83f84d9d6c0059e118960feb089285f677611c..1066405ee1370032b09b63f49fdc32b550ddd261 100644
--- a/src/kernel_services/ast_printing/printer_api.ml
+++ b/src/kernel_services/ast_printing/printer_api.ml
@@ -275,6 +275,12 @@ class type extensible_printer_type = object
method logic_type_info: Format.formatter -> logic_type_info -> unit
method logic_ctor_info: Format.formatter -> logic_ctor_info -> unit
method logic_var: Format.formatter -> logic_var -> unit
+
+ (** logic names, with full module path if needed (eg. "foo::bar::jazz")
+ Defaults to [self#varname], with the full name truncated to the currently
+ opened module, if any. *)
+ method logic_name: Format.formatter -> string -> unit
+
method quantifiers: Format.formatter -> quantifiers -> unit
method predicate_node: Format.formatter -> predicate_node -> unit
method predicate: Format.formatter -> predicate -> unit
diff --git a/src/kernel_services/ast_queries/acsl_extension.ml b/src/kernel_services/ast_queries/acsl_extension.ml
index 5b75815f9c2bc165e44e407e5c74764a7b86222e..6fe88ccaccfe1ad9155a770c8d108e31b5911148 100644
--- a/src/kernel_services/ast_queries/acsl_extension.ml
+++ b/src/kernel_services/ast_queries/acsl_extension.ml
@@ -73,6 +73,8 @@ type extension_common = {
plugin: string;
is_same_ext: extension_same;
}
+type extension_module_importer =
+ module_builder -> location -> string list -> unit
let default_printer printer fmt = function
| Ext_id i -> Format.fprintf fmt "%d" i
@@ -132,6 +134,9 @@ module Extensions = struct
(*hash table for status, preprocessor and typer of block extensions*)
let ext_block_tbl = Hashtbl.create 5
+ (*hash table for module importers*)
+ let ext_module_importer = Hashtbl.create 5
+
let find_single name :extension_single =
try Hashtbl.find ext_single_tbl name with Not_found ->
Kernel.fatal ~current:true "unsupported clause of name '%s'" name
@@ -144,6 +149,10 @@ module Extensions = struct
try Hashtbl.find ext_block_tbl name with Not_found ->
Kernel.fatal ~current:true "unsupported clause of name '%s'" name
+ let find_importer name :extension_module_importer =
+ try Hashtbl.find ext_module_importer name with Not_found ->
+ Kernel.fatal ~current:true "unsupported module importer '%s'" name
+
(* [Logic_lexer] can ask for something that is not a category, which is not
a fatal error. *)
let category name = (Hashtbl.find ext_tbl name).category
@@ -184,6 +193,14 @@ module Extensions = struct
Hashtbl.add ext_tbl name info2
end
+ let register_module_importer name loader =
+ if Hashtbl.mem ext_module_importer name then
+ Kernel.warning ~wkey:Kernel.wkey_acsl_extension
+ "Trying to register module importer %s twice. Ignoring second importer"
+ name
+ else
+ Hashtbl.add ext_module_importer name loader
+
let preprocess name = (find_single name).preprocessor
let preprocess_block name = (find_block name).preprocessor
@@ -264,6 +281,8 @@ let register_code_annot_next_loop =
Extensions.register (Ext_code_annot Ext_next_loop)
let register_code_annot_next_both =
Extensions.register (Ext_code_annot Ext_next_both)
+let register_module_importer =
+ Extensions.register_module_importer
(* Setup global references *)
@@ -278,7 +297,8 @@ let () =
Logic_typing.set_extension_handler
~is_extension: Extensions.is_extension
~typer: Extensions.typing
- ~typer_block: Extensions.typing_block ;
+ ~typer_block: Extensions.typing_block
+ ~importer: Extensions.find_importer;
Cil.set_extension_handler
~visit: Extensions.visit ;
Cil_printer.set_extension_handler
diff --git a/src/kernel_services/ast_queries/acsl_extension.mli b/src/kernel_services/ast_queries/acsl_extension.mli
index 05fc80c89312da72e64f2edaedacae7a9aefd5c9..937f8c65cb097bdedc77aaf615c28ab6c662da90 100644
--- a/src/kernel_services/ast_queries/acsl_extension.mli
+++ b/src/kernel_services/ast_queries/acsl_extension.mli
@@ -58,6 +58,9 @@ type extension_printer =
type extension_same =
acsl_extension_kind -> acsl_extension_kind -> Ast_diff.is_same_env -> bool
+type extension_module_importer =
+ module_builder -> location -> string list -> unit
+
(** type of functions that register new ACSL extensions to be used in place of
various kinds of ACSL annotations.
@@ -97,20 +100,20 @@ type extension_same =
status or not.
Here is a basic example:
- [
- let count = ref 0
- let foo_typer typing_context loc = function
- | p :: [] ->
- Ext_preds
- [ (typing_context.type_predicate
- typing_context
- (typing_context.post_state [Normal])
- p)])
- | [] -> let id = !count in incr count; Ext_id id
- | _ -> typing_context.error loc "expecting a predicate after keyword FOO"
- let () =
- Acsl_extension.register_behavior ~plugin:"myplugin" "FOO" foo_typer false
- ]
+ {[
+ let count = ref 0
+ let foo_typer ctxt loc = function
+ | [] ->
+ let id = !count in incr count;
+ Ext_id id
+ | [p] ->
+ Ext_preds [ctxt.type_predicate ctxt (ctxt.post_state [Normal]) p]
+ | _ ->
+ typing_context.error loc "expecting a predicate after keyword FOO"
+
+ let () =
+ Acsl_extension.register_behavior ~plugin:"myplugin" "FOO" foo_typer false
+ ]}
@before 29.0-Copper parameters [plugin] and [is_same_ext] were not present
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf>
*)
@@ -153,3 +156,28 @@ val register_code_annot_next_loop: register_extension
(** Registers extension both for code and loop annotations. *)
val register_code_annot_next_both: register_extension
+
+(**
+ Module importer extensions allow extending the import clause with external
+ loaders. For instance, consider the following declaration:
+ {[
+ //@ import A: foo::bar;
+ ]}
+
+ This import clause will invoke an external module importer named ["A"]
+ provided it has been properly registered.
+
+ A module importer extension is a function that receives a [module_builder]
+ parameter to be populated with contents of the module. The module name is
+ provided as list (See {!Logic_utils.longident} for details).
+
+ New type and function symbols shall be created with `Cil.make_xxx` functions.
+ The registered symbols {i will} be automatically prefixed with the name of
+ the imported module if necessary.
+
+ The register module importer function might be invoked several times,
+ typically when a given module is imported from several files. Although
+ external module importers might use memoization internally, the provided
+ module builder shall be populated on every call.
+*)
+val register_module_importer : string -> extension_module_importer -> unit
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index 9dc42b8d8cfa752ef4fa4d1e0c7d7cc3ce097da3..7a92019e1c3fad9103ffc8be607821b8330f2bb6 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -1517,8 +1517,10 @@ let rec gannot_correspondence =
| Dvolatile _ -> ()
(* reading and writing function themselves will be checked elsewhere. *)
- | Daxiomatic(_,l,_,_) ->
+ | 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.ml b/src/kernel_services/ast_queries/cil.ml
index 1b3ace6387f1f46102ea851ef3dc07653c483e40..4aca4612649883b0cf76235bf72965e323d5e18f 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -428,7 +428,7 @@ let attributeHash: (string, attributeClass) Hashtbl.t =
"selectany"; "allocate"; "nothrow"; "novtable"; "property";
"uuid"; "align" ];
List.iter (fun a -> Hashtbl.add table a (AttrFunType false))
- [ "format"; "regparm"; "longcall"; "noinline"; "always_inline";];
+ [ "format"; "regparm"; "longcall"; "noinline"; "always_inline"; ];
List.iter (fun a -> Hashtbl.add table a (AttrFunType true))
[ "stdcall";"cdecl"; "fastcall"; "noreturn"];
List.iter (fun a -> Hashtbl.add table a AttrType)
@@ -1916,12 +1916,13 @@ and childrenAnnotation vis a =
Dvolatile(tset',rvi',wvi',attr',loc)
else a
| Daxiomatic(id,l,attr,loc) ->
- (*
- Format.eprintf "cil.visitCilAnnotation on axiomatic %s@." id;
- *)
let l' = Extlib.map_no_copy (visitCilAnnotation vis) l in
let attr' = visitCilAttributes vis attr in
if l' != l || attr != attr' then Daxiomatic(id,l',attr',loc) else a
+ | Dmodule(id,l,attr,drv,loc) ->
+ let l' = Extlib.map_no_copy (visitCilAnnotation vis) l in
+ let attr' = visitCilAttributes vis attr in
+ if l' != l || attr != attr' then Dmodule(id,l',attr',drv,loc) else a
| Dextended (e,attr,loc) ->
let e' = visitCilExtended vis e in
let attr' = visitCilAttributes vis attr in
@@ -4132,7 +4133,7 @@ and bitsSizeOf t =
raise
(SizeOfError
(Format.sprintf "abstract type '%s'" (compFullName comp), t))
- | TComp ({cfields=Some[]}, _) when acceptEmptyCompinfo () ->
+ | TComp ({cfields=Some[]}, _) when acceptEmptyCompinfo() ->
find_sizeof t (fun () -> t,0)
| TComp ({cfields=Some[]} as comp,_) ->
find_sizeof t
@@ -5254,7 +5255,7 @@ let mapGlobals (fl: file)
let global_annotation_attributes = function
| Dfun_or_pred ({l_var_info = { lv_attr }}, _) -> lv_attr
| Dvolatile (_,_,_,attrs,_) -> attrs
- | Daxiomatic (_,_,attrs,_) -> attrs
+ | Daxiomatic (_,_,attrs,_) | Dmodule(_,_,attrs,_,_) -> attrs
| Dtype ({ lt_attr }, _) -> lt_attr
| Dlemma (_,_,_,_,attrs,_) -> attrs
| Dinvariant ({l_var_info = { lv_attr }}, _) -> lv_attr
@@ -6693,14 +6694,14 @@ let rec has_flexible_array_member t =
let is_flexible_array t =
match unrollType t with
| TArray (_, None, _) -> true
- | TArray (_, Some z, _) -> (msvcMode () || gccMode ()) && isZero z
+ | TArray (_, Some z, _) -> (msvcMode() || gccMode()) && isZero z
| _ -> false
in
match unrollType t with
| TComp ({ cfields = Some ((_::_) as l) },_) ->
let last = (Extlib.last l).ftype in
is_flexible_array last ||
- ((gccMode () || msvcMode ()) && has_flexible_array_member last)
+ ((gccMode() || msvcMode()) && has_flexible_array_member last)
| _ -> false
(* last_field is [true] if the given type is the type of the last field of
diff --git a/src/kernel_services/ast_queries/cil_const.ml b/src/kernel_services/ast_queries/cil_const.ml
index bed7d0dd72d5aa760337ed34d094d45c3a8864bd..20033aed2b0d8163ee290341ce9999f11a086dab 100644
--- a/src/kernel_services/ast_queries/cil_const.ml
+++ b/src/kernel_services/ast_queries/cil_const.ml
@@ -186,8 +186,10 @@ let make_logic_info k x =
let make_logic_info_local = make_logic_info LVLocal
let make_logic_info = make_logic_info LVGlobal
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
+let make_logic_type name = {
+ lt_name = name ;
+ lt_params = [] ;
+ lt_def = None ;
+ lt_attr = [] ;
+}
+
diff --git a/src/kernel_services/ast_queries/cil_const.mli b/src/kernel_services/ast_queries/cil_const.mli
index b43e9f2456f8cb68c489b83d27c9e2bc96d0c962..1c3c1cf27bacc1952bc76db8f87a4b71cdede787 100644
--- a/src/kernel_services/ast_queries/cil_const.mli
+++ b/src/kernel_services/ast_queries/cil_const.mli
@@ -211,15 +211,14 @@ val make_logic_var_quant: string -> logic_type -> logic_var
val make_logic_var_local: string -> logic_type -> logic_var
(** Create a fresh logical (global) variable giving its name and type. *)
-val make_logic_info : string -> (* logic_type -> *) logic_info
+val make_logic_info : string -> logic_info
(** Create a new local logic variable given its name.
@since Fluorine-20130401
*)
-val make_logic_info_local : string -> (* logic_type -> *) logic_info
+val make_logic_info_local : string -> logic_info
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
+(** Create a logic type info given its name.
+ @since Frama-C+dev
*)
+val make_logic_type : string -> logic_type_info
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index f11de6f809ec1404417c390aa3bfab294568466b..7f6d2ff8823eafa1fab66456909f79944fb9b887 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -2219,6 +2219,18 @@ module Global_annotation = struct
if res = 0 then Attributes.compare attr1 attr2 else res
| Daxiomatic _, _ -> -1
| _, Daxiomatic _ -> 1
+ | Dmodule (m1,g1,attr1,drv1,_), Dmodule (m2,g2,attr2,drv2,_) ->
+ let res = String.compare m1 m2 in
+ if res = 0 then
+ let res = compare_list compare g1 g2 in
+ if res = 0 then
+ let res = Stdlib.compare drv1 drv2 in
+ if res = 0 then Attributes.compare attr1 attr2
+ else res
+ else res
+ else res
+ | Dmodule _, _ -> -1
+ | _, Dmodule _ -> 1
| Dtype(t1,_), Dtype(t2,_) -> Logic_type_info.compare t1 t2
| Dtype _, _ -> -1
| _, Dtype _ -> 1
@@ -2250,6 +2262,7 @@ module Global_annotation = struct
| Daxiomatic (_,[],_,_) -> 5
(* Empty axiomatic is weird but authorized. *)
| Daxiomatic (_,g::_,_,_) -> 5 * hash g
+ | Dmodule (m,_,_,_,_) -> 5 * Datatype.String.hash m
| Dtype (t,_) -> 7 * Logic_type_info.hash t
| Dlemma(n,_,_,_,_,_) -> 11 * Datatype.String.hash n
| Dinvariant(l,_) -> 13 * Logic_info.hash l
@@ -2263,6 +2276,7 @@ module Global_annotation = struct
let loc = function
| Dfun_or_pred(_, loc)
| Daxiomatic(_, _, _, loc)
+ | Dmodule(_, _, _, _, loc)
| Dtype (_, loc)
| Dlemma(_, _, _, _, _, loc)
| Dinvariant(_, loc)
@@ -2273,7 +2287,7 @@ module Global_annotation = struct
let attr = function
| Dfun_or_pred({ l_var_info = { lv_attr }}, _) -> lv_attr
- | Daxiomatic(_, _, attr, _) -> attr
+ | Daxiomatic(_, _, attr, _) | Dmodule(_, _, attr, _, _) -> attr
| Dtype ({lt_attr}, _) -> lt_attr
| Dlemma(_, _, _, _, attr, _) -> attr
| Dinvariant({ l_var_info = { lv_attr }}, _) -> lv_attr
@@ -2682,9 +2696,3 @@ module Syntactic_scope =
(* -------------------------------------------------------------------------- *)
let clear_caches () = List.iter (fun f -> f ()) !clear_caches
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 489e20d633eeeebe1fd46468d8cfc982bcad6fd5..6ca05d52d01f0f2c06f51347850d52601ad55b19 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -699,6 +699,7 @@ let files_to_cabs_cil files cpp_commands =
if Kernel.UnspecifiedAccess.get () then
Undefined_sequence.check_sequences merged_file;
merged_file, cabs_files
+
(* "Implicit" annotations are those added by the kernel with ACSL name
'Frama_C_implicit_init'. Currently, this concerns statements that are
generated to initialize local variables. *)
@@ -1255,7 +1256,7 @@ let extract_logic_infos g =
| Dfun_or_pred (li,_) | Dinvariant (li,_) | Dtype_annot (li,_) -> li :: acc
| Dvolatile _ | Dtype _ | Dlemma _
| Dmodel_annot _ | Dextended _ -> acc
- | Daxiomatic(_,l,_,_) -> List.fold_left aux acc l
+ | Daxiomatic(_,l,_,_) | Dmodule(_,l,_,_,_) -> List.fold_left aux acc l
in aux [] g
let find_logic_info_decl li =
diff --git a/src/kernel_services/ast_queries/logic_env.ml b/src/kernel_services/ast_queries/logic_env.ml
index f6c3d366337b3ba83800c1a1787078d12a32b107..04d065b5b91cdf923b9b8e6eb1e3de8ea2ae65b9 100644
--- a/src/kernel_services/ast_queries/logic_env.ml
+++ b/src/kernel_services/ast_queries/logic_env.ml
@@ -156,6 +156,19 @@ module Axiomatics =
let size = 17
end)
+module ModuleOccurence =
+ Datatype.Pair
+ (Datatype.Option(Datatype.String)) (* external driver *)
+ (Cil_datatype.Location)
+
+module Modules =
+ State_builder.Hashtbl(Datatype.String.Hashtbl)(ModuleOccurence)
+ (struct
+ let name = "Logic_env.Modules"
+ let dependencies = []
+ let size = 17
+ end)
+
module Model_info =
State_builder.Hashtbl
(Datatype.String.Hashtbl)
@@ -175,6 +188,7 @@ let init_dependencies from =
Logic_ctor_info.self;
Lemmas.self;
Axiomatics.self;
+ Modules.self;
Model_info.self;
]
@@ -342,6 +356,7 @@ let prepare_tables () =
Logic_info.clear ();
Lemmas.clear ();
Axiomatics.clear();
+ Modules.clear();
Model_info.clear ();
Logic_type_builtin.iter Logic_type_info.add;
Logic_ctor_builtin.iter Logic_ctor_info.add;
diff --git a/src/kernel_services/ast_queries/logic_env.mli b/src/kernel_services/ast_queries/logic_env.mli
index c84b4872d93b34ff1ef2c1799651149cc00cd391..7bdbb547c3398e525012900b65b184b33375869d 100644
--- a/src/kernel_services/ast_queries/logic_env.mli
+++ b/src/kernel_services/ast_queries/logic_env.mli
@@ -64,6 +64,11 @@ module Lemmas: State_builder.Hashtbl
module Axiomatics: State_builder.Hashtbl
with type key = string and type data = Cil_types.location
+(** @since Frama-C+dev *)
+module Modules: State_builder.Hashtbl
+ with type key = string
+ and type data = string option * Cil_types.location (* driver, loc *)
+
val builtin_states: State.t list
(** {2 Shortcuts to the functions of the modules above} *)
diff --git a/src/kernel_services/ast_queries/logic_parse_string.ml b/src/kernel_services/ast_queries/logic_parse_string.ml
index f7ea6404e5b3a35bd09fea74c8a62d6e79b22bd8..b37125a59cc7cd035dca5f2bca17931a97d88a09 100644
--- a/src/kernel_services/ast_queries/logic_parse_string.ml
+++ b/src/kernel_services/ast_queries/logic_parse_string.ml
@@ -96,13 +96,6 @@ let default_typer kf kinstr =
let find_type = Globals.Types.find_type
let find_label s = Kernel_function.find_label kf s
- include Logic_env
-
- let add_logic_function =
- add_logic_function_gen Logic_utils.is_same_logic_profile
-
- let remove_logic_info =
- remove_logic_info_gen Logic_utils.is_same_logic_profile
let integral_cast ty t =
raise
@@ -129,7 +122,9 @@ let sync_typedefs () =
Logic_env.reset_typenames ();
Globals.Types.iter_types
(fun name _ ns ->
- if ns = Logic_typing.Typedef then Logic_env.add_typename name)
+ if ns = Logic_typing.Typedef then
+ try ignore @@ String.index name ':' with Not_found ->
+ Logic_env.add_typename name)
let wrap f parsetree loc =
match parsetree with
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 2d75c19ccdfa05074319c0587459e1b23cdb4f82..e7f3e3ff6034f52f5fdb9f572988c1adb18615b7 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -27,7 +27,6 @@ open Cil
open Logic_ptree
open Logic_const
open Logic_utils
-open Format
exception Backtrack
@@ -495,6 +494,10 @@ module Type_namespace =
let hash : t -> int = Hashtbl.hash
end)
+type logic_infos =
+ | Ctor of logic_ctor_info
+ | Lfun of logic_info list
+
type typing_context = {
is_loop: unit -> bool;
anonCompFieldName : string;
@@ -505,16 +508,6 @@ type typing_context = {
find_comp_field: compinfo -> string -> offset;
find_type : type_namespace -> string -> typ;
find_label : string -> stmt ref;
- remove_logic_function : string -> unit;
- remove_logic_info: logic_info -> unit;
- remove_logic_type: string -> unit;
- remove_logic_ctor: string -> unit;
- add_logic_function: logic_info -> unit;
- add_logic_type: string -> logic_type_info -> unit;
- add_logic_ctor: string -> logic_ctor_info -> unit;
- find_all_logic_functions: string -> logic_info list;
- find_logic_type: string -> logic_type_info;
- find_logic_ctor: string -> logic_ctor_info;
pre_state:Lenv.t;
post_state:Cil_types.termination_kind list -> Lenv.t;
assigns_env:Lenv.t;
@@ -531,35 +524,46 @@ type typing_context = {
accept_formal:bool ->
Lenv.t ->
Logic_ptree.assigns -> Cil_types.assigns;
- error: 'a 'b. location -> ('a,formatter,unit,'b) format4 -> 'a;
+ error: 'a 'b. location -> ('a,Format.formatter,unit,'b) format4 -> 'a;
on_error: 'a 'b. ('a -> 'b) -> ((location * string) -> unit) -> 'a -> 'b
}
+type module_builder = {
+ add_logic_type : location -> logic_type_info -> unit ;
+ add_logic_function : location -> logic_info -> unit ;
+}
+
module Extensions = struct
let initialized = ref false
let ref_is_extension = ref (fun _ -> assert false)
let ref_typer = ref (fun _ _ _ _ -> assert false)
let ref_typer_block = ref (fun _ _ _ _ -> assert false)
+ let ref_importer = ref (fun _ _ _ _ -> assert false)
- let set_handler ~is_extension ~typer ~typer_block =
+ let set_handler ~is_extension ~typer ~typer_block ~importer =
assert (not !initialized) ;
ref_is_extension := is_extension ;
ref_typer := typer ;
ref_typer_block := typer_block;
+ ref_importer := importer ;
initialized := true
let is_extension name = !ref_is_extension name
- let typer name ~typing_context:typing_context ~loc =
+ let typer name ~typing_context ~loc =
!ref_typer name typing_context loc
- let typer_block name ~typing_context:typing_context ~loc =
- !ref_typer_block name typing_context loc
+ let typer_block name ~typing_context ~loc mId =
+ !ref_typer_block name typing_context loc mId
+
+ let importer name ~builder ~loc (moduleId: string list) : unit =
+ !ref_importer name builder loc moduleId
end
let set_extension_handler = Extensions.set_handler
let get_typer = Extensions.typer
let get_typer_block = Extensions.typer_block
+let get_importer = Extensions.importer
let rec arithmetic_conversion ty1 ty2 =
match unroll_type ty1, unroll_type ty2 with
@@ -661,7 +665,7 @@ sig
Cil_types.logic_type -> Logic_ptree.code_annot -> code_annotation
val type_annot : location -> Logic_ptree.type_annot -> logic_info
val model_annot : location -> Logic_ptree.model_annot -> model_info
- val annot : Logic_ptree.decl -> global_annotation
+ val annot : Logic_ptree.decl -> global_annotation option
val funspec :
string list ->
varinfo -> (varinfo list) option -> typ -> Logic_ptree.spec -> funspec
@@ -679,18 +683,8 @@ module Make
val find_comp_field: compinfo -> string -> offset
val find_type : type_namespace -> string -> typ
val find_label : string -> stmt ref
- val remove_logic_function : string -> unit
- val remove_logic_info: logic_info -> unit
- val remove_logic_type: string -> unit
- val remove_logic_ctor: string -> unit
- val add_logic_function: logic_info -> unit
- val add_logic_type: string -> logic_type_info -> unit
- val add_logic_ctor: string -> logic_ctor_info -> unit
- val find_all_logic_functions: string -> logic_info list
- val find_logic_type: string -> logic_type_info
- val find_logic_ctor: string -> logic_ctor_info
val integral_cast: Cil_types.typ -> Cil_types.term -> Cil_types.term
- val error: location -> ('a,formatter,unit, 'b) format4 -> 'a
+ val error: location -> ('a,Format.formatter,unit, 'b) format4 -> 'a
val on_error: ('a -> 'b) -> ((location * string) -> unit) -> 'a -> 'b
end) =
struct
@@ -714,20 +708,103 @@ struct
find_comp_field = C.find_comp_field;
find_type = C.find_type ;
find_label = C.find_label;
- remove_logic_function = C.remove_logic_function;
- remove_logic_info = C.remove_logic_info;
- remove_logic_type = C.remove_logic_type;
- remove_logic_ctor = C.remove_logic_ctor;
- add_logic_function = C.add_logic_function;
- add_logic_type = C.add_logic_type;
- add_logic_ctor = C.add_logic_ctor;
- find_all_logic_functions = C.find_all_logic_functions;
- find_logic_type = C.find_logic_type;
- find_logic_ctor = C.find_logic_ctor;
error = C.error;
on_error = C.on_error;
}
+ (* Imported Scope *)
+
+ type scope = {
+ unqualified: bool; (* accepted for non-qualified names *)
+ long_prefix: string; (* last '::' included *)
+ short_prefix: string; (* last '::' included *)
+ }
+
+ let scopes : (scope option * scope list) Stack.t = Stack.create ()
+
+ let current_scope : scope option ref = ref None
+ let imported_scopes : scope list ref = ref []
+
+ let all_scopes () =
+ match !current_scope with
+ | None -> !imported_scopes
+ | Some s -> s :: !imported_scopes
+
+ let unqualified_scopes () =
+ List.filter (fun s -> s.unqualified) @@ all_scopes ()
+
+ let push_imports () =
+ let current = !current_scope in
+ let imported = !imported_scopes in
+ let all = all_scopes () in
+ Stack.push (current,imported) scopes ;
+ imported_scopes := all
+
+ let pop_imports () =
+ begin
+ let closed = !current_scope in
+ let c,cs = Stack.pop scopes in
+ let cs =
+ match closed with
+ | Some s when c <> None -> s :: cs
+ | _ -> cs
+ in
+ current_scope := c ;
+ imported_scopes := cs ;
+ end
+
+ let add_import ?(current=false) ?alias name =
+ begin
+ let short =
+ match alias with
+ | Some "_" -> ""
+ | Some a -> a
+ | None ->
+ List.hd @@ List.rev @@ Logic_utils.longident name
+ in
+ let s = {
+ unqualified = current || alias = None;
+ long_prefix = name ^ "::";
+ short_prefix = short ^ "::";
+ } in
+ if current then
+ current_scope := Some s
+ else
+ imported_scopes := s :: !imported_scopes ;
+ end
+
+ let find_import fn a =
+ let find_opt b = try Some (fn b) with Not_found -> None in
+ if Logic_utils.is_qualified a then
+ let resolved_name =
+ let has_short_prefix s = String.starts_with ~prefix:s.short_prefix a in
+ match List.find_opt has_short_prefix @@ all_scopes () with
+ | None -> a
+ | Some s ->
+ let p = String.length s.short_prefix in
+ let n = String.length a in
+ s.long_prefix ^ String.sub a p (n-p)
+ in find_opt resolved_name
+ else
+ let find_in_scope s = find_opt (s.long_prefix ^ a) in
+ match List.find_map find_in_scope @@ unqualified_scopes () with
+ | None -> find_opt a
+ | Some _ as result -> result
+
+ let resolve_ltype =
+ find_import Logic_env.find_logic_type
+
+ let resolve_lapp f env =
+ try Some (Lfun [Lenv.find_logic_info f env]) with Not_found ->
+ find_import
+ begin fun a ->
+ try
+ Ctor (Logic_env.find_logic_ctor a)
+ with Not_found ->
+ let ls = Logic_env.find_all_logic_functions a in
+ if ls <> [] then Lfun ls else raise Not_found
+ end f
+
let rollback = Queue.create ()
let start_transaction () = Queue.clear rollback
@@ -739,25 +816,68 @@ struct
let add_rollback_action f x = Queue.add (fun () -> f x) rollback
- let add_logic_function loc li =
- let l = Logic_env.find_all_logic_functions li.l_var_info.lv_name in
- if List.exists (Logic_utils.is_same_logic_profile li) l then begin
- C.error loc
- "%s %s is already declared with the same profile"
- (match li.l_type with None -> "predicate" | Some _ -> "logic function")
- li.l_var_info.lv_name
- end else begin
- C.add_logic_function li;
- add_rollback_action C.remove_logic_info li
- end
+ let add_logic_info loc lf =
+ let lv = lf.l_var_info in
+ try
+ let _ = Logic_env.find_logic_ctor lv.lv_name in
+ C.error loc "constructor %s is already defined" lv.lv_name
+ with Not_found ->
+ if Logic_utils.mem_logic_function lf then
+ begin
+ C.error loc
+ "%s %s is already declared with the same profile"
+ (match lf.l_type with None -> "predicate" | Some _ -> "logic function")
+ lv.lv_name
+ end
+ else
+ begin
+ Logic_utils.add_logic_function lf;
+ add_rollback_action Logic_utils.remove_logic_function lf
+ end
- let add_logic_type loc info =
+ let add_logic_type loc lt =
try
- ignore (C.find_logic_type info.lt_name);
- C.error loc "logic type %s is already defined" info.lt_name
+ ignore (Logic_env.find_logic_type lt.lt_name);
+ C.error loc "logic type %s is already defined" lt.lt_name
with Not_found ->
- C.add_logic_type info.lt_name info;
- add_rollback_action C.remove_logic_type info.lt_name
+ Logic_env.add_logic_type lt.lt_name lt;
+ add_rollback_action Logic_env.remove_logic_type lt.lt_name
+
+ let add_logic_ctor loc ct =
+ try
+ ignore (Logic_env.find_logic_ctor ct.ctor_name);
+ C.error loc "type constructor %s is already defined" ct.ctor_name
+ with Not_found ->
+ let lfs = Logic_env.find_all_logic_functions ct.ctor_name in
+ if lfs <> [] then
+ C.error loc "logic function %s is already defined" ct.ctor_name
+ else
+ begin
+ Logic_env.add_logic_ctor ct.ctor_name ct;
+ add_rollback_action Logic_env.remove_logic_ctor ct.ctor_name ;
+ end
+
+ let make_module_builder (decls : global_annotation list ref) moduleId =
+ let prefix = moduleId ^ "::" in
+ let wrap s =
+ if String.starts_with ~prefix s then s else prefix ^ s in
+ let add_logic_ctor loc ct =
+ ct.ctor_name <- wrap ct.ctor_name ;
+ add_logic_ctor loc ct in
+ let add_logic_type loc lt =
+ lt.lt_name <- wrap lt.lt_name ;
+ add_logic_type loc lt ;
+ begin
+ match lt.lt_def with
+ | Some (LTsum cts) -> List.iter (add_logic_ctor loc) cts
+ | Some (LTsyn _) | None -> ()
+ end ;
+ decls := (Dtype(lt,loc)) :: !decls in
+ let add_logic_function loc lf =
+ lf.l_var_info.lv_name <- wrap lf.l_var_info.lv_name ;
+ add_logic_info loc lf ;
+ decls := (Dfun_or_pred(lf,loc)) :: !decls in
+ { add_logic_type ; add_logic_function }
let check_non_void_ptr loc ty =
if Logic_utils.isLogicVoidPointerType ty then
@@ -937,6 +1057,7 @@ struct
| LTint ikind -> Ctype (TInt (ikind, []))
| LTfloat fkind -> Ctype (TFloat (fkind, []))
| LTarray (ty,length) ->
+
let size = match length with
| ASnone -> None
| ASinteger s ->
@@ -966,8 +1087,8 @@ struct
in size_exp size
with Not_found ->
ctxt.error loc "size of array must be an integral value";
- in
- Ctype (TArray (ctype ty, size,[]))
+ in Ctype (TArray (ctype ty, size,[]))
+
| LTpointer ty -> Ctype (TPtr (ctype ty, []))
| LTenum e ->
(try Ctype (ctxt.find_type Enum e)
@@ -978,35 +1099,43 @@ struct
| LTunion u ->
(try Ctype (ctxt.find_type Union u)
with Not_found -> ctxt.error loc "no such union %s" u)
+
| LTarrow (prms,rt) ->
(* For now, our only function types are C function pointers. *)
let prms = List.map (fun x -> "", ctype x, []) prms in
let rt = ctype rt in
- (match prms with
- [] -> Ctype (TFun(rt,None,false,[]))
- | [(_,arg_typ,_)] when isVoidType arg_typ ->
- (* Same invariant as in C *)
- Ctype (TFun(rt,Some [],false,[]))
- | _ -> Ctype (TFun(rt,Some prms,false,[])))
+ begin
+ match prms with
+ | [] -> Ctype (TFun(rt,None,false,[]))
+ | [(_,arg_typ,_)] when isVoidType arg_typ ->
+ (* Same invariant as in C *)
+ Ctype (TFun(rt,Some [],false,[]))
+ | _ -> Ctype (TFun(rt,Some prms,false,[]))
+ end
+
| LTnamed (id,[]) ->
- (try Lenv.find_type_var id env
- with Not_found ->
- try Ctype (ctxt.find_type Typedef id) with Not_found ->
- try
- let info = ctxt.find_logic_type id in
- if info.lt_params <> [] then
- ctxt.error loc "wrong number of parameter for type %s" id
- else Ltype (info,[])
- with Not_found ->
- ctxt.error loc "no such type %s" id)
+ begin
+ try Lenv.find_type_var id env
+ with Not_found ->
+ try Ctype (ctxt.find_type Typedef id) with Not_found ->
+ match resolve_ltype id with
+ | Some info ->
+ if info.lt_params <> [] then
+ ctxt.error loc "wrong number of parameter for type %s" id
+ else Ltype (info,[])
+ | None -> ctxt.error loc "no such type %s" id
+ end
+
| LTnamed(id,l) ->
- (try
- let info = ctxt.find_logic_type id in
- if List.length info.lt_params <> List.length l then
- ctxt.error loc "wrong number of parameter for type %s" id
- else Ltype (info,List.map ltype l)
- with Not_found ->
- ctxt.error loc "no such type %s" id)
+ begin
+ match resolve_ltype id with
+ | Some info ->
+ if List.length info.lt_params <> List.length l then
+ ctxt.error loc "wrong number of parameter for type %s" id
+ else Ltype (info,List.map ltype l)
+ | None -> ctxt.error loc "no such type %s" id
+ end
+
| LTinteger -> Linteger
| LTreal -> Lreal
| LTattribute (ty,attr) ->
@@ -1286,7 +1415,7 @@ struct
c_mk_cast ~force e oldt newt
| t1, Ltype ({lt_name = name},[])
when name = Utf8_logic.boolean && is_integral_type t1 ->
- let t2 = Ltype (C.find_logic_type Utf8_logic.boolean,[]) in
+ let t2 = Ltype (Logic_env.find_logic_type Utf8_logic.boolean,[]) in
let e = mk_cast e Linteger in
Logic_const.term ~loc (TBinOp(Ne,e,lzero ~loc())) t2
| t1, Linteger when Logic_const.is_boolean_type t1 && explicit ->
@@ -1841,10 +1970,10 @@ struct
prefer boolean as common type when doing comparison. *)
| Ltype({lt_name = name},[]), t
when is_integral_type t && name = Utf8_logic.boolean ->
- Ltype(C.find_logic_type Utf8_logic.boolean,[])
+ Ltype(Logic_env.find_logic_type Utf8_logic.boolean,[])
| t, Ltype({lt_name = name},[])
when is_integral_type t && name = Utf8_logic.boolean ->
- Ltype(C.find_logic_type Utf8_logic.boolean,[])
+ Ltype(Logic_env.find_logic_type Utf8_logic.boolean,[])
| Lreal, Ctype ty | Ctype ty, Lreal when isArithmeticType ty -> Lreal
| Ltype (s1,l1), Ltype (s2,l2)
when s1.lt_name = s2.lt_name && List.for_all2 is_same_type l1 l2 ->
@@ -1992,10 +2121,10 @@ struct
let rename_variable t v1 v2 =
visitCilTerm (new rename_variable v1 v2) t
- let find_logic_info v env =
+ let find_lv_logic_info v env =
try Lenv.find_logic_info v.lv_name env
with Not_found ->
- let l = C.find_all_logic_functions v.lv_name in
+ let l = Logic_env.find_all_logic_functions v.lv_name in
(* Data constructors can not be in eta-reduced form. v must be
a logic function, so that List.find can not fail here.
*)
@@ -2030,7 +2159,7 @@ struct
to suppose that v has no label (this is checked
when type-checking v as a variable)
*)
- Tapp(find_logic_info v env,[],args);
+ Tapp(find_lv_logic_info v env,[],args);
term_type = rt});
term_type = v.lv_type}
| _ -> { term_loc = loc; term_name = names;
@@ -2494,8 +2623,9 @@ struct
let locs = List.rev_map (make_set_conversion convert_ptr) locs in
locs,typ
and lfun_app ctxt env loc f labels ttl =
- try
- let info = ctxt.find_logic_ctor f in
+ match resolve_lapp f env with
+ | None -> C.error loc "unbound logic function %s" f
+ | Some (Ctor info) ->
if labels <> [] then begin
if ctxt.silent then raise Backtrack;
ctxt.error loc
@@ -2503,18 +2633,13 @@ struct
It cannot have logic labels" f;
end;
let params = List.map fresh info.ctor_params in
- let env, tl =
- type_arguments ~overloaded:false env loc params ttl
- in
- let t = Ltype(info.ctor_type,
- List.map fresh_type_var
- info.ctor_type.lt_params)
- in
- let t = instantiate env t in
+ let env, tl = type_arguments ~overloaded:false env loc params ttl in
+ let alphas = List.map fresh_type_var info.ctor_type.lt_params in
+ let t = instantiate env @@ Ltype(info.ctor_type,alphas) in
TDataCons(info,tl), t
- with Not_found ->
+ | Some (Lfun infos) ->
let info, label_assoc, tl, t =
- type_logic_app env loc f labels ttl
+ type_logic_app_infos env loc f infos labels ttl
in
match t with
| None ->
@@ -2641,63 +2766,63 @@ struct
| _ -> assert false
end
with Not_found ->
- try
fresh_type#reset ();
- let info = ctxt.find_logic_ctor x in
- match info.ctor_params with
- [] ->
- TDataCons(info,[]),
- Ltype(info.ctor_type,
- List.map fresh_type_var
- info.ctor_type.lt_params)
- | _ ->
- ctxt.error loc "Data constructor %s needs arguments"
- info.ctor_name
- with Not_found ->
- (* We have a global logic variable. It may depend on
- a single state (multiple labels need to be explicitly
- instantiated and are treated as PLapp below).
- NB: for now, if we have a real function (with parameters
- other than labels) and a label,
- we end up with a Tapp with no argument, which is not
- exactly good. Either TVar should take an optional label
- for this particular case, or we should definitely move
- to partial app everywhere (since we have support for
- \lambda, this is not a very big step anyway)
- *)
- let make_expr f =
- let typ =
- match f.l_type, f.l_profile with
- | Some t, [] -> t
- | Some t, l -> Larrow (List.map (fun x -> x.lv_type) l, t)
- | None, _ ->
- if ctxt.silent then raise Backtrack;
- ctxt.error loc "%s is not a logic variable" x
+ match resolve_lapp x env with
+ | None -> ctxt.error loc "unbound logic variable %s" x
+ | Some (Ctor info) ->
+ begin
+ match info.ctor_params with
+ [] ->
+ TDataCons(info,[]),
+ Ltype(info.ctor_type,
+ List.map fresh_type_var
+ info.ctor_type.lt_params)
+ | _ ->
+ ctxt.error loc "Data constructor %s needs arguments"
+ info.ctor_name
+ end
+ | Some (Lfun ls) ->
+ (* We have a global logic variable. It may depend on
+ a single state (multiple labels need to be explicitly
+ instantiated and are treated as PLapp below).
+ NB: for now, if we have a real function (with parameters
+ other than labels) and a label,
+ we end up with a Tapp with no argument, which is not
+ exactly good. Either TVar should take an optional label
+ for this particular case, or we should definitely move
+ to partial app everywhere (since we have support for
+ \lambda, this is not a very big step anyway)
+ *)
+ let make_expr f =
+ let typ =
+ match f.l_type, f.l_profile with
+ | Some t, [] -> t
+ | Some t, l -> Larrow (List.map (fun x -> x.lv_type) l, t)
+ | None, _ ->
+ if ctxt.silent then raise Backtrack;
+ ctxt.error loc "%s is not a logic variable" x
+ in
+ let typ = fresh typ in
+ match f.l_labels with
+ [] ->
+ TLval (TVar(f.l_var_info),TNoOffset), typ
+ | [_] ->
+ let curr = find_current_label loc env in
+ Tapp(f,[curr],[]), typ
+ | _ ->
+ ctxt.error loc
+ "%s labels must be explicitly instantiated" x
in
- let typ = fresh typ in
- match f.l_labels with
- [] ->
- TLval (TVar(f.l_var_info),TNoOffset), typ
- | [_] ->
- let curr = find_current_label loc env in
- Tapp(f,[curr],[]), typ
- | _ ->
- ctxt.error loc
- "%s labels must be explicitly instantiated" x
- in
- match ctxt.find_all_logic_functions x with
-
- [] -> ctxt.error loc "unbound logic variable %s" x
- | [f] -> make_expr f
- | l ->
- (try
- let f =
- List.find (fun info -> info.l_profile = []) l
- in make_expr f
- with Not_found ->
- ctxt.error loc
- "invalid use of overloaded function \
- %s as constant" x)
+ match ls with
+ | [f] -> make_expr f
+ | l ->
+ try
+ let f =
+ List.find (fun info -> info.l_profile = []) l
+ in make_expr f
+ with Not_found ->
+ ctxt.error loc
+ "invalid use of overloaded function %s as constant" x
end
| PLapp (f, labels, tl) ->
let env = drop_qualifiers env in
@@ -2959,14 +3084,14 @@ struct
let env = drop_qualifiers env in
let f _ op t1 t2 =
(TBinOp(binop_of_rel op, t1, t2),
- Ltype(ctxt.find_logic_type Utf8_logic.boolean,[]))
+ Ltype(Logic_env.find_logic_type Utf8_logic.boolean,[]))
in
type_relation ctxt env f t1 op t2
| PLtrue ->
- let ctrue = ctxt.find_logic_ctor "\\true" in
+ let ctrue = Logic_env.find_logic_ctor "\\true" in
TDataCons(ctrue,[]), Ltype(ctrue.ctor_type,[])
| PLfalse ->
- let cfalse = ctxt.find_logic_ctor "\\false" in
+ let cfalse = Logic_env.find_logic_ctor "\\false" in
TDataCons(cfalse,[]), Ltype(cfalse.ctor_type,[])
| PLlambda(prms,e) ->
let env = drop_qualifiers env in
@@ -2976,24 +3101,24 @@ struct
| PLnot t ->
let env = drop_qualifiers env in
let t = type_bool_term ctxt env t in
- TUnOp(LNot,t), Ltype (ctxt.find_logic_type Utf8_logic.boolean,[])
+ TUnOp(LNot,t), Ltype (Logic_env.find_logic_type Utf8_logic.boolean,[])
| PLand (t1,t2) ->
let env = drop_qualifiers env in
let t1 = type_bool_term ctxt env t1 in
let t2 = type_bool_term ctxt env t2 in
- TBinOp(LAnd,t1,t2), Ltype (ctxt.find_logic_type Utf8_logic.boolean,[])
+ TBinOp(LAnd,t1,t2), Ltype (Logic_env.find_logic_type Utf8_logic.boolean,[])
| PLor (t1,t2) ->
let env = drop_qualifiers env in
let t1 = type_bool_term ctxt env t1 in
let t2 = type_bool_term ctxt env t2 in
- TBinOp(LOr,t1,t2), Ltype (ctxt.find_logic_type Utf8_logic.boolean,[])
+ TBinOp(LOr,t1,t2), Ltype (Logic_env.find_logic_type Utf8_logic.boolean,[])
| PLtypeof t1 ->
let env = drop_qualifiers env in
let t1 = term env t1 in
- Ttypeof t1, Ltype (ctxt.find_logic_type "typetag",[])
+ Ttypeof t1, Ltype (Logic_env.find_logic_type "typetag",[])
| PLtype ty ->
- begin match logic_type ctxt loc env ty with
- | Ctype ty -> Ttype ty, Ltype (ctxt.find_logic_type "typetag",[])
+ begin match logic_type ctxt loc env ty with
+ | Ctype ty -> Ttype ty, Ltype (Logic_env.find_logic_type "typetag",[])
| Linteger | Lreal | Ltype _ | Lvar _ | Larrow _ ->
ctxt.error loc "cannot take type tag of logic type"
end
@@ -3086,7 +3211,7 @@ struct
let t1,ty1 = type_num_term_option ctxt env t1 in
let t2,ty2 = type_num_term_option ctxt env t2 in
(Trange(t1,t2),
- Ltype(ctxt.find_logic_type "set", [arithmetic_conversion ty1 ty2]))
+ Ltype(Logic_env.find_logic_type "set", [arithmetic_conversion ty1 ty2]))
| PLvalid _ | PLvalid_read _ | PLobject_pointer _ | PLvalid_function _
| PLfresh _ | PLallocable _ | PLfreeable _
| PLinitialized _ | PLdangling _ | PLexists _ | PLforall _
@@ -3199,26 +3324,26 @@ struct
| TAddrOf lv
| Tat ({term_node = TAddrOf lv}, _) ->
f lv t
- | _ -> C.error t.term_loc "not a dependency value: %a"
- Cil_printer.pp_term t
+ | _ ->
+ C.error t.term_loc "not a dependency value: %a" Cil_printer.pp_term t
in
lift_set check_from t
and type_logic_app env loc f labels ttl =
- (* support for overloading *)
- let infos =
- try [Lenv.find_logic_info f env]
- with Not_found ->
- C.find_all_logic_functions f in
+ match resolve_lapp f env with
+ | Some (Lfun infos) -> type_logic_app_infos env loc f infos labels ttl
+ | Some (Ctor info) ->
+ C.error loc "not a predicate: constructor %s" info.ctor_name
+ | None ->
+ C.error loc "unbound logic predicate %s" f
+
+ and type_logic_app_infos env loc f (infos : logic_info list) labels ttl =
match infos with
- | [] -> C.error loc "unbound logic function %s" f
| [info] ->
begin
let labels = List.map (find_logic_label loc env) labels in
let params = List.map (fun x -> fresh x.lv_type) info.l_profile in
- let env, tl =
- type_arguments ~overloaded:false env loc params ttl
- in
+ let env, tl = type_arguments ~overloaded:false env loc params ttl in
let label_assoc = labels_assoc loc f env info.l_labels labels in
match info.l_type with
| Some t ->
@@ -3236,26 +3361,19 @@ struct
try
let labels = List.map (find_logic_label loc env) labels in
let params =
- List.map (fun x -> fresh x.lv_type) info.l_profile
- in
+ List.map (fun x -> fresh x.lv_type) info.l_profile in
let env, tl =
- type_arguments ~overloaded:true env loc params ttl
- in
- let tl =
- List.combine (List.map (instantiate env) params) tl
- in
- let label_assoc = labels_assoc loc f env info.l_labels labels
- in
+ type_arguments ~overloaded:true env loc params ttl in
+ let tl = List.combine (List.map (instantiate env) params) tl in
+ let label_assoc = labels_assoc loc f env info.l_labels labels in
match info.l_type with
| Some t ->
let t = fresh t in
let t =
try instantiate env t
with _ -> raise Not_applicable
- in
- (info, label_assoc, tl, Some t)::acc
- | None ->
- (info, label_assoc, tl, None)::acc
+ in (info, label_assoc, tl, Some t)::acc
+ | None -> (info, label_assoc, tl, None)::acc
with Not_applicable -> acc)
[] infos
in
@@ -3281,15 +3399,13 @@ struct
tt
and type_bool_term ctxt env t =
- let module [@warning "-60"] C = struct end in
let tt = ctxt.type_term ctxt env t in
if not (plain_boolean_type tt.term_type) then
ctxt.error t.lexpr_loc "boolean expected but %a found"
Cil_printer.pp_logic_type tt.term_type;
- mk_cast tt (Ltype (ctxt.find_logic_type Utf8_logic.boolean,[]))
+ mk_cast tt (Ltype (Logic_env.find_logic_type Utf8_logic.boolean,[]))
and type_num_term_option ctxt env t =
- let module [@warning "-60"] C = struct end in
match t with
None -> None, Linteger (* Warning: should be an hybrid of integer
and float. *)
@@ -3345,7 +3461,6 @@ struct
| _ -> [], ctxt.type_predicate ctxt env p0
let term_lval_assignable ctxt ~accept_formal ~accept_const env t =
- let module [@warning "-60"] C = struct end in
let t = ctxt.type_term ctxt env t in
let mode = { lval_assignable_mode with accept_formal ; accept_const } in
if not (check_lval_kind mode t) then
@@ -3354,7 +3469,6 @@ struct
lift_set (term_lval (fun _ t -> t)) t
let term ctxt env t =
- let module [@warning "-60"] C = struct end in
match t.lexpr_node with
| PLnamed(name,t) ->
let t = ctxt.type_term ctxt env t in
@@ -3364,7 +3478,6 @@ struct
{ term_node = t'; term_loc=t.lexpr_loc; term_type=ty; term_name = [] }
let predicate ctxt env p0 =
- let module [@warning "-60"] C = struct end in
let loc = p0.lexpr_loc in
let predicate = ctxt.type_predicate ctxt in
let term = ctxt.type_term ctxt in
@@ -3401,7 +3514,7 @@ struct
prel ~loc (Cil_types.Req, t, Cil.lzero ~loc ())
| p -> pnot ~loc p)
| PLapp (p, labels, tl) ->
- let ttl= List.map (term env) tl in
+ let ttl = List.map (term env) tl in
let info, label_assoc, tl, t = type_logic_app env loc p labels ttl in
begin
match t with
@@ -3502,7 +3615,7 @@ struct
let info =
List.find
(fun x -> x.l_profile = [])
- (ctxt.find_all_logic_functions x)
+ (Logic_env.find_all_logic_functions x)
in make_app info
with Not_found -> boolean_to_predicate ctxt env p0))
| PLlet(x,def,body) ->
@@ -3747,8 +3860,7 @@ struct
~logic_type
~type_predicate
~type_term
- ~type_assigns:type_assign
- in
+ ~type_assigns:type_assign in
let b_assumes = List.map (id_predicate env) bas in
let b_requires= List.map (id_predicate_top env) br in
let b_post_cond =
@@ -4008,7 +4120,17 @@ struct
in
labels,env
- let logic_decl loc f labels poly ?return_type p =
+ type context =
+ | Toplevel
+ | InAxiomatic
+ | InModule of string
+
+ let fullname ~context name =
+ match context with
+ | Toplevel | InAxiomatic -> name
+ | InModule m -> Format.sprintf "%s::%s" m name
+
+ let logic_decl loc ~context f labels poly ?return_type p =
let labels,env = annot_env loc labels poly in
let t = match return_type with
| None -> None;
@@ -4016,7 +4138,7 @@ struct
in
let p, env = formals loc env p in
check_polymorphism loc ?return_type:t p;
- let info = Cil_const.make_logic_info f in
+ let info = Cil_const.make_logic_info (fullname ~context f) in
(* Should we add implicitly a default label for the declaration? *)
let labels = match !Lenv.default_label with
None -> labels
@@ -4033,24 +4155,29 @@ struct
info.l_profile <- p;
info.l_type <- t;
info.l_labels <- labels;
- add_logic_function loc info;
+ add_logic_info loc info;
env,info
let type_annot loc ti =
let p = ti.this_type, ti.this_name in
(* Note: Logic_decl registers the logic function *)
- let env, info = logic_decl loc ti.inv_name [] [] [p] in
+ let env, info = logic_decl loc ~context:Toplevel ti.inv_name [] [] [p] in
let body = predicate env ti.inv in
info.l_body <- LBpred body;
update_info_wrt_default_label info;
info
- let type_datacons loc env type_info (name,params) =
+ let type_datacons loc env type_info ~context (name,params) =
+ let name = fullname ~context name in
(try
- let info = C.find_logic_ctor name in
+ let info = Logic_env.find_logic_ctor name in
C.error loc "type constructor %s is already used by type %s"
name info.ctor_type.lt_name
- with Not_found -> ());
+ with Not_found ->
+ let infos = Logic_env.find_all_logic_functions name in
+ if infos <> [] then
+ C.error loc "logic function %s is already defined" name
+ );
let tparams = List.map (plain_logic_type loc env) params in
let my_info =
{ ctor_name = name;
@@ -4058,21 +4185,22 @@ struct
ctor_params = tparams
}
in
- C.add_logic_ctor name my_info;
+ Logic_env.add_logic_ctor name my_info;
my_info
- let typedef loc env my_info def =
+ let typedef loc ~context env my_info def =
match def with
- | TDsum cons -> LTsum (List.map (type_datacons loc env my_info) cons)
+ | TDsum cons -> LTsum (List.map (type_datacons loc env my_info ~context) cons)
| TDsyn typ -> LTsyn (plain_logic_type loc env typ)
- let rec annot in_axiomatic a =
+ let rec decl ~context a =
let open Current_loc.Operators in
let loc = a.decl_loc in
let<> UpdatedCurrentLoc = loc in
match a.decl_node with
+
| LDlogic_reads (f, labels, poly, t, p, l) ->
- let env,info = logic_decl loc f labels poly ~return_type:t p in
+ let env,info = logic_decl loc ~context f labels poly ~return_type:t p in
info.l_body <-
(match l with
| Some l ->
@@ -4085,9 +4213,10 @@ struct
| None -> LBnone);
(* potential creation of label w.r.t. reads clause *)
update_info_wrt_default_label info;
- Dfun_or_pred (info,loc)
+ Some (Dfun_or_pred (info,loc))
+
| LDpredicate_reads (f, labels, poly, p, l) ->
- let env,info = logic_decl loc f labels poly p in
+ let env,info = logic_decl loc ~context f labels poly p in
info.l_body <-
(match l with
| Some l ->
@@ -4100,9 +4229,10 @@ struct
| None -> LBnone);
(* potential creation of label w.r.t. reads clause *)
update_info_wrt_default_label info;
- Dfun_or_pred (info,loc)
+ Some (Dfun_or_pred (info,loc))
+
| LDlogic_def(f, labels, poly,t,p,e) ->
- let env,info = logic_decl loc f labels poly ~return_type:t p in
+ let env,info = logic_decl loc ~context f labels poly ~return_type:t p in
let rt = match info.l_type with
| None -> assert false
| Some t -> t
@@ -4114,22 +4244,23 @@ struct
info.l_body <- LBterm (update_term_wrt_default_label new_term);
(* potential creation of label w.r.t. def *)
update_info_wrt_default_label info;
- Dfun_or_pred (info,loc)
+ Some (Dfun_or_pred (info,loc))
end else
C.error loc
- "return type of logic function %s is %a but %a was expected"
- f
+ "return type of logic function %s is %a but %a was expected" f
Cil_printer.pp_logic_type new_typ
Cil_printer.pp_logic_type rt
+
| LDpredicate_def (f, labels, poly, p, e) ->
- let env,info = logic_decl loc f labels poly p in
+ let env,info = logic_decl loc ~context f labels poly p in
let e = update_predicate_wrt_default_label (predicate env e) in
info.l_body <- LBpred e;
(* potential creation of label w.r.t. def *)
update_info_wrt_default_label info;
- Dfun_or_pred (info,loc)
+ Some (Dfun_or_pred (info,loc))
+
| LDinductive_def (f, input_labels, poly, p, indcases) ->
- let _env,info = logic_decl loc f input_labels poly p in
+ let _env,info = logic_decl loc ~context f input_labels poly p in
(* env is ignored: because params names are indeed useless...*)
let (global_default, l) =
List.fold_left
@@ -4154,50 +4285,99 @@ struct
Update the inductive cases that need it (i.e. do not define
their own label(s)).
*)
- let l =
- List.rev_map update_ind_case_wrt_default_label l
- in
+ let l = List.rev_map update_ind_case_wrt_default_label l in
info.l_body <- LBinductive l;
update_info_wrt_default_label info;
- Dfun_or_pred (info,loc)
+ Some (Dfun_or_pred (info,loc))
+
| LDaxiomatic(id,decls) ->
- if in_axiomatic then
- (* Not supported yet. See issue 43 on ACSL's github repository. *)
- C.error loc "Nested axiomatic. Ignoring body of %s" id
- else begin
- let change oldloc =
+ begin match context with
+ | Toplevel -> ()
+ | InAxiomatic ->
+ (* Not supported yet. See issue 43 on ACSL's github repository. *)
+ C.error loc "Nested axiomatic. Ignoring body of %s" id
+ | InModule _ ->
+ C.error loc "Nested modules and axiomatic. Ignoring body of %s" id
+ end;
+ let change oldloc =
+ C.error loc
+ "Duplicated axiomatics %s (first occurrence at %a)"
+ id Cil_printer.pp_location oldloc in
+ ignore (Logic_env.Axiomatics.memo ~change (fun _ -> loc) id);
+ let l = List.filter_map (decl ~context:InAxiomatic) decls in
+ Some (Daxiomatic(id,l,[],loc))
+
+ | LDmodule(id,decls) ->
+ begin match context with
+ | Toplevel | InModule _ -> ()
+ | InAxiomatic ->
+ (* Not supported yet. See issue 43 on ACSL's github repository. *)
+ C.error loc "Nested module and axiomatic. Ignoring body of %s" id
+ end;
+ let name = fullname ~context id in
+ let context = InModule name in
+ let change (_,oldloc) =
+ C.error loc
+ "Duplicated module %s (first occurrence at %a)"
+ id Cil_printer.pp_location oldloc in
+ ignore (Logic_env.Modules.memo ~change (fun _ -> (None,loc)) name);
+ push_imports () ;
+ add_import ~current:true name ;
+ let l = List.filter_map (decl ~context) decls in
+ pop_imports () ;
+ Some (Dmodule(name,l,[],None,loc))
+
+ | LDimport(None,name,alias) ->
+ add_import ?alias name ; None
+
+ | LDimport(Some driver as drv,name,alias) ->
+ let annot =
+ match Logic_env.Modules.find name with
+ | None, oldloc ->
C.error loc
- "Duplicated axiomatics %s (first occurrence at %a)"
- id Cil_printer.pp_location oldloc
- in
- let l = List.map (annot true) decls in
- ignore (Logic_env.Axiomatics.memo ~change (fun _ -> loc) id);
- Daxiomatic(id,l,[],loc)
- end
- | LDtype(s,l,def) ->
+ "Module %s already defined (at %a)"
+ name Cil_printer.pp_location oldloc
+ | Some odrv, oldloc ->
+ if odrv <> driver then
+ C.error loc
+ "Module %s already imported with driver %s (at %a)"
+ name odrv Cil_printer.pp_location oldloc
+ else None
+ | exception Not_found ->
+ let decls = ref [] in
+ let builder = make_module_builder decls name in
+ let path = Logic_utils.longident name in
+ Extensions.importer driver ~builder ~loc path ;
+ Logic_env.Modules.add name (drv,loc) ;
+ Some (Dmodule(name,List.rev !decls,[],drv,loc))
+ in add_import ?alias name ; annot
+
+ | LDtype(name,l,def) ->
let env = init_type_variables loc l in
+ let name = fullname ~context name in
let my_info =
- { lt_name = s;
+ { lt_name = name;
lt_params = l;
lt_def = None; (* will be updated later *)
lt_attr = [];
- }
- in
+ } in
add_logic_type loc my_info;
- let tdef = Option.map (typedef loc env my_info) def in
- if is_cyclic_typedef s tdef then
- C.error loc "Definition of %s is cyclic" s;
+ let tdef = Option.map (typedef loc ~context env my_info) def in
+ if is_cyclic_typedef name tdef then
+ C.error loc "Definition of %s is cyclic" name;
my_info.lt_def <- tdef;
- Dtype (my_info,loc)
- | LDlemma (x,labels, poly, {tp_kind = kind; tp_statement = e}) ->
- if Logic_env.Lemmas.mem x then begin
- let old_def = Logic_env.Lemmas.find x in
+ Some (Dtype (my_info,loc))
+
+ | LDlemma (name,labels, poly, {tp_kind = kind; tp_statement = e}) ->
+ let name = fullname ~context name in
+ if Logic_env.Lemmas.mem name then begin
+ let old_def = Logic_env.Lemmas.find name in
let old_kind = match old_def with
| Dlemma(_,_,_,{tp_kind },_,_) -> tp_kind
| _ -> Assert in
let old_loc = Cil_datatype.Global_annotation.loc old_def in
C.error loc "%a %s is already registered as %a (%a)"
- Cil_printer.pp_lemma_kind kind x
+ Cil_printer.pp_lemma_kind kind name
Cil_printer.pp_lemma_kind old_kind
Cil_datatype.Location.pretty old_loc
end;
@@ -4207,9 +4387,10 @@ struct
| None -> labels
| Some lab -> [lab]
in
- let def = Dlemma (x,labels, poly, p, [], loc) in
- Logic_env.Lemmas.add x def;
- def
+ let def = Dlemma (name,labels, poly, p, [], loc) in
+ Logic_env.Lemmas.add name def;
+ Some def
+
| LDinvariant (s, e) ->
let labels,env = annot_env loc [] [] in
let li = Cil_const.make_logic_info s in
@@ -4220,13 +4401,13 @@ struct
in
li.l_labels <- labels;
li.l_body <- LBpred p;
- add_logic_function loc li;
+ add_logic_info loc li;
update_info_wrt_default_label li;
- Dinvariant (li,loc)
- | LDtype_annot l ->
- Dtype_annot (type_annot loc l,loc)
- | LDmodel_annot l ->
- Dmodel_annot (model_annot loc l,loc);
+ Some (Dinvariant (li,loc))
+
+ | LDtype_annot l -> Some (Dtype_annot (type_annot loc l,loc))
+ | LDmodel_annot l -> Some (Dmodel_annot (model_annot loc l,loc))
+
| LDvolatile (tsets, (rd_opt, wr_opt)) ->
let env = keep_qualifiers (Lenv.empty ()) in
let ctxt = base_ctxt env in
@@ -4304,7 +4485,7 @@ struct
let get_volatile_fct checks_type = function
| None -> None
| Some fct ->
- try (match (C.find_var fct).lv_origin
+ try (match (ctxt.find_var fct).lv_origin
with
| None -> raise Not_found
| Some vi as vi_opt-> checks_type fct vi.vtype ; vi_opt)
@@ -4314,31 +4495,27 @@ struct
let tsets = List.map (Logic_const.new_identified_term) tsets in
let rvi_opt = get_volatile_fct checks_reads_fct rd_opt in
let wvi_opt = get_volatile_fct checks_writes_fct wr_opt in
- Dvolatile (tsets, rvi_opt, wvi_opt, [], loc)
+ Some (Dvolatile (tsets, rvi_opt, wvi_opt, [], loc))
+
| LDextended (Ext_lexpr(kind, content)) ->
let typing_context = base_ctxt (Lenv.empty ()) in
let status,tcontent = Extensions.typer kind ~typing_context ~loc content in
let textended = Logic_const.new_acsl_extension kind loc status tcontent in
- Dextended (textended, [], loc)
+ Some (Dextended (textended, [], loc))
+
| LDextended (Ext_extension (kind, name, content)) ->
let typing_context = base_ctxt (Lenv.empty ()) in
let status,tcontent =
Extensions.typer_block kind ~typing_context ~loc (name,content)
in
let textended = Logic_const.new_acsl_extension kind loc status tcontent in
- Dextended (textended, [], loc)
-
- let annot a =
- start_transaction ();
- let res = annot false a in
- finish_transaction (); res
+ Some (Dextended (textended, [], loc))
- let annot = C.on_error annot (fun _ -> rollback_transaction ())
+ let annot = C.on_error
+ (fun a ->
+ start_transaction ();
+ let res = decl ~context:Toplevel a in
+ finish_transaction (); res)
+ (fun _ -> rollback_transaction ())
end
-
-(*
- 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 0b255b0fd0482ba9355d71f6d95f4edb657c8dc1..aa049e08e03be17934e1d913c82f68d4d9961a07 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -77,7 +77,6 @@ module Lenv : sig
val find_type_var: string -> t -> Cil_types.logic_type
val find_logic_info: string -> t -> Cil_types.logic_info
val find_logic_label: string -> t -> Cil_types.logic_label
-
end
type type_namespace = Typedef | Struct | Union | Enum
@@ -86,8 +85,29 @@ type type_namespace = Typedef | Struct | Union | Enum
module Type_namespace: Datatype.S with type t = type_namespace
+type logic_infos =
+ | Ctor of logic_ctor_info
+ | Lfun of logic_info list
+
(** Functions that can be called when type-checking an extension of ACSL.
+ @before Frama-C+dev The following fields were present:
+
+ {[
+ remove_logic_function : string -> unit;
+ remove_logic_info: logic_info -> unit;
+ remove_logic_type: string -> unit;
+ remove_logic_ctor: string -> unit;
+ add_logic_function: logic_info -> unit;
+ add_logic_type: string -> logic_type_info -> unit;
+ add_logic_ctor: string -> logic_ctor_info -> unit;
+ find_all_logic_functions: string -> logic_info list;
+ find_logic_type: string -> logic_type_info;
+ find_logic_ctor: string -> logic_ctor_info;
+ ]}
+
+ You shall now use directly functions from {!Logic_env} and {!Logic_utils}.
+
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf>
*)
type typing_context = {
@@ -104,16 +124,6 @@ type typing_context = {
find_comp_field: compinfo -> string -> offset;
find_type : type_namespace -> string -> typ;
find_label : string -> stmt ref;
- remove_logic_function : string -> unit;
- remove_logic_info: logic_info -> unit;
- remove_logic_type: string -> unit;
- remove_logic_ctor: string -> unit;
- add_logic_function: logic_info -> unit;
- add_logic_type: string -> logic_type_info -> unit;
- add_logic_ctor: string -> logic_ctor_info -> unit;
- find_all_logic_functions: string -> logic_info list;
- find_logic_type: string -> logic_type_info;
- find_logic_ctor: string -> logic_ctor_info;
pre_state:Lenv.t;
post_state:termination_kind list -> Lenv.t;
assigns_env: Lenv.t;
@@ -135,7 +145,6 @@ type typing_context = {
accept_formal:bool ->
Lenv.t -> Logic_ptree.assigns -> assigns;
error: 'a 'b. location -> ('a,Format.formatter,unit,'b) format4 -> 'a;
-
on_error: 'a 'b. ('a -> 'b) -> ((location * string) -> unit) -> 'a -> 'b
(** [on_error f rollback x] will attempt to evaluate [f x]. If this triggers
an error while in [-kernel-warn-key annot-error] mode, [rollback
@@ -148,6 +157,14 @@ type typing_context = {
*)
}
+(** Functions that can be called when importing external modules into ACSL.
+ See {!Acsl_extension.register_module_importer} for details.
+ @since Frama-C+dev
+*)
+type module_builder = {
+ add_logic_type : location -> logic_type_info -> unit ;
+ add_logic_function : location -> logic_info -> unit ;
+}
module type S =
sig
@@ -202,7 +219,10 @@ sig
val model_annot :
location -> Logic_ptree.model_annot -> model_info
- val annot : Logic_ptree.decl -> global_annotation
+ (** Some logic declaration might not introduce new global annotations
+ (eg. already imported external modules).
+ @before Frama-C+dev always return a global annotation *)
+ val annot : Logic_ptree.decl -> global_annotation option
(** [funspec behaviors f prms typ spec] type-checks a function contract.
@param behaviors list of existing behaviors (outside of the current
@@ -237,19 +257,6 @@ module Make
val find_comp_field: compinfo -> string -> offset
val find_label : string -> stmt ref
- val remove_logic_function : string -> unit
- val remove_logic_info: logic_info -> unit
- val remove_logic_type: string -> unit
- val remove_logic_ctor: string -> unit
-
- val add_logic_function: logic_info -> unit
- val add_logic_type: string -> logic_type_info -> unit
- val add_logic_ctor: string -> logic_ctor_info -> unit
-
- val find_all_logic_functions : string -> Cil_types.logic_info list
- val find_logic_type: string -> logic_type_info
- val find_logic_ctor: string -> logic_ctor_info
-
(** What to do when we have a term of type Integer in a context
expecting a C integral type.
@raise Failure to reject such conversion
@@ -308,10 +315,10 @@ val set_extension_handler:
is_extension:(string -> bool) ->
typer:(string -> typing_context -> location -> Logic_ptree.lexpr list ->
(bool * acsl_extension_kind)) ->
- typer_block:(string -> typing_context ->
- Filepath.position * Filepath.position ->
+ typer_block:(string -> typing_context -> location ->
string * Logic_ptree.extended_decl list ->
bool * Cil_types.acsl_extension_kind) ->
+ importer:(string -> module_builder -> location -> string list -> unit) ->
unit
(** Used to setup references related to the handling of ACSL extensions.
If your name is not [Acsl_extension], do not call this
@@ -321,7 +328,7 @@ val set_extension_handler:
val get_typer :
string ->
typing_context:typing_context ->
- loc:Filepath.position * Filepath.position ->
+ loc:location ->
Logic_ptree.lexpr list -> bool * Cil_types.acsl_extension_kind
val get_typer_block:
@@ -331,8 +338,8 @@ val get_typer_block:
string * Logic_ptree.extended_decl list ->
bool * Cil_types.acsl_extension_kind
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
+val get_importer:
+ string ->
+ builder:module_builder ->
+ loc:Logic_ptree.location ->
+ string list -> unit
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 4fbd3210b4737feca4e9ad1d7cfe8046d17a4fc4..8dc2bbe288a557b7e5139024b745974b6aa9522a 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -739,6 +739,9 @@ let rec add_attribute_glob_annot a g =
| Daxiomatic(n,l,al,loc) ->
Daxiomatic(n,List.map (add_attribute_glob_annot a) l,
Cil.addAttribute a al,loc)
+ | Dmodule(n,l,al,drv,loc) ->
+ Dmodule(n,List.map (add_attribute_glob_annot a) l,
+ Cil.addAttribute a al,drv,loc)
| Dtype(ti,_) -> ti.lt_attr <- Cil.addAttribute a ti.lt_attr; g
| Dlemma(n,labs,t,p,al,l) ->
Dlemma(n,labs,t,p,Cil.addAttribute a al,l)
@@ -867,7 +870,17 @@ let is_same_builtin_profile l1 l2 =
is_same_list (fun (_,t1) (_,t2) -> is_same_type t1 t2)
l1.bl_profile l2.bl_profile
+let is_qualified a =
+ try ignore @@ String.index a ':' ; true with Not_found -> false
+
+let longident = Str.split @@ Str.regexp_string "::"
+
+let mem_logic_function f =
+ List.exists (is_same_logic_profile f) @@
+ Logic_env.find_all_logic_functions f.l_var_info.lv_name
+
let add_logic_function = Logic_env.add_logic_function_gen is_same_logic_profile
+let remove_logic_function = Logic_env.remove_logic_info_gen is_same_logic_profile
let is_same_logic_ctor_info ci1 ci2 =
ci1.ctor_name = ci2.ctor_name &&
@@ -1217,6 +1230,9 @@ let rec is_same_global_annotation ga1 ga2 =
| Daxiomatic (id1,ga1,attr1,_), Daxiomatic (id2,ga2,attr2,_) ->
id1 = id2 && is_same_list is_same_global_annotation ga1 ga2
&& is_same_attributes attr1 attr2
+ | Dmodule (id1,ga1,attr1,drv1,_), Dmodule (id2,ga2,attr2,drv2,_) ->
+ id1 = id2 && is_same_list is_same_global_annotation ga1 ga2 && drv1 = drv2
+ && is_same_attributes attr1 attr2
| Dtype (t1,_), Dtype (t2,_) -> is_same_logic_type_info t1 t2
| Dlemma(n1,labs1,typs1,st1,attr1,_),
Dlemma(n2,labs2,typs2,st2,attr2,_) ->
@@ -1233,10 +1249,10 @@ let rec is_same_global_annotation ga1 ga2 =
is_same_opt (fun x y -> x.vname = y.vname) w1 w2 &&
is_same_attributes attr1 attr2
| Dextended(id1,_,_), Dextended(id2,_,_) -> id1 = id2
- | (Dfun_or_pred _ | Daxiomatic _ | Dtype _ | Dlemma _
+ | (Dfun_or_pred _ | Daxiomatic _ | Dmodule _ | Dtype _ | Dlemma _
| Dinvariant _ | Dtype_annot _ | Dmodel_annot _
| Dvolatile _ | Dextended _),
- (Dfun_or_pred _ | Daxiomatic _ | Dtype _ | Dlemma _
+ (Dfun_or_pred _ | Daxiomatic _ | Dmodule _ | Dtype _ | Dlemma _
| Dinvariant _ | Dtype_annot _ | Dmodel_annot _
| Dvolatile _ | Dextended _) -> false
@@ -2670,9 +2686,3 @@ class simplify_const_lval global_find_init = object (self)
end
let () = Cil_datatype.punrollLogicType := unroll_type
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index 9ef563d8833f901ce18594e055e4804f26f8a9ab..43a080b0f4c99eba312b59cffcb135f89f8dc31d 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -34,14 +34,34 @@ exception Not_well_formed of location * string
(** exception raised when an unknown extension is called. *)
exception Unknown_ext
+(** Test if the given string contains ':' (long-identifiers). *)
+val is_qualified : string -> bool
+
+(** Split a long-identifier into the list of its components.
+ eg. ["A::B::(<:)"] is split into [["A";"B";"(<:)"]].
+ Returns a singleton for regular identifiers.
+ @since Frama-C+dev *)
+val longident : string -> string list
+
(** basic utilities for logic terms and predicates. See also {! Logic_const}
to build terms and predicates.
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
-(** add a logic function in the environment.
- See {!Logic_env.add_logic_function_gen}*)
+(** Check if there is a logic function with same profile in the environment.
+ @since Frama-C+dev *)
+val mem_logic_function : logic_info -> bool
+
+(** Add a logic function in the environment.
+ Replaces any existing logic function with the same profile.
+ See {!Logic_env.add_logic_function_gen}
+ @since Frama-C+dev *)
val add_logic_function : logic_info -> unit
+(** remove any logic function with the same profile from the environment.
+ See {!Logic_env.remove_logic_function_gen}
+ @since Frama-C+dev *)
+val remove_logic_function : logic_info -> unit
+
(** {2 Types} *)
(** [is_instance_of poly t1 t2] returns [true] if [t1] can be derived from [t2]
diff --git a/src/kernel_services/parsetree/logic_ptree.ml b/src/kernel_services/parsetree/logic_ptree.ml
index 79b07e9374dd3a3be35a5aebec6f5efd0c58be1b..b079330d0ef0a6dc51ea6b1b3f75a75ac76f004e 100644
--- a/src/kernel_services/parsetree/logic_ptree.ml
+++ b/src/kernel_services/parsetree/logic_ptree.ml
@@ -244,6 +244,13 @@ and decl_node =
| LDaxiomatic of string * decl list
(** [LDaxiomatic(id,decls)]
represents a block of axiomatic definitions.*)
+ | LDmodule of string * decl list
+ (** [LDmodule(id,decls)]
+ represents a module of axiomatic definitions.*)
+ | LDimport of string option * string * string option
+ (** [LDimport(driver,module,alias)]
+ imports symbols from module using the specified driver,
+ with optional alias.*)
| LDinvariant of string * lexpr (** global invariant. *)
| LDtype_annot of type_annot (** type invariant. *)
| LDmodel_annot of model_annot (** model field. *)
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 03d0e1bec5084f4b8d47992c33939437bcb70913..57b20fe46352e2e6d87accb9ca8a9ff4177ebc06 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -104,6 +104,8 @@ let dkey_print_logic_coercions = register_category "printer:logic-coercions"
let dkey_print_logic_types = register_category "printer:logic-types"
+let dkey_print_imported_modules = register_category "printer:imported-modules"
+
let dkey_print_attrs = register_category "printer:attrs"
let dkey_print_sid = register_category "printer:sid"
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 675cfd1021d2948a4c9c9031c0cac99e57e7e03d..7bc8269c8df0146b4a11d87cd8200fda8df85963 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -102,6 +102,8 @@ val dkey_print_logic_coercions: category
val dkey_print_logic_types: category
+val dkey_print_imported_modules: category
+
val dkey_print_sid: category
val dkey_print_unspecified: category
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index 542efe1f658b28233203430cb2bc78d2fffd3556..a8984174213dff3c3ce1c0d8f4d140dc72f88de5 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -697,13 +697,6 @@ struct
let find_type _ = raise Not_found
let find_label _ = raise Not_found
- include Logic_env
- let add_logic_function =
- add_logic_function_gen Logic_utils.is_same_logic_profile
-
- let remove_logic_info =
- remove_logic_info_gen Logic_utils.is_same_logic_profile
-
let integral_cast ty t =
Aorai_option.abort
"term %a has type %a, but %a is expected."
diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml
index 1f44c023b73701dede5ade8337c197c52ded326f..fa5ff5e1979eb01c03353d4a315b3c3739856858 100644
--- a/src/plugins/eva/api/general_requests.ml
+++ b/src/plugins/eva/api/general_requests.ml
@@ -263,7 +263,8 @@ let property_evaluation_point = function
| IPAssigns {ias_kf = kf} | IPFrom {if_kf = kf} ->
Pre kf
| IPPredicate _ | IPComplete _ | IPDisjoint _ | IPDecrease _
- | IPAxiomatic _ | IPLemma _ | IPTypeInvariant _ | IPGlobalInvariant _
+ | IPAxiomatic _ | IPModule _ | IPLemma _
+ | IPTypeInvariant _ | IPGlobalInvariant _
| IPOther _ | IPAllocation _ | IPReachable _ | IPExtended _ | IPBehavior _ ->
raise Not_found
diff --git a/src/plugins/eva/gui/gui_eval.ml b/src/plugins/eva/gui/gui_eval.ml
index 05999668da4373c98805fa58fc8bc348491faee0..ad9d93edab3535f68e9873189bb0826bb10d9c91 100644
--- a/src/plugins/eva/gui/gui_eval.ml
+++ b/src/plugins/eva/gui/gui_eval.ml
@@ -38,7 +38,7 @@ let classify_pre_post kf ip =
let open Property in
match ip with
| IPPredicate {ip_kind = PKEnsures (_, Normal)} -> Some (GL_Post kf)
- | IPPredicate {ip_kind=PKEnsures _} | IPAxiomatic _ | IPLemma _
+ | IPPredicate {ip_kind=PKEnsures _} | IPAxiomatic _ | IPModule _ | IPLemma _
| IPTypeInvariant _ | IPGlobalInvariant _
| IPOther _ | IPCodeAnnot _ | IPAllocation _ | IPReachable _
| IPExtended _
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index 33403999da9d1bd033efa5709bc5b7a94386b705..e728a759797e0ebf99ec185a9e25c1a7208c6778 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -504,6 +504,9 @@ let to_do_on_select
| PIP(IPAxiomatic _ as ip) ->
main_ui#pretty_information "This is an axiomatic.@.";
main_ui#view_original (location ip)
+ | PIP(IPModule _ as ip) ->
+ main_ui#pretty_information "This is an ACSL module.@.";
+ main_ui#view_original (location ip)
| PIP(IPLemma { il_pred } as ip) ->
main_ui#pretty_information "This is a %a.@."
Cil_printer.pp_lemma_kind il_pred.tp_kind;
diff --git a/src/plugins/gui/filetree.ml b/src/plugins/gui/filetree.ml
index 4543cc17c76c8d9a35c51daadae8e100ce8c1a0e..140723ca344496c8404efbafd087d1b4919466aa 100644
--- a/src/plugins/gui/filetree.ml
+++ b/src/plugins/gui/filetree.ml
@@ -316,6 +316,7 @@ module MYTREE = struct
Some (global_name li.l_var_info.lv_name)
| Dvolatile _ -> Some "volatile clause"
| Daxiomatic (s, _, _,_) -> Some (global_name s)
+ | Dmodule (s, _, _, _, _) -> Some (global_name s)
| Dtype (lti, _) -> Some (global_name lti.lt_name)
| Dlemma (s, _, _, _, _,_) -> Some (global_name s)
| Dinvariant (li, _) -> Some (global_name li.l_var_info.lv_name)
diff --git a/src/plugins/gui/property_navigator.ml b/src/plugins/gui/property_navigator.ml
index 5592bd188cd1a9245116289196699706a367acfe..a8537e8587e9e825dec5008b995111beaf47af07 100644
--- a/src/plugins/gui/property_navigator.ml
+++ b/src/plugins/gui/property_navigator.ml
@@ -133,6 +133,7 @@ module Refreshers: sig
val instances: check
val lemmas: check
val axiomatic: check
+ val modules: check
val typeInvariants: check
val globalInvariants: check
@@ -274,6 +275,8 @@ struct
~hint:"Show lemmas" ()
let axiomatic = add ~name:"Axiomatic" ~default:false
~hint:"Show global axiomatics" ()
+ let modules = add ~name:"Module" ~default:false
+ ~hint:"Show global modules" ()
let instances = add ~name:"Instances"
~hint:"Show properties that are instances of root properties" ()
let typeInvariants = add ~name:"Type invariants"
@@ -387,6 +390,7 @@ struct
terminates.add hb;
stmtSpec.add hb;
axiomatic.add hb;
+ modules.add hb;
lemmas.add hb;
typeInvariants.add hb;
globalInvariants.add hb;
@@ -639,6 +643,7 @@ let make_panel (main_ui:main_window_extension_points) =
| IPTypeInvariant _ -> typeInvariants.get()
| IPGlobalInvariant _ -> globalInvariants.get()
| IPAxiomatic _ -> axiomatic.get () && not (onlyCurrent.get ())
+ | IPModule _ -> modules.get () && not (onlyCurrent.get ())
| IPLemma _ -> lemmas.get ()
| IPComplete _ -> complete_disjoint.get ()
| IPDisjoint _ -> complete_disjoint.get ()
@@ -842,9 +847,3 @@ let extend (main_ui:main_window_extension_points) =
main_ui#register_source_highlighter highlighter
let () = Design.register_extension extend
-
-(*
- Local Variables:
- compile-command: "make -C ../../.."
- End:
-*)
diff --git a/src/plugins/metrics/metrics_cilast.ml b/src/plugins/metrics/metrics_cilast.ml
index f2f587d755fbeb32642fe6bd8feac62a3528292f..17f41a670808f3a94fc8d2e4c6bd61767e6fa925 100644
--- a/src/plugins/metrics/metrics_cilast.ml
+++ b/src/plugins/metrics/metrics_cilast.ml
@@ -320,7 +320,7 @@ class slocVisitor ~libc : sloc_visitor = object(self)
match an with
| Dfun_or_pred (li, _) -> li.l_var_info.lv_name
| Dvolatile (_, _, _, _, _) -> " (Volatile) "
- | Daxiomatic (s, _, _, _) -> s
+ | Daxiomatic (s, _, _, _) | Dmodule (s, _, _, _, _) -> s
| Dtype (lti, _) -> lti.lt_name
| Dlemma (ln, _, _, _, _, _) -> ln
| Dinvariant (toto, _) -> toto.l_var_info.lv_name
diff --git a/src/plugins/metrics/metrics_pivot.ml b/src/plugins/metrics/metrics_pivot.ml
index 11e68d855c32d780f93e60a3b152a23569527608..0232ba1dc92dc88b1187d52872a4a56c6016bd0b 100644
--- a/src/plugins/metrics/metrics_pivot.ml
+++ b/src/plugins/metrics/metrics_pivot.ml
@@ -97,6 +97,7 @@ let node_of_global_annotation = function
| Dfun_or_pred _ -> "logic_fun_or_pred"
| Dvolatile _ -> "logic_volatile"
| Daxiomatic _ -> "axiomatic"
+ | Dmodule _ -> "module"
| Dtype _ -> "logic_type"
| Dlemma _ -> "logic_lemma"
| Dinvariant _ -> "invariant"
@@ -142,6 +143,7 @@ let name_of_global_annotation = function
| Dinvariant (li, _)
| Dtype_annot (li, _) -> Some (name_of_logic_info li)
| Daxiomatic (name, _, _, _)
+ | Dmodule (name, _, _, _, _)
| Dtype ({lt_name = name}, _)
| Dlemma (name, _, _, _, _, _)
| Dmodel_annot ({mi_name = name}, _)
@@ -157,6 +159,7 @@ let node_of_property = function
Format.asprintf "%a" Property.pretty_predicate_kind idp.ip_kind
| IPCodeAnnot ica -> node_of_code_annotation_node ica.ica_ca.annot_content
| IPAxiomatic _ -> "axiomatic"
+ | IPModule _ -> "module"
| IPLemma _ -> "lemma"
| IPBehavior _ -> "behavior"
| IPComplete _ -> "complete"
@@ -176,6 +179,7 @@ let names_of_property = function
| Property.IPPredicate idp -> idp.ip_pred.ip_content.tp_statement.pred_name
| IPCodeAnnot _ -> []
| IPAxiomatic _ -> []
+ | IPModule _ -> []
| IPLemma _ -> []
| IPBehavior _ -> []
| IPComplete _ -> []
diff --git a/src/plugins/report/classify.ml b/src/plugins/report/classify.ml
index 5ff525c353c9baabd13989e9543ddd309b50fbb1..b25a011b68370cda35fc2945c31bfc4dbd1d1714 100644
--- a/src/plugins/report/classify.ml
+++ b/src/plugins/report/classify.ml
@@ -431,7 +431,7 @@ let rec monitored_property ip =
| IPDisjoint _ -> true
| IPReachable {ir_kf=None} -> false
| IPReachable {ir_kf=Some _} -> true
- | IPAxiomatic _ -> false
+ | IPAxiomatic _ | IPModule _ -> false
| IPLemma _ -> true
| IPTypeInvariant _ | IPGlobalInvariant _ -> true
| IPOther _ -> true
diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml
index c80c97892fae77886d3fa6410c586ee651e25b4c..bba21be7666385e9fa90760540a5d5b2eccdf427 100644
--- a/src/plugins/server/kernel_properties.ml
+++ b/src/plugins/server/kernel_properties.ml
@@ -78,6 +78,7 @@ struct
let t_global_invariant = t_kind "global_invariant" "Global invariant"
let t_axiomatic = t_kind "axiomatic" "Axiomatic definitions"
+ let t_module = t_kind "module" "Logic module"
let t_axiom = t_kind "axiom" "Logical axiom"
let t_lemma = t_kind "lemma" "Logical lemma"
let t_check_lemma = t_kind "check_lemma" "Logical check lemma"
@@ -101,6 +102,7 @@ struct
end
| IPExtended { ie_ext={ ext_name=_ } } -> t_ext
| IPAxiomatic _ -> t_axiomatic
+ | IPModule _ -> t_module
| IPLemma { il_pred = { tp_kind = Admit } } -> t_axiom
| IPLemma { il_pred = { tp_kind = Assert } } -> t_lemma
| IPLemma { il_pred = { tp_kind = Check } } -> t_check_lemma
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index f8924443306b6cdcc99d6ecdf844a4a5039c8a19..a026b4ac453d1401d74e562bf73f5eda18f12fd9 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -261,16 +261,16 @@ struct
match a,b with
| Mtype a , Mtype b -> ext_compare a b
| Mtype _ , _ -> (-1)
- | _ , Mtype _ -> 1
+ | _ , Mtype _ -> (+1)
| Mrecord(a,_) , Mrecord(b,_) -> ext_compare a b
| Mrecord _ , _ -> (-1)
- | _ , Mrecord _ -> 1
+ | _ , Mrecord _ -> (+1)
| Comp (a, KValue) , Comp (b, KValue)
| Comp (a, KInit) , Comp (b, KInit) -> Compinfo.compare a b
| Comp (_, KValue) , Comp (_, KInit) -> (-1)
- | Comp (_, KInit) , Comp (_, KValue) -> 1
+ | Comp (_, KInit) , Comp (_, KValue) -> (+1)
| Comp _ , _ -> (-1)
- | _ , Comp _ -> 1
+ | _ , Comp _ -> (+1)
| Atype a , Atype b -> Logic_type_info.compare a b
let equal a b = (compare a b = 0)
@@ -379,12 +379,12 @@ struct
match f , g with
| Mfield(_,_,f,_) , Mfield(_,_,g,_) -> String.compare f g
| Mfield _ , Cfield _ -> (-1)
- | Cfield _ , Mfield _ -> 1
+ | Cfield _ , Mfield _ -> (+1)
| Cfield(f, KValue) , Cfield(g, KValue)
| Cfield(f, KInit) , Cfield(g, KInit) ->
Fieldinfo.compare f g
| Cfield(_, KInit), Cfield(_, KValue) -> (-1)
- | Cfield(_, KValue), Cfield(_, KInit) -> 1
+ | Cfield(_, KValue), Cfield(_, KInit) -> (+1)
let equal f g = (compare f g = 0)
@@ -583,7 +583,7 @@ struct
match c1 , c2 with
| None , None -> 0
| None , _ -> (-1)
- | _ , None -> 1
+ | _ , None -> (+1)
| Some c1 , Some c2 -> WpContext.S.compare c1 c2
let compare_source s1 s2 =
@@ -594,17 +594,17 @@ struct
| Extern f , Extern g ->
ext_compare f g
| Generated _ , Extern _ -> (-1)
- | Extern _ , Generated _ -> 1
+ | Extern _ , Generated _ -> (+1)
let compare f g =
if f==g then 0 else
match f , g with
| FUN {m_source=mf} , FUN {m_source=mg} -> compare_source mf mg
| FUN _ , _ -> (-1)
- | _ , FUN _ -> 1
+ | _ , FUN _ -> (+1)
| ACSL f , ACSL g -> Logic_info.compare f g
| ACSL _ , _ -> (-1)
- | _ , ACSL _ -> 1
+ | _ , ACSL _ -> (+1)
| CTOR c , CTOR d -> Logic_ctor_info.compare c d
let equal f g = (compare f g = 0)
diff --git a/src/plugins/wp/LogicUsage.ml b/src/plugins/wp/LogicUsage.ml
index 7cebbc5d2e4051eb6dc3d648356aa4a4d6502af5..fdac903ee60da0d2d499752479f92afdf5fad39a 100644
--- a/src/plugins/wp/LogicUsage.ml
+++ b/src/plugins/wp/LogicUsage.ml
@@ -223,7 +223,7 @@ let ip_of_axiomatic g =
| Some ip -> ip
let axiomatic_of_global ~context = function
- | Daxiomatic(name,globals,_,loc) as g ->
+ | (Daxiomatic(name,globals,_,loc) | Dmodule(name,globals,_,_,loc)) as g ->
let a = {
ax_name = name ;
ax_position = fst loc ;
@@ -234,8 +234,7 @@ let axiomatic_of_global ~context = function
List.iter (populate a ~context) globals ;
a.ax_types <- List.rev a.ax_types ;
a.ax_logics <- List.rev a.ax_logics ;
- a.ax_lemmas <- List.rev a.ax_lemmas ;
- a
+ a.ax_lemmas <- List.rev a.ax_lemmas ; a
| _ -> assert false
let register_logic d section l =
@@ -365,9 +364,9 @@ class visitor =
method! vannotation global =
match global with
- (* --- AXIOMATICS --- *)
+ (* --- AXIOMATICS & MODULES --- *)
- | Daxiomatic _ ->
+ | Daxiomatic _ | Dmodule _ ->
begin
let pf = database.proofcontext in
let ax = axiomatic_of_global ~context:pf global in
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index ec6b9b0cf758c9241e9564daf8d9588654bcf6e3..b296586692f2456c3d9d2120dead22a6ab087076 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -99,7 +99,7 @@ let is_active_mode ~mode ~goal (p: Property.t) =
| IPComplete _ | IPDisjoint _ -> is_default_bhv mode
| IPOther _ -> true
| IPFrom _ | IPGlobalInvariant _ | IPTypeInvariant _
- | IPAxiomatic _ | IPLemma _
+ | IPAxiomatic _ | IPModule _ | IPLemma _
| IPExtended _ | IPBehavior _
| IPReachable _ | IPPropertyInstance _
-> assert false (* n/a *)
diff --git a/src/plugins/wp/cfgGenerator.ml b/src/plugins/wp/cfgGenerator.ml
index f9c0980cbdcfa8621efb2a6a624a2d575c48d36a..de3e46df8bea47ad66ca3c0dce1a0bee6b4e226f 100644
--- a/src/plugins/wp/cfgGenerator.ml
+++ b/src/plugins/wp/cfgGenerator.ml
@@ -134,6 +134,8 @@ let rec strategy_ip model pool target =
add_lemma_task pool (LogicUsage.logic_lemma il_name)
| IPAxiomatic { iax_props } ->
List.iter (strategy_ip model pool) iax_props
+ | IPModule { im_props } ->
+ List.iter (strategy_ip model pool) im_props
| IPBehavior { ib_kf = kf ; ib_bhv = bhv } ->
add_fun_task model pool ~kf ~bhvs:[bhv] ()
| IPPredicate { ip_kf = kf ; ip_kind ; ip_kinstr = ki } ->
diff --git a/src/plugins/wp/tests/wp_plugin/module.i b/src/plugins/wp/tests/wp_plugin/module.i
new file mode 100644
index 0000000000000000000000000000000000000000..9a65901b4a0d378fdf85dff4921a6498a4072e1d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/module.i
@@ -0,0 +1,17 @@
+/*@
+ module foo::Bar {
+ type t;
+ logic t e;
+ logic t op(t x, t y);
+ logic t opN(t x, integer n) = n >= 0 ? op(x, opN(x,n-1)) : e;
+ }
+ module foo::Jazz {
+ import foo::Bar \as X;
+ logic X::t inv(X::t x);
+ logic X::t opN(X::t x, integer n) = n >= 0 ? X::opN(x,n) : X::opN(inv(x),-n);
+ }
+ import foo::Bar \as A;
+ import foo::Jazz \as B;
+ lemma AbsOp: \forall foo::Bar::t x, integer n;
+ B::opN(x,\abs(n)) == A::opN(x,\abs(n));
+ */
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/module.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/module.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..72b87f009f7db966b79acc13eddd9efc0fa2094f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/module.res.oracle
@@ -0,0 +1,11 @@
+# frama-c -wp [...]
+[kernel] Parsing module.i (no preprocessing)
+[wp] Running WP plugin...
+------------------------------------------------------------
+ Global
+------------------------------------------------------------
+
+Goal Lemma 'AbsOp':
+Let a = IAbs.abs(n). Prove: L_fooJazzopN(x, a) = L_fooBaropN(x, a).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/module.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/module.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..093854278c4d72fbd754f92d41ee362124bb680b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/module.res.oracle
@@ -0,0 +1,11 @@
+# frama-c -wp [...]
+[kernel] Parsing module.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 1 goal scheduled
+[wp] [Valid] typed_lemma_AbsOp (Alt-Ergo) (Cached)
+[wp] Proved goals: 1 / 1
+ Alt-Ergo: 1
+------------------------------------------------------------
+ Axiomatics WP Alt-Ergo Total Success
+ Lemma - 1 1 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 0d00f2dc2ef00c1d74def350ac92407f724c98a1..15abb61bcfbc36cec20ea42923485d08c7455758 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -470,6 +470,7 @@ let user_prop_names p =
| IPFrom _
| IPAllocation _
| IPAxiomatic _
+ | IPModule _
| IPBehavior _
| IPReachable _
| IPPropertyInstance _
@@ -659,9 +660,9 @@ let property_hints hs =
| IPCodeAnnot {ica_ca} -> annot_hints hs ica_ca.annot_content
| IPAssigns {ias_froms} -> assigns_hints hs ias_froms
| IPAllocation _ (* TODO *)
- | IPFrom _ | Property.IPDecrease _ | Property.IPPropertyInstance _
- | IPReachable _ | Property.IPAxiomatic _ | Property.IPOther _
- | IPTypeInvariant _ | Property.IPGlobalInvariant _ -> ()
+ | IPFrom _ | IPDecrease _ | IPPropertyInstance _
+ | IPReachable _ | IPAxiomatic _ | IPModule _ | IPOther _
+ | IPTypeInvariant _ | IPGlobalInvariant _ -> ()
let prop_id_keys p =
begin
diff --git a/tests/spec/Extend.ml b/tests/spec/Extend.ml
index 240b3da0212a6f7168cebee620e334fdcc962b2d..d3a082a65a601a626f988840f498223b090621d9 100644
--- a/tests/spec/Extend.ml
+++ b/tests/spec/Extend.ml
@@ -91,7 +91,7 @@ let type_bla typing_context _loc l =
match p.lexpr_node with
| PLapp("\\trace", [], [pred]) ->
let pred = typing_context.type_predicate typing_context env pred in
- let li = List.hd (ctxt.find_all_logic_functions "\\trace") in
+ let li = List.hd (Logic_env.find_all_logic_functions "\\trace") in
let i = Count.next () in
let ti = Logic_const.tinteger ~loc:pred.pred_loc i in
Bla_table.add i pred;
diff --git a/tests/spec/bar.i b/tests/spec/bar.i
new file mode 100644
index 0000000000000000000000000000000000000000..8ebaf7de02eccd2f6a4cebff30215e1574d8700a
--- /dev/null
+++ b/tests/spec/bar.i
@@ -0,0 +1,10 @@
+/* run.config
+ DONTRUN: Companion file of foo.i
+*/
+
+/*@
+ module A {
+ type t;
+ logic t op(t x);
+ }
+ */
diff --git a/tests/spec/foo.i b/tests/spec/foo.i
new file mode 100644
index 0000000000000000000000000000000000000000..f41b48bf59caa03ae48818bbc7b5798d5b0bcd64
--- /dev/null
+++ b/tests/spec/foo.i
@@ -0,0 +1,11 @@
+/* run.config
+ DEPS: bar.i
+ OPT: bar.i -print
+ */
+
+/*@
+ module A {
+ type t;
+ logic t op(t x);
+ }
+ */
diff --git a/tests/spec/import.i b/tests/spec/import.i
new file mode 100644
index 0000000000000000000000000000000000000000..837dffbac760fa5033558c9180fdd888069089e1
--- /dev/null
+++ b/tests/spec/import.i
@@ -0,0 +1,13 @@
+/* run.config
+MODULE: @PTEST_NAME@
+OPT: -print
+OPT: -print -kernel-msg-key printer:imported-modules
+*/
+
+/*@ import foo: A::B; */
+/*@ predicate check1(B::t x) = B::check(x,0); */
+/*@ predicate check2(A::B::t x) = A::B::check(x,0); */
+
+/*@ import foo: A::B \as C; */
+/*@ predicate check3(C::t x) = C::check(x,0); */
+/*@ predicate check4(C::t x) = A::B::check(x,0); */
diff --git a/tests/spec/import.ml b/tests/spec/import.ml
new file mode 100644
index 0000000000000000000000000000000000000000..ca99db7c9845d4dee600b58794a88ec373f6402c
--- /dev/null
+++ b/tests/spec/import.ml
@@ -0,0 +1,25 @@
+open Cil_types
+open Logic_typing
+
+let () = Format.printf "[test-import] Linking.@."
+
+let loader (ctxt: module_builder) (loc: location) (m: string list) =
+ begin
+ Format.printf "[test-import:%d] Loading %s.@."
+ (fst loc).pos_lnum (String.concat "::" m) ;
+ let t = Cil_const.make_logic_type "t" in
+ let check = Cil_const.make_logic_info "check" in
+ let x = Cil_const.make_logic_var_formal "x" (Ltype(t,[])) in
+ let k = Cil_const.make_logic_var_formal "k" Linteger in
+ check.l_profile <- [x;k] ;
+ ctxt.add_logic_type loc t ;
+ ctxt.add_logic_function loc check ;
+ end
+
+let register () =
+ begin
+ Format.printf "[test-import] Registering 'foo'.@." ;
+ Acsl_extension.register_module_importer "foo" loader ;
+ end
+
+let () = Cmdline.run_after_extended_stage register
diff --git a/tests/spec/module.c b/tests/spec/module.c
new file mode 100644
index 0000000000000000000000000000000000000000..6fa3d132da5e5acc9cf49cb54232485521ec6110
--- /dev/null
+++ b/tests/spec/module.c
@@ -0,0 +1,86 @@
+/* run.config
+ STDOPT:
+ STDOPT: +"-cpp-extra-args='-DILL_TYPED'"
+ */
+
+/*@
+ module Foo {
+ type t;
+ logic t e;
+ logic t op(t x, t y);
+ logic t opN(t x, integer n) = n >= 0 ? op(x, opN(x,n-1)) : e;
+ }
+ module foo::bar {
+ import Foo \as X;
+ type a;
+ logic a f(a x);
+ logic X::t inv(X::t x);
+ logic X::t opN(X::t x, integer n) = n >= 0 ? X::opN(x,n) : opN(inv(x),-n);
+ }
+ module foo::jazz {
+ import Foo; // both t and Foo::t can be used
+ type a;
+ logic a f(a x);
+ logic t inv(Foo::t x);
+ logic t opN(t x, integer n) = n >= 0 ? opN(x,n) : Foo::opN(inv(x),-n);
+ }
+ module priority {
+ import Foo ;
+ import foo::bar ;
+ import foo::jazz ;
+ logic t inv_jazz(t x) = inv(x); // OK, shall call foo::jazz::opN
+ logic a f_jazz(a x) = f(x); // OK, shall call foo::jazz::f
+ logic bar::a f_bar(bar::a y) = bar::f(y); // OK
+ }
+ module priority_aliased {
+ import Foo ;
+ import foo::bar \as B;
+ import foo::jazz \as J;
+ logic t inv_jazz(t x) = J::inv(x); // OK
+ logic J::a f_jazz(J::a x) = J::f(x); // OK
+ logic B::a f_bar (B::a y) = B::f(y); // OK
+ }
+ import Foo \as A;
+ import foo::bar \as B;
+ lemma AbsOp: \forall Foo::t x, integer n;
+ B::opN(x,\abs(n)) == A::opN(x,\abs(n));
+ */
+
+#ifdef ILL_TYPED
+
+/*@
+ import Foo \as F;
+ logic t x = F::e; // ill-formed: t should be F::t
+*/
+
+/*@
+ import Foo \as F;
+ import foo \as f;
+ logic F::t x = f::bar::inv(F::e); // OK
+ logic F::t y = bar::inv(F::e); // KO
+*/
+
+/*@
+ module A {
+ logic integer a = 0;
+ module B {
+ logic integer b = a + 1;
+ }
+ }
+
+import A::B \as b;
+
+logic integer z = b::a; // KO
+
+*/
+
+/*@
+ module wrong_priority {
+ import Foo ;
+ import foo::bar ;
+ import foo::jazz ;
+ logic a f_ko(a x) = bar::f(x); // KO, ill typed
+ }
+ */
+
+#endif
diff --git a/tests/spec/oracle/foo.res.oracle b/tests/spec/oracle/foo.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..50873ff7f5d0ac82c0ceba417b17ee722bb6accb
--- /dev/null
+++ b/tests/spec/oracle/foo.res.oracle
@@ -0,0 +1,11 @@
+[kernel] Parsing foo.i (no preprocessing)
+[kernel] Parsing bar.i (no preprocessing)
+/* Generated by Frama-C */
+/*@ module A {
+ type t;
+
+ logic t op(t x) ;
+
+ }
+ */
+
diff --git a/tests/spec/oracle/import.0.res.oracle b/tests/spec/oracle/import.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f0f5707e2ba6de2ef31dda0f96f9bc8b235a3fa2
--- /dev/null
+++ b/tests/spec/oracle/import.0.res.oracle
@@ -0,0 +1,16 @@
+[test-import] Linking.
+[test-import] Registering 'foo'.
+[kernel] Parsing import.i (no preprocessing)
+[test-import:7] Loading A::B.
+/* Generated by Frama-C */
+/*@ import foo: A::B \as _ ;
+ */
+/*@ predicate check1(A::B::t x) = A::B::check(x, 0);
+ */
+/*@ predicate check2(A::B::t x) = A::B::check(x, 0);
+ */
+/*@ predicate check3(A::B::t x) = A::B::check(x, 0);
+ */
+/*@ predicate check4(A::B::t x) = A::B::check(x, 0);
+ */
+
diff --git a/tests/spec/oracle/import.1.res.oracle b/tests/spec/oracle/import.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..b5236c1c99d2aa32e40c018dc31bfb639b8e0beb
--- /dev/null
+++ b/tests/spec/oracle/import.1.res.oracle
@@ -0,0 +1,22 @@
+[test-import] Linking.
+[test-import] Registering 'foo'.
+[kernel] Parsing import.i (no preprocessing)
+[test-import:7] Loading A::B.
+/* Generated by Frama-C */
+/*@ // import foo:
+ module A::B {
+ type t;
+
+ predicate check(t x, ℤ k) ;
+
+ }
+ */
+/*@ predicate check1(A::B::t x) = A::B::check(x, 0);
+ */
+/*@ predicate check2(A::B::t x) = A::B::check(x, 0);
+ */
+/*@ predicate check3(A::B::t x) = A::B::check(x, 0);
+ */
+/*@ predicate check4(A::B::t x) = A::B::check(x, 0);
+ */
+
diff --git a/tests/spec/oracle/module.0.res.oracle b/tests/spec/oracle/module.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a09b766c3acab61ad73797fb42bb17fa8f4bd5b8
--- /dev/null
+++ b/tests/spec/oracle/module.0.res.oracle
@@ -0,0 +1,65 @@
+[kernel] Parsing module.c (with preprocessing)
+/* Generated by Frama-C */
+/*@
+module Foo {
+ type t;
+
+ logic t e;
+
+ logic t op(t x, t y) ;
+
+ logic t opN(t x, ℤ n) = n ≥ 0? op(x, opN(x, n - 1)): e;
+
+ }
+ */
+/*@
+module foo::bar {
+ type a;
+
+ logic a f(a x) ;
+
+ logic Foo::t inv(Foo::t x) ;
+
+ logic Foo::t opN(Foo::t x, ℤ n) =
+ n ≥ 0? Foo::opN(x, n): opN(inv(x), -n);
+
+ }
+ */
+/*@
+module foo::jazz {
+ type a;
+
+ logic a f(a x) ;
+
+ logic Foo::t inv(Foo::t x) ;
+
+ logic Foo::t opN(Foo::t x, ℤ n) =
+ n ≥ 0? opN(x, n): Foo::opN(inv(x), -n);
+
+ }
+ */
+/*@
+module priority {
+ logic Foo::t inv_jazz(Foo::t x) = foo::jazz::inv(x);
+
+ logic foo::jazz::a f_jazz(foo::jazz::a x) = foo::jazz::f(x);
+
+ logic foo::bar::a f_bar(foo::bar::a y) = foo::bar::f(y);
+
+ }
+ */
+/*@
+module priority_aliased {
+ logic Foo::t inv_jazz(Foo::t x) = foo::jazz::inv(x);
+
+ logic foo::jazz::a f_jazz(foo::jazz::a x) = foo::jazz::f(x);
+
+ logic foo::bar::a f_bar(foo::bar::a y) = foo::bar::f(y);
+
+ }
+ */
+/*@
+lemma AbsOp:
+ ∀ Foo::t x, ℤ n; foo::bar::opN(x, \abs(n)) ≡ Foo::opN(x, \abs(n));
+ */
+
diff --git a/tests/spec/oracle/module.1.res.oracle b/tests/spec/oracle/module.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..b59f47ec8eac8cf2157e152182df5cb5a034f9e7
--- /dev/null
+++ b/tests/spec/oracle/module.1.res.oracle
@@ -0,0 +1,85 @@
+[kernel] Parsing module.c (with preprocessing)
+[kernel:annot-error] module.c:53: Warning:
+ no such type t. Ignoring global annotation
+[kernel:annot-error] module.c:60: Warning:
+ unbound logic function bar::inv. Ignoring global annotation
+[kernel:annot-error] module.c:73: Warning:
+ unbound logic variable b::a. Ignoring global annotation
+[kernel:annot-error] module.c:82: Warning:
+ incompatible types foo::jazz::a and foo::bar::a. Ignoring global annotation
+/* Generated by Frama-C */
+/*@
+module Foo {
+ type t;
+
+ logic t e;
+
+ logic t op(t x, t y) ;
+
+ logic t opN(t x, ℤ n) = n ≥ 0? op(x, opN(x, n - 1)): e;
+
+ }
+ */
+/*@
+module foo::bar {
+ type a;
+
+ logic a f(a x) ;
+
+ logic Foo::t inv(Foo::t x) ;
+
+ logic Foo::t opN(Foo::t x, ℤ n) =
+ n ≥ 0? Foo::opN(x, n): opN(inv(x), -n);
+
+ }
+ */
+/*@
+module foo::jazz {
+ type a;
+
+ logic a f(a x) ;
+
+ logic Foo::t inv(Foo::t x) ;
+
+ logic Foo::t opN(Foo::t x, ℤ n) =
+ n ≥ 0? opN(x, n): Foo::opN(inv(x), -n);
+
+ }
+ */
+/*@
+module priority {
+ logic Foo::t inv_jazz(Foo::t x) = foo::jazz::inv(x);
+
+ logic foo::jazz::a f_jazz(foo::jazz::a x) = foo::jazz::f(x);
+
+ logic foo::bar::a f_bar(foo::bar::a y) = foo::bar::f(y);
+
+ }
+ */
+/*@
+module priority_aliased {
+ logic Foo::t inv_jazz(Foo::t x) = foo::jazz::inv(x);
+
+ logic foo::jazz::a f_jazz(foo::jazz::a x) = foo::jazz::f(x);
+
+ logic foo::bar::a f_bar(foo::bar::a y) = foo::bar::f(y);
+
+ }
+ */
+/*@
+lemma AbsOp:
+ ∀ Foo::t x, ℤ n; foo::bar::opN(x, \abs(n)) ≡ Foo::opN(x, \abs(n));
+ */
+/*@ logic Foo::t x= foo::bar::inv(Foo::e);
+ */
+/*@ module A {
+ logic ℤ a= 0;
+
+ module B {
+ logic ℤ b= A::a + 1;
+
+ }
+
+ }
+ */
+
diff --git a/tests/spec/oracle/reset_env.res.oracle b/tests/spec/oracle/reset_env.res.oracle
index 3b1ae6dc368510ee07912d898dba76c225a14774..36dafa0e4307cd0da496227ebed624d675ebc4bc 100644
--- a/tests/spec/oracle/reset_env.res.oracle
+++ b/tests/spec/oracle/reset_env.res.oracle
@@ -2,6 +2,6 @@
[kernel:annot-error] reset_env.i:5: Warning:
unbound logic variable INEXISTENT_SYMBOL. Ignoring global annotation
[kernel:annot-error] reset_env.i:9: Warning:
- unbound logic function bla. Ignoring specification of function f
+ unbound logic predicate bla. Ignoring specification of function f
/* Generated by Frama-C */
diff --git a/tests/spec/oracle/submodule.res.oracle b/tests/spec/oracle/submodule.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..4ccdc877c00aeba71da94ed4c5f3869cfdc63e59
--- /dev/null
+++ b/tests/spec/oracle/submodule.res.oracle
@@ -0,0 +1,31 @@
+[kernel] Parsing submodule.i (no preprocessing)
+/* Generated by Frama-C */
+/*@
+module Foo {
+ type t;
+
+ logic t elt;
+
+ module Bar {
+ predicate test1(Foo::t x) = x ≡ Foo::elt;
+
+ predicate test2(Foo::t x, Foo::t y) = test1(x) ∧ test1(y);
+
+ module Jazz {
+ predicate test3(Foo::t x) = Foo::Bar::test2(x, x);
+
+ predicate test4(Foo::t y) = Foo::Bar::test1(y);
+
+ }
+
+ }
+
+ predicate test5(t y) = Bar::test2(y, y);
+
+ predicate test6(t y) = Bar::Jazz::test3(y);
+
+ predicate test7(t z) = Bar::test1(z);
+
+ }
+ */
+
diff --git a/tests/spec/submodule.i b/tests/spec/submodule.i
new file mode 100644
index 0000000000000000000000000000000000000000..1fc8a014113a5e11aaa45b5ab4b779d347abd82e
--- /dev/null
+++ b/tests/spec/submodule.i
@@ -0,0 +1,19 @@
+/*@
+ module Foo {
+ type t;
+ logic t elt;
+ module Bar {
+ predicate test1(t x) = x == Foo::elt;
+ predicate test2(t x, t y) = test1(x) && test1(y);
+
+ module Jazz {
+ predicate test3(t x) = test2(x,x);
+ predicate test4(t y) = Bar::test1(y);
+ }
+
+ }
+ predicate test5(t y) = Bar::test2(y,y);
+ predicate test6(t y) = Bar::Jazz::test3(y);
+ predicate test7(t z) = Foo::Bar::test1(z);
+ }
+*/