diff --git a/src/kernel_internals/parsing/clexer.mll b/src/kernel_internals/parsing/clexer.mll
index 40341eef3217c41faa876a7a04c7bc8398c8e918..2e95e6c11daa679ce1fe023f70bd838b43cd744f 100644
--- a/src/kernel_internals/parsing/clexer.mll
+++ b/src/kernel_internals/parsing/clexer.mll
@@ -53,6 +53,9 @@ module E = Errorloc
let currentLoc () = E.currentLoc ()
+let parse_error ?(loc=currentLoc()) msg =
+ E.parse_error ~loc msg
+
(* Convert char into Int64 *)
let int64_of_char c = Int64.of_int (Char.code c)
@@ -67,9 +70,15 @@ let enter_ghost_code () = ghost_code := true
let exit_ghost_code () = ghost_code := false
let ghost_annot = ref false
+let ghost_annot_start = ref Cil_datatype.Location.unknown
let is_ghost_annot () = !ghost_annot
-let enter_ghost_annot () = ghost_annot := true
-let exit_ghost_annot () = ghost_annot := false
+let get_ghost_annot_start () = !ghost_annot_start
+let enter_ghost_annot () =
+ ghost_annot := true;
+ ghost_annot_start:= currentLoc()
+let exit_ghost_annot () =
+ ghost_annot := false;
+ ghost_annot_start := Cil_datatype.Location.unknown
let add_comment c = Cabshelper.Comments.add (currentLoc()) c
@@ -290,7 +299,7 @@ let scan_escape = function
| '[' -> int64_of_char '['
| '%' -> int64_of_char '%'
| '\\' -> int64_of_char '\\'
- | other -> E.parse_error "Unrecognized escape sequence: \\%c" other
+ | other -> parse_error "Unrecognized escape sequence: \\%c" other
let scan_hex_escape str =
let radix = Int64.of_int 16 in
@@ -415,11 +424,6 @@ let make_annot ~one_line default lexbuf s =
| Logic_ptree.Aloop_annot (loc,a) -> LOOP_ANNOT (a,loc)
| Logic_ptree.Aattribute_annot (loc,a) -> ATTRIBUTE_ANNOT (a, loc)
-let parse_error lexbuf msg =
- let loc = lexbuf.Lexing.lex_curr_p in
- let source = Cil_datatype.Position.of_lexing_pos loc in
- E.parse_error ~source msg
-
(* Initialize the pointer in Errormsg *)
let () =
Lexerhack.add_type := add_type ;
@@ -528,7 +532,7 @@ rule initial = parse
{
if is_ghost_code () || is_oneline_ghost ()
then GHOST (currentLoc())
- else parse_error lexbuf "Use of \\ghost out of ghost code"
+ else parse_error "Use of \\ghost out of ghost code"
}
| blank {initial lexbuf} | '\n'
@@ -628,7 +632,7 @@ rule initial = parse
if c = !annot_char then
if is_ghost_code () || is_oneline_ghost ()
then (enter_ghost_annot () ; annot_lex initial annot_first_token lexbuf)
- else parse_error lexbuf "This kind of annotation is valid only inside ghost code"
+ else parse_error "This kind of annotation is valid only inside ghost code"
else (lexbuf.Lexing.lex_curr_pos <- lexbuf.Lexing.lex_curr_pos - 1 ; SLASH)
}
@@ -685,7 +689,7 @@ rule initial = parse
| _ as c
{
if is_ghost_code() && c = '@' then initial lexbuf
- else parse_error lexbuf "Invalid symbol"
+ else parse_error "Invalid symbol"
}
@@ -696,7 +700,7 @@ and might_end_ghost = parse
and comment buffer = parse
| "*/" { }
- | eof { parse_error lexbuf "Unterminated C comment" }
+ | eof { parse_error "Unterminated C comment" }
| _ { lex_comment comment buffer lexbuf }
@@ -793,7 +797,7 @@ and str = parse
| hex_escape { lex_hex_escape str lexbuf }
| oct_escape { lex_oct_escape str lexbuf }
| escape { lex_simple_escape str lexbuf }
- | eof { parse_error lexbuf "unterminated string" }
+ | eof { parse_error "unterminated string" }
| _ { lex_unescaped str lexbuf }
@@ -802,14 +806,14 @@ and chr = parse
| hex_escape { lex_hex_escape chr lexbuf }
| oct_escape { lex_oct_escape chr lexbuf }
| escape { lex_simple_escape chr lexbuf }
- | eof { parse_error lexbuf "unterminated char" }
+ | eof { parse_error "unterminated char" }
| _ { lex_unescaped chr lexbuf }
and annot_first_token = parse
| "ghost" ((blank| '\\'?'\n' | ghost_comments)* as comments) "else"
{
- if is_oneline_ghost () then parse_error lexbuf "nested ghost code" ;
+ if is_oneline_ghost () then parse_error "nested ghost code" ;
Buffer.clear buf ;
let loc = currentLoc () in
do_ghost_else_comments true comments ;
@@ -819,7 +823,7 @@ and annot_first_token = parse
| "ghost"
{
- if is_oneline_ghost () then parse_error lexbuf "nested ghost code" ;
+ if is_oneline_ghost () then parse_error "nested ghost code" ;
Buffer.clear buf ;
enter_ghost_code () ;
LGHOST
@@ -834,12 +838,15 @@ and annot_token = parse
| "*/"
{
if is_ghost_annot ()
- then parse_error lexbuf "Ghost multi-line annotation not terminated" ;
+ then begin
+ let loc = (fst (get_ghost_annot_start()), snd (currentLoc())) in
+ parse_error ~loc "Ghost multi-line annotation not terminated"
+ end;
let s = Buffer.contents buf in
make_annot ~one_line:false initial lexbuf s
}
- | eof { parse_error lexbuf "Unterminated annotation" }
+ | eof { parse_error "Unterminated annotation" }
| '\n' { E.newline() ; Buffer.add_char buf '\n' ; annot_token lexbuf }
| _ as c
{
@@ -860,14 +867,14 @@ and annot_one_line = parse
| "ghost" ((blank|"\\\n")+ as comments) "else"
{
do_ghost_else_comments false comments ;
- if is_oneline_ghost () then parse_error lexbuf "nested ghost code" ;
+ if is_oneline_ghost () then parse_error "nested ghost code" ;
enter_oneline_ghost () ;
LGHOST_ELSE (currentLoc ())
}
| "ghost"
{
- if is_oneline_ghost () then parse_error lexbuf "nested ghost code" ;
+ if is_oneline_ghost () then parse_error "nested ghost code" ;
enter_oneline_ghost () ;
LGHOST
}
@@ -878,7 +885,7 @@ and annot_one_line = parse
and annot_one_line_logic = parse
| '\n' { make_annot ~one_line:true initial lexbuf (Buffer.contents buf) }
- | eof { parse_error lexbuf "Invalid C file: should end with a newline" }
+ | eof { parse_error "Invalid C file: should end with a newline" }
| _ as c { Buffer.add_char buf c ; annot_one_line_logic lexbuf }
diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly
index a023f02eea1f8f38c1b441d860f4e07316d39d0e..3a7000e478ed5fd0f64cea7570b811bfef34eac6 100644
--- a/src/kernel_internals/parsing/cparser.mly
+++ b/src/kernel_internals/parsing/cparser.mly
@@ -89,14 +89,15 @@ and isJUSTBASE = function
| PARENTYPE (_, d, _) -> isJUSTBASE d
| _ -> false
-let announceFunctionName ((n, decl, _, _):name) =
+let announceFunctionName ((n, decl, _, loc):name) =
!Lexerhack.add_identifier n;
(* Start a context that includes the parameter names and the whole body.
* Will pop when we finish parsing the function body *)
!Lexerhack.push_context ();
(try findProto decl
with NoProto ->
- Errorloc.parse_error "Cannot find the prototype in a function definition");
+ Errorloc.parse_error
+ ~loc "Cannot find the prototype in a function definition");
currentFunctionName := n
let check_funspec_abrupt_clauses fname spec =
@@ -106,8 +107,8 @@ let check_funspec_abrupt_clauses fname spec =
(function
| (Cil_types.Normal | Cil_types.Exits),_ -> ()
| (Cil_types.Breaks | Cil_types.Continues | Cil_types.Returns),
- { Logic_ptree.tp_statement = { lexpr_loc = (loc,_)}} ->
- Errorloc.parse_error ~source:loc
+ { Logic_ptree.tp_statement = { lexpr_loc = loc}} ->
+ Errorloc.parse_error ~loc
"Specification of function %s can only contain ensures or \
exits post-conditions" fname)
bhv.Logic_ptree.b_post_cond)
@@ -206,18 +207,18 @@ let doOldParDecl (names: string list)
let args = List.map findOneName names in
(args, isva)
-let int64_to_char value =
+let int64_to_char ~loc value =
if (Int64.compare value (Int64.of_int 255) > 0) ||
(Int64.compare value Int64.zero < 0) then
- Errorloc.parse_error "integral literal 0x%Lx too big" value
+ Errorloc.parse_error ~loc "integral literal 0x%Lx too big" value
else
Char.chr (Int64.to_int value)
(* takes a not-nul-terminated list, and converts it to a string. *)
-let intlist_to_string str =
+let intlist_to_string ~loc str =
let buffer = Buffer.create 64 in
let add_char c =
- Buffer.add_char buffer (int64_to_char c)
+ Buffer.add_char buffer (int64_to_char ~loc c)
in
let add_char_list l = List.iter add_char l in
List.iter add_char_list str ;
@@ -276,13 +277,14 @@ let transformOffsetOf (speclist, dtype) member =
let rec replaceBase e =
let node = match e.expr_node with
| VARIABLE field ->
- MEMBEROFPTR (castExpr, field)
+ MEMBEROFPTR (castExpr, field)
| MEMBEROF (base, field) ->
- MEMBEROF (replaceBase base, field)
+ MEMBEROF (replaceBase base, field)
| INDEX (base, index) ->
- INDEX (replaceBase base, index)
+ INDEX (replaceBase base, index)
| _ ->
- Errorloc.parse_error "malformed offset expression in offsetof macro"
+ Errorloc.parse_error ~loc:e.expr_loc
+ "malformed offset expression in offsetof macro"
in { e with expr_node = node }
in
let memberExpr = replaceBase member in
@@ -479,35 +481,41 @@ global:
| EXTERN string_constant declaration
{ LINKAGE (fst $2, (*handleLoc*) (snd $2), [ $3 ]) }
| EXTERN string_constant LBRACE globals RBRACE
- { LINKAGE (fst $2, (*handleLoc*) (snd $2),
- List.map
- (fun (x,y) ->
- if x then
- Errorloc.parse_error "invalid ghost in extern linkage \
- specification"
- else y)
- $4) }
+ { LINKAGE (
+ fst $2, (*handleLoc*) (snd $2),
+ List.map
+ (fun (x,y) ->
+ if x then
+ let loc = Cabshelper.get_definitionloc y in
+ Errorloc.parse_error ~loc
+ "invalid ghost in extern linkage specification"
+ else y)
+ $4)
+ }
| ASM LPAREN string_constant RPAREN SEMICOLON
{ GLOBASM (fst $3, (*handleLoc*) $1) }
| pragma { $1 }
/* (* Old-style function prototype. This should be somewhere else, like in
* "declaration". For now we keep it at global scope only because in local
* scope it looks too much like a function call *) */
-| IDENT LPAREN old_parameter_list_ne RPAREN old_pardef_list SEMICOLON
- {
- let loc = Cil_datatype.Location.of_lexing_loc $loc($1) in
- (* Convert pardecl to new style *)
- let pardecl, isva = doOldParDecl $3 $5 in
- (* Make the function declarator *)
- doDeclaration None loc []
- [(($1, PROTO(JUSTBASE, pardecl,[],isva),
- ["FC_OLDSTYLEPROTO",[]], loc), NO_INIT)]
- }
-| IDENT LPAREN RPAREN SEMICOLON {
- let loc = Cil_datatype.Location.of_lexing_loc $loc($1) in
- doDeclaration None loc []
- [(($1, PROTO(JUSTBASE,[],[],false),
- ["FC_OLDSTYLEPROTO",[]], loc), NO_INIT)]
+| f=IDENT LPAREN prms=old_parameter_list_ne RPAREN
+ decls=old_pardef_list SEMICOLON
+ {
+ let dloc = Cil_datatype.Location.of_lexing_loc $loc in
+ let floc = Cil_datatype.Location.of_lexing_loc $loc(f) in
+ (* Convert pardecl to new style *)
+ let pardecl, isva = doOldParDecl prms decls in
+ (* Make the function declarator *)
+ doDeclaration None dloc []
+ [((f, PROTO(JUSTBASE, pardecl,[],isva),
+ ["FC_OLDSTYLEPROTO",[]], floc), NO_INIT)]
+ }
+| f=IDENT LPAREN RPAREN SEMICOLON {
+ let dloc = Cil_datatype.Location.of_lexing_loc $loc in
+ let floc = Cil_datatype.Location.of_lexing_loc $loc(f) in
+ doDeclaration None dloc []
+ [((f, PROTO(JUSTBASE,[],[],false),
+ ["FC_OLDSTYLEPROTO",[]], floc), NO_INIT)]
}
;
@@ -759,7 +767,9 @@ constant:
string_constant:
/* Now that we know this constant isn't part of a wstring, convert it
back to a string for easy viewing. */
- string_list { intlist_to_string (fst $1), snd $1 }
+ string_list {
+ let loc = Cil_datatype.Location.of_lexing_loc $loc in
+ intlist_to_string ~loc (fst $1), snd $1 }
;
string_list:
@@ -979,7 +989,7 @@ statement:
let loc = Cil_datatype.Location.of_lexing_loc $loc($1) in
match $4 with
| [] -> (* should not happen if grammar is written correctly *)
- Errorloc.parse_error "empty statement after label"
+ Errorloc.parse_error ~loc "empty statement after label"
| s :: others -> no_ghost [LABEL($1,s,loc)] @ others }
| CASE expression COLON annotated_statement
@@ -1061,32 +1071,40 @@ ghost_parameter:
;
declaration: /* ISO 6.7.*/
- decl_spec_list init_declarator_list SEMICOLON
- { doDeclaration None ((snd $1)) (fst $1) $2 }
-| decl_spec_list SEMICOLON
- { if !Lexerhack.is_typedef () then begin
- let source =
- Cil_datatype.Position.of_lexing_pos $startpos($1)
- in
- Kernel.warning ~source ~wkey:Kernel.wkey_unnamed_typedef
- "typedef without a name"
+ specif=decl_spec_list decls=init_declarator_list SEMICOLON
+ {
+ let loc = Cil_datatype.Location.of_lexing_loc $loc in
+ doDeclaration None loc (fst specif) decls
+ }
+| decls=decl_spec_list SEMICOLON
+ {
+ let loc = Cil_datatype.Location.of_lexing_loc $loc in
+ if !Lexerhack.is_typedef () then begin
+ let source = fst loc in
+ let wkey = Kernel.wkey_unnamed_typedef in
+ Kernel.warning ~source ~wkey "typedef without a name"
end;
!Lexerhack.reset_typedef();
- doDeclaration None ((snd $1)) (fst $1) []
+ doDeclaration None loc (fst decls) []
}
-| SPEC decl_spec_list init_declarator_list SEMICOLON
- { doDeclaration (Some $1) ((snd $2)) (fst $2) $3 }
-| SPEC decl_spec_list SEMICOLON
- { if !Lexerhack.is_typedef () then begin
+| spec=SPEC specif=decl_spec_list decls=init_declarator_list SEMICOLON
+ {
+ let loc = Cil_datatype.Location.of_lexing_loc $loc in
+ doDeclaration (Some spec) loc (fst specif) decls
+ }
+| spec=SPEC specif=decl_spec_list SEMICOLON
+ {
+ let loc = Cil_datatype.Location.of_lexing_loc $loc in
+ if !Lexerhack.is_typedef () then begin
let source =
- Cil_datatype.Position.of_lexing_pos $startpos($2)
+ Cil_datatype.Position.of_lexing_pos $startpos(specif)
in
- Kernel.warning ~source ~wkey:Kernel.wkey_unnamed_typedef
- "typedef without a name"
+ let wkey = Kernel.wkey_unnamed_typedef in
+ Kernel.warning ~source ~wkey "typedef without a name"
end;
!Lexerhack.reset_typedef();
- doDeclaration (Some $1) ((snd $2)) (fst $2) [] }
-| static_assert_declaration
+ doDeclaration (Some spec) loc (fst specif) [] }
+| static_assert_declaration SEMICOLON
{ let (e, m, loc) = $1 in STATIC_ASSERT (e, m, loc) }
;
@@ -1109,7 +1127,8 @@ generic_selection: /* ISO C11 6.5.1.1 */
}
| GENERIC LPAREN assignment_expression RPAREN
{
- Errorloc.parse_error
+ let loc = Cil_datatype.Location.of_lexing_loc $loc in
+ Errorloc.parse_error ~loc
"_Generic requires at least one generic association";
}
@@ -1442,12 +1461,14 @@ pointer_opt:
;
type_name: /* (* ISO 6.7.6 *) */
- decl_spec_list abstract_decl { let d, a = $2 in
- if a <> [] then
- Errorloc.parse_error
- "attributes in type name";
- (fst $1, d)
- }
+ specif=decl_spec_list name=abstract_decl {
+ let d, a = name in
+ if a <> [] then begin
+ let loc = Cil_datatype.Location.of_lexing_loc ($loc(name)) in
+ Errorloc.parse_error ~loc "attributes in type name"
+ end;
+ (fst specif, d)
+ }
| decl_spec_list { (fst $1, JUSTBASE) }
;
abstract_decl: /* (* ISO 6.7.6. *) */
@@ -1556,9 +1577,7 @@ cvspec:
{
let annot, loc = $1 in
if String.compare annot "\\ghost" = 0 then begin
- let start = $startpos in
- let source = Cil_datatype.Position.of_lexing_pos start in
- Errorloc.parse_error ~source "Use of \\ghost out of ghost code"
+ Errorloc.parse_error ~loc "Use of \\ghost out of ghost code"
end else
SpecCV(CV_ATTRIBUTE_ANNOT annot), loc
}
@@ -1834,8 +1853,14 @@ asmattr:
| CONST asmattr { ("const", []) :: $2 }
;
asmtemplate:
- one_string { [intlist_to_string [fst $1]] }
-| one_string asmtemplate { intlist_to_string [fst $1] :: $2 }
+ line=one_string {
+ let loc = Cil_datatype.Location.of_lexing_loc $loc in
+ [intlist_to_string ~loc [fst line]]
+ }
+| line=one_string rest=asmtemplate {
+ let loc = Cil_datatype.Location.of_lexing_loc $loc(line) in
+ intlist_to_string ~loc [fst line] :: rest
+}
;
asmoutputs:
/* empty */ { None }
diff --git a/src/kernel_internals/parsing/errorloc.ml b/src/kernel_internals/parsing/errorloc.ml
index b214658b0ff44b412f30ebf5be6f47ee571fa431..9d1e3669dce6fe5e0e3fada852afb769d27be3f0 100644
--- a/src/kernel_internals/parsing/errorloc.ml
+++ b/src/kernel_internals/parsing/errorloc.ml
@@ -138,19 +138,24 @@ let setCurrentFile n =
}
end
-(* Prints the [pos.pos_lnum]-th line from file [pos.pos_fname],
- plus up to [ctx] lines before and after [pos.pos_lnum] (if they exist),
- similar to 'grep -C<ctx>'. The first line is numbered 1.
+(* Prints the line(s) between start_pos and pos,
+ plus up to [ctx] lines before and after (if they exist),
+ similar to 'grep -C<ctx>'.
Most exceptions are silently caught and printing is stopped if they occur. *)
-let pp_context_from_file ?(ctx=2) ?start_line fmt pos =
+let pp_context_from_file ?(ctx=2) fmt (start_pos, pos) =
+ let open Filepath in
try
- let in_ch = open_in (pos.Filepath.pos_path :> string) in
+ let start_pos =
+ if Normalized.equal start_pos.pos_path pos.pos_path then start_pos
+ else pos
+ in
+ let in_ch = open_in (pos.pos_path :> string) in
try
begin
- let first_error_line, last_error_line =
- match start_line with
- | None -> pos.Filepath.pos_lnum, pos.Filepath.pos_lnum
- | Some l -> min l pos.Filepath.pos_lnum, max l pos.Filepath.pos_lnum
+ let first_error_line, start_char, last_error_line =
+ min start_pos.pos_lnum pos.pos_lnum,
+ (start_pos.pos_cnum - start_pos.pos_bol + 1),
+ max start_pos.pos_lnum pos.pos_lnum
in
(* The difference between the first and last error lines can be very
large; in this case, we print only the first and last [error_ctx]
@@ -161,7 +166,6 @@ let pp_context_from_file ?(ctx=2) ?start_line fmt pos =
let error_height = last_error_line - first_error_line + 1 in
let compress_error = error_height > 2 * error_ctx + 1 + 2 in
let i = ref 1 in
- let error_line_len = ref 0 in
try
(* advance to line *)
while !i < first_to_print do
@@ -187,7 +191,6 @@ let pp_context_from_file ?(ctx=2) ?start_line fmt pos =
!i <= last_error_line - error_ctx then
() (* ignore line *)
else begin
- error_line_len := String.length line;
Format.fprintf fmt "%-6d%s\n" !i line;
end;
incr i
@@ -197,9 +200,13 @@ let pp_context_from_file ?(ctx=2) ?start_line fmt pos =
if last_error_line <> first_error_line then
Format.fprintf fmt "\n"
else begin
+ let len = pos.pos_cnum - pos.pos_bol - start_char + 1 in
+ (* output at least one '^' *)
+ let len = if len = 0 then 1 else len in
let cursor =
String.make 6 ' ' ^
- String.make !error_line_len '^'
+ String.make (start_char - 1) ' ' ^
+ String.make len '^'
in
Format.fprintf fmt "%s\n" cursor
end;
@@ -244,38 +251,37 @@ let pp_location fmt (pos_start, pos_end) =
Format.fprintf fmt "Location: between %a and %a"
pp_pos pos_start pp_pos pos_end
-let parse_error ?source msg =
+let parse_error ?loc msg =
let current = Option.get !current in
- let last_pos =
- match source with
- | None ->
- Cil_datatype.Position.of_lexing_pos current.lexbuf.Lexing.lex_curr_p
- | Some s -> s
- in
(* there are cases when we are called before menhir has requested at
least two tokens, ending up in an assertion failure. Unfortunately,
ErrorReports API does not allow us to check whether the buffer is
empty or not.
*)
+ let all_pos = Stack.create() in
let () =
- try ignore (MenhirLib.ErrorReports.last current.menhir_pos) with _ -> ()
- in
- let start_pos =
+ (* this is absolutely not a hack and used MenhirLib exactly as intended. *)
try
- let pos,_ =
+ let pp loc = Stack.push loc all_pos; "" in
+ ignore (MenhirLib.ErrorReports.show pp current.menhir_pos)
+ with _ -> ()
+ in
+ let loc =
+ match loc with
+ | Some loc -> loc
+ | None ->
+ if Stack.is_empty all_pos then
Cil_datatype.Location.of_lexing_loc
- (MenhirLib.ErrorReports.last current.menhir_pos)
- in
- if Cil_datatype.Position.compare pos last_pos <= 0 then pos
+ (current.lexbuf.Lexing.lex_start_p, current.lexbuf.Lexing.lex_curr_p)
else
- (* during interaction between C and ACSL parser, it might happen,
- at least as long as we haven't completed the move to menhir for
- ACSL, that the start_pos seen by menhir is after the current position
- of the (shared) lexbuf. This would lead to confusing error messages,
- so we drop the one from menhir.
- *)
- last_pos
- with _ -> last_pos
+ let _,start_pos = Stack.pop all_pos in
+ let last_pos =
+ if Stack.is_empty all_pos then
+ current.lexbuf.Lexing.lex_start_p
+ else
+ fst (Stack.pop all_pos)
+ in
+ Cil_datatype.Location.of_lexing_loc (start_pos, last_pos)
in
let pretty_token fmt token =
(* prints more detailed information around the erroneous token;
@@ -287,13 +293,13 @@ let parse_error ?source msg =
Format.fprintf fmt ", before or at token: %s" token
in
Pretty_utils.ksfprintf (fun str ->
- Kernel.feedback ~source:start_pos "%s:@." str
+ Kernel.feedback ~source:(fst loc) "%s:@." str
~append:(fun fmt ->
Format.fprintf fmt "%a%a\n"
- pp_location (start_pos, last_pos)
+ pp_location loc
pretty_token (Lexing.lexeme current.lexbuf);
Format.fprintf fmt "%a@."
- (pp_context_from_file ~start_line:start_pos.Filepath.pos_lnum ~ctx:2) last_pos);
+ (pp_context_from_file ~ctx:2) loc);
raise (Log.AbortError "kernel"))
msg
diff --git a/src/kernel_internals/parsing/errorloc.mli b/src/kernel_internals/parsing/errorloc.mli
index 2935d53572084dc87080568f9f6842d22218abe5..a83180cd21bda8a38594036ed6a639aae1949399 100644
--- a/src/kernel_internals/parsing/errorloc.mli
+++ b/src/kernel_internals/parsing/errorloc.mli
@@ -66,27 +66,32 @@ val finishParsing: unit -> unit (** Call this function to finish parsing and
close the input channel *)
-(** prints the line identified by the position, together with [ctx] lines
+(** prints the line(s) identified by the location, together with [ctx] lines
of context before and after. [ctx] defaults to 2.
- If [start_line] is specified, then all lines between [start_line] and
- [pos.pos_lnum] are considered part of the error.
+ If the location expands to multiple lines, those lines will be separated
+ from context by blank lines.
+ Otherwise, the portion of the line that is between the two positions of
+ the location will be underlined with [^]
+ NB: if the two positions in the location refer to different files, the
+ first position will not be considered.
+ @before Frama-C+dev: the function took as argument a single position and
+ and an optional [start_line] (as an [int]) to indicate a different starting
+ line.
*)
val pp_context_from_file:
- ?ctx:int -> ?start_line:int -> Format.formatter -> Filepath.position -> unit
+ ?ctx:int -> Format.formatter -> Cil_types.location -> unit
(** prints a readable description of a location
@since 22.0-Titanium *)
val pp_location: Format.formatter -> Cil_types.location -> unit
(** Emits the corresponding error message with some location information.
- If given, [source] will be treated as the last position of the offending
- expression that led to the error. It defaults to the current position of
- the lexbuf currently in use (i.e. {!startParsing} must have been called
- before that, and no {!finishParsing} call must have been done in between).
- The start position will be inferred from menhir's error reporting mecanisms.
+ If not given, [location] will be considered to be between the end of
+ the forelast token read by the parser and the start of the last token,
+ i.e. we assume the parser has read an unexpected token.
*)
val parse_error:
- ?source:Filepath.position -> ('a, Format.formatter, unit, 'b) format4 -> 'a
+ ?loc:Cil_types.location -> ('a, Format.formatter, unit, 'b) format4 -> 'a
val had_errors : unit -> bool
(** Has an error been raised since the last call to {!clear_errors}? *)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index c440701e41cd2e4d98ad1cab896990b17a35d205..613d5ee148de1b13ebb7fb05591c2b75dff9b1a7 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -127,11 +127,14 @@ let typeForInsertedVar: (Cil_types.typ -> Cil_types.typ) ref = ref (fun t -> t)
let cabs_exp loc node = { expr_loc = loc; expr_node = node }
-let abort_context msg =
- let pos = fst (Cil.CurrentLoc.get ()) in
+let abort_context ?loc msg =
+ let loc = match loc with
+ | None -> Cil.CurrentLoc.get()
+ | Some loc -> loc
+ in
let append fmt =
Format.pp_print_newline fmt ();
- Errorloc.pp_context_from_file fmt pos
+ Errorloc.pp_context_from_file fmt loc
in
Kernel.abort ~current:true ~append msg
@@ -581,7 +584,8 @@ let check_aligned attrs =
component [ci], and checks the alignment of aligned() attributes.
This function is complemented by
[process_pragmas_pack_align_field_attributes]. *)
-let process_pragmas_pack_align_comp_attributes ci cattrs =
+let process_pragmas_pack_align_comp_attributes loc ci cattrs =
+ let source = snd loc in
match !current_packing_pragma, align_pragma_for_struct ci.corig_name with
| None, None -> check_aligned cattrs
| Some n, apragma ->
@@ -596,7 +600,7 @@ let process_pragmas_pack_align_comp_attributes ci cattrs =
Drop existing "aligned" attributes, if there are invalid ones. *)
if Cil.hasAttribute "packed" cattrs then (dropAttribute "aligned" cattrs)
else begin
- Kernel.feedback ~dkey:Kernel.dkey_typing_pragma ~current:true
+ Kernel.feedback ~source ~dkey:Kernel.dkey_typing_pragma
"adding aligned(%a) attribute to comp '%s' due to packing pragma"
Integer.pretty n ci.cname;
addAttribute (Attr("aligned",[AInt n])) (dropAttribute "aligned" cattrs)
@@ -605,7 +609,7 @@ let process_pragmas_pack_align_comp_attributes ci cattrs =
(* The largest aligned wins with GCC. Don't know
with other compilers. *)
let align = Integer.max n local in
- Kernel.feedback ~dkey:Kernel.dkey_typing_pragma ~current:true
+ Kernel.feedback ~source ~dkey:Kernel.dkey_typing_pragma
"setting aligned(%a) attribute to comp '%s' due to packing pragma"
Integer.pretty align ci.cname;
addAttribute (Attr("aligned",[AInt align]))
@@ -631,6 +635,7 @@ let process_pragmas_pack_align_comp_attributes ci cattrs =
the minimum of both is taken into account (note that, in GCC, if a field
has 2 alignment directives, it is the maximum of those that is taken). *)
let process_pragmas_pack_align_field_attributes fi fattrs cattr =
+ Cil.CurrentLoc.set fi.floc;
match !current_packing_pragma, align_pragma_for_struct fi.forig_name with
| None, None -> check_aligned fattrs
| Some n, apragma ->
@@ -2753,7 +2758,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
@@ -2777,7 +2782,12 @@ let makeGlobalVarinfo (isadef: bool) (vi: varinfo) : varinfo * bool =
formals;
with
| Invalid_argument _ ->
- abort_context "Inconsistent formals" ;
+ abort_context
+ "Function %a redeclared with incompatible formals \
+ (original declaration was at %a)"
+ Cil_datatype.Varinfo.pretty vi
+ Cil_datatype.Location.pretty oldloc
+ ;
| Not_found ->
Cil.setFormalsDecl oldvi vi.vtype)
| _ -> ()
@@ -2942,7 +2952,10 @@ let rec setOneInit this o preinit =
let idx, (* Index in the current comp *)
restoff (* Rest offset *) =
match o with
- | Index({enode = Const(CInt64(i,_,_))}, off) -> to_integer i, off
+ | NoOffset -> assert false
+ | Index({enode = Const(CInt64(i,_,_));eloc}, off) ->
+ CurrentLoc.set eloc;
+ to_integer i, off
| Field (f, off) ->
(* Find the index of the field *)
let rec loop (idx: int) = function
@@ -2958,7 +2971,9 @@ let rec setOneInit this o preinit =
| _ :: restf -> loop (idx + 1) restf
in
loop 0 (Option.value ~default:[] f.fcomp.cfields), off
- | _ -> abort_context "setOneInit: non-constant index"
+ | Index({ eloc },_) ->
+ CurrentLoc.set eloc;
+ abort_context "setOneInit: non-constant index"
in
let pMaxIdx, pArray =
match this with
@@ -3359,6 +3374,7 @@ let integerArrayLength (leno: exp option) : int =
try lenOfArray leno
with
| LenOfArray cause ->
+ Cil.CurrentLoc.set len.eloc;
abort_context
"Array length %a is %a: no explicit initializer allowed."
Cil_printer.pp_exp len Cil.pp_incorrect_array_length cause
@@ -4089,7 +4105,7 @@ let rec nested_call e =
a struct-returning call. *)
let contains_temp_subarray = ref false
-let rec doSpecList ghost (suggestedAnonName: string)
+let rec doSpecList loc ghost (suggestedAnonName: string)
(* This string will be part of
* the names for anonymous
* structures and enums *)
@@ -4270,7 +4286,7 @@ let rec doSpecList ghost (suggestedAnonName: string)
if n <> "" then n else anonStructName "struct" suggestedAnonName in
(* Use the (non-cv, non-name) attributes in !attrs now *)
let a = extraAttrs @ (getTypeAttrs ()) in
- makeCompType ghost true n' ~norig:n nglist (doAttributes ghost a)
+ makeCompType loc ghost true n' ~norig:n nglist (doAttributes ghost a)
| [Cabs.Tunion (n, None, _)] -> (* A reference to a union *)
if n = "" then
@@ -4282,7 +4298,7 @@ let rec doSpecList ghost (suggestedAnonName: string)
if n <> "" then n else anonStructName "union" suggestedAnonName in
(* Use the attributes now *)
let a = extraAttrs @ (getTypeAttrs ()) in
- makeCompType ghost false n' ~norig:n nglist (doAttributes ghost a)
+ makeCompType loc ghost false n' ~norig:n nglist (doAttributes ghost a)
| [Cabs.Tenum (n, None, _)] -> (* Just a reference to an enum *)
if n = "" then
@@ -4441,7 +4457,7 @@ let rec doSpecList ghost (suggestedAnonName: string)
t'
| [Cabs.TtypeofT (specs, dt)] ->
- doOnlyType ghost specs dt
+ doOnlyType loc ghost specs dt
| l ->
abort_context
@@ -4588,9 +4604,9 @@ and doAttr ghost (a: Cabs.attribute) : attribute list =
ACons(n', ae')
end
| Cabs.EXPR_SIZEOF e -> ASizeOfE (ae e)
- | Cabs.TYPE_SIZEOF (bt, dt) -> ASizeOf (doOnlyType ghost bt dt)
+ | Cabs.TYPE_SIZEOF (bt, dt) -> ASizeOf (doOnlyType loc ghost bt dt)
| Cabs.EXPR_ALIGNOF e -> AAlignOfE (ae e)
- | Cabs.TYPE_ALIGNOF (bt, dt) -> AAlignOf (doOnlyType ghost bt dt)
+ | Cabs.TYPE_ALIGNOF (bt, dt) -> AAlignOf (doOnlyType loc ghost bt dt)
| Cabs.BINARY(Cabs.AND, aa1, aa2) ->
ABinOp(LAnd, ae aa1, ae aa2)
| Cabs.BINARY(Cabs.OR, aa1, aa2) ->
@@ -4890,7 +4906,7 @@ and doType (ghost:bool) isFuncArg
(* Make the argument as for a formal *)
let doOneArg argl_length is_ghost (s, (n, ndt, a, cloc)) : varinfo =
let ghost = is_ghost || ghost in
- let s' = doSpecList ghost n s in
+ let s' = doSpecList cloc ghost n s in
let vi = makeVarInfoCabs ~ghost ~isformal:true ~isglobal:false
(convLoc cloc) s' (n,ndt,a) in
if isVoidType vi.vtype then begin
@@ -5048,8 +5064,8 @@ and isVariableSizedArray ghost (dt: Cabs.decl_type)
| None -> None
| Some (se, e) -> Some (dt', se, e)
-and doOnlyType ghost (specs: Cabs.spec_elem list) (dt: Cabs.decl_type) : typ =
- let bt',sto,inl,attrs = doSpecList ghost "" specs in
+and doOnlyType loc ghost (specs: Cabs.spec_elem list) (dt: Cabs.decl_type) : typ =
+ let bt',sto,inl,attrs = doSpecList loc ghost "" specs in
if sto <> NoStorage || inl then
Kernel.error ~once:true ~current:true "Storage or inline specifier in type only";
let tres, nattr =
@@ -5060,7 +5076,7 @@ and doOnlyType ghost (specs: Cabs.spec_elem list) (dt: Cabs.decl_type) : typ =
tres
-and makeCompType ghost (isstruct: bool)
+and makeCompType loc ghost (isstruct: bool)
(n: string)
~(norig: string)
(nglist: Cabs.field_group list)
@@ -5080,16 +5096,17 @@ and makeCompType ghost (isstruct: bool)
let addFieldGroup ~last:last_group (flds : fieldinfo list)
((s: Cabs.spec_elem list), (nl: (Cabs.name * Cabs.expression option) list)) =
(* Do the specifiers exactly once *)
- let sugg = match nl with
- | [] -> ""
- | ((n, _, _, _), _) :: _ -> n
+ let sugg,loc = match nl with
+ | [] -> "",CurrentLoc.get()
+ | ((n, _, _, loc), _) :: _ -> n,loc
in
- let bt, sto, inl, attrs = doSpecList ghost sugg s in
+ let bt, sto, inl, attrs = doSpecList loc ghost sugg s in
(* Do the fields *)
let addFieldInfo ~last:last_field (flds : fieldinfo list)
(((n,ndt,a,cloc) : Cabs.name), (widtho : Cabs.expression option))
: fieldinfo list =
let source = fst cloc in
+ Cil.CurrentLoc.set cloc;
if sto <> NoStorage || inl then
Kernel.error ~once:true ~source "Storage or inline not allowed for fields";
let allowZeroSizeArrays = Cil.gccMode () || Cil.msvcMode () in
@@ -5206,7 +5223,8 @@ and makeCompType ghost (isstruct: bool)
(* abort and not error, as this circularity could lead
to infinite recursion... *)
abort_context
- "type %s %s is circular"
+ "field %s declaration contains a circular reference to type %s %s"
+ fname
(if comp.cstruct then "struct" else "union")
comp.cname;
end else
@@ -5303,7 +5321,7 @@ and makeCompType ghost (isstruct: bool)
(* ignore (E.log "makeComp: %s: %a\n" comp.cname d_attrlist a); *)
let a = Cil.addAttributes comp.cattr a in
- comp.cattr <- process_pragmas_pack_align_comp_attributes comp a;
+ comp.cattr <- process_pragmas_pack_align_comp_attributes loc comp a;
let res = TComp (comp, []) in
(* Create a typedef for this one *)
cabsPushGlobal (GCompTag (comp, CurrentLoc.get ()));
@@ -5313,11 +5331,11 @@ and makeCompType ghost (isstruct: bool)
(* Now create a typedef with just this type *)
res
-and preprocessCast ghost (specs: Cabs.specifier)
+and preprocessCast loc ghost (specs: Cabs.specifier)
(dt: Cabs.decl_type)
(ie: Cabs.init_expression)
: Cabs.specifier * Cabs.decl_type * Cabs.init_expression =
- let typ = doOnlyType ghost specs dt in
+ let typ = doOnlyType loc ghost specs dt in
(* If we are casting to a union type then we have to treat this as a
* constructor expression. This is to handle the gcc extension that allows
* cast from a type of a field to the type of the union *)
@@ -5728,7 +5746,7 @@ and doExp local_env
end
| Cabs.TYPE_SIZEOF (bt, dt) ->
- let typ = doOnlyType local_env.is_ghost bt dt in
+ let typ = doOnlyType loc local_env.is_ghost bt dt in
fail_if_incompatible_sizeof ~ensure_complete:true "sizeof" typ;
let res = new_exp ~loc (SizeOf typ) in
finishExp [] (unspecified_chunk empty) res theMachine.typeOfSizeOf
@@ -5755,7 +5773,7 @@ and doExp local_env
finishExp [] scope_chunk size theMachine.typeOfSizeOf
| Cabs.TYPE_ALIGNOF (bt, dt) ->
- let typ = doOnlyType local_env.is_ghost bt dt in
+ let typ = doOnlyType loc local_env.is_ghost bt dt in
fail_if_incompatible_sizeof ~ensure_complete:true "alignof" typ;
let res = new_exp ~loc (AlignOf typ) in
finishExp [] (unspecified_chunk empty) res theMachine.typeOfSizeOf
@@ -5777,9 +5795,9 @@ and doExp local_env
theMachine.typeOfSizeOf
| Cabs.CAST ((specs, dt), ie) ->
- let s', dt', ie' = preprocessCast local_env.is_ghost specs dt ie in
+ let s', dt', ie' = preprocessCast loc local_env.is_ghost specs dt ie in
(* We know now that we can do s' and dt' many times *)
- let typ = doOnlyType local_env.is_ghost s' dt' in
+ let typ = doOnlyType loc local_env.is_ghost s' dt' in
let what' =
match what with
| AExp (Some _) -> AExp (Some typ)
@@ -5806,7 +5824,7 @@ and doExp local_env
* variable *)
let newvar = "__constr_expr_" ^ string_of_int (!constrExprId) in
incr constrExprId;
- let spec_res = doSpecList local_env.is_ghost "" s' in
+ let spec_res = doSpecList loc local_env.is_ghost "" s' in
let se1 =
if !scopes == [] then begin
(* This is a global. Mark the new vars as static *)
@@ -5814,7 +5832,7 @@ and doExp local_env
let t, _, inl, attrs = spec_res in
t, Static, inl, attrs
in
- ignore (createGlobal local_env.is_ghost None spec_res'
+ ignore (createGlobal loc local_env.is_ghost None spec_res'
((newvar, dt', [], loc), ie'));
(unspecified_chunk empty)
end else
@@ -7344,6 +7362,7 @@ and doExp local_env
| Ok control_t ->
let has_default, assocs =
List.fold_left (fun (has_default, acc) (type_name, expr) ->
+ let loc = expr.expr_loc in
match type_name with
| None -> (* default *)
if has_default then
@@ -7351,7 +7370,7 @@ and doExp local_env
"multiple default clauses in _Generic selection";
true, ((None, expr) :: acc)
| Some (spec, dt) ->
- let t = doOnlyType ghost spec dt in
+ let t = doOnlyType loc ghost spec dt in
if not (Cil.isCompleteType t) then
abort_context
"generic association with incomplete type '%a'"
@@ -7888,7 +7907,7 @@ and doFullExp local_env const e what =
(* there is a sequence point after a full exp *)
empty @@@ (se', ghost), e',t
-and doInitializer local_env (vi: varinfo) (inite: Cabs.init_expression)
+and doInitializer loc local_env (vi: varinfo) (inite: Cabs.init_expression)
(* Return the accumulated chunk, the initializer and the new type (might be
* different for arrays), together with the lvals read during evaluation of
* the initializer (for local intialization)
@@ -7914,7 +7933,7 @@ and doInitializer local_env (vi: varinfo) (inite: Cabs.init_expression)
let acc, preinit, restl =
let so = makeSubobj vi vi.vtype NoOffset in
let asconst = if vi.vglob then CConst else CNoConst in
- doInit local_env asconst Extlib.nop NoInitPre so
+ doInit loc local_env asconst Extlib.nop NoInitPre so
(unspecified_chunk empty) [ (Cabs.NEXT_INIT, inite) ]
in
if restl <> [] then
@@ -7953,14 +7972,17 @@ and doInitializer local_env (vi: varinfo) (inite: Cabs.init_expression)
– preinit corresponding to the complete initialization
– the list of unused initializers if any (should be empty most of the time)
*)
-and doInit local_env asconst add_implicit_ensures preinit so acc initl =
+and doInit loc local_env asconst add_implicit_ensures preinit so acc initl =
+ CurrentLoc.set loc;
+ let source = fst loc in
let ghost = local_env.is_ghost in
let whoami fmt = Cil_printer.pp_lval fmt (Var so.host, so.soOff) in
let initl1 =
match initl with
| (Cabs.NEXT_INIT,
- Cabs.SINGLE_INIT ({ expr_node = Cabs.CAST ((s, dt), ie)} as e)) :: rest ->
- let s', dt', ie' = preprocessCast ghost s dt ie in
+ Cabs.SINGLE_INIT
+ ({ expr_node = Cabs.CAST ((s, dt), ie); expr_loc} as e)) :: rest ->
+ let s', dt', ie' = preprocessCast expr_loc ghost s dt ie in
(Cabs.NEXT_INIT,
Cabs.SINGLE_INIT
({expr_node = Cabs.CAST ((s', dt'), ie'); expr_loc = e.expr_loc}))
@@ -7973,9 +7995,12 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
match initl1 with
| (what,
Cabs.SINGLE_INIT
- ({expr_node = Cabs.CAST ((specs, dt), Cabs.COMPOUND_INIT ci)})) :: rest ->
- let s', dt', _ie' = preprocessCast ghost specs dt (Cabs.COMPOUND_INIT ci) in
- let typ = doOnlyType ghost s' dt' in
+ ({expr_node = Cabs.CAST ((specs, dt), Cabs.COMPOUND_INIT ci);
+ expr_loc})) :: rest ->
+ let s', dt', _ie' =
+ preprocessCast expr_loc ghost specs dt (Cabs.COMPOUND_INIT ci)
+ in
+ let typ = doOnlyType expr_loc ghost s' dt' in
if Typ.equal
(Cil.typeDeepDropAllAttributes typ)
(Cil.typeDeepDropAllAttributes so.soTyp)
@@ -8055,14 +8080,14 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
so'.stack <- [InArray(so'.curOff, bt, leno, ref 0)];
normalSubobj so';
let acc', preinit', initl' =
- doInit local_env asconst add_implicit_ensures preinit so' acc charinits in
+ doInit loc local_env asconst add_implicit_ensures preinit so' acc charinits in
if initl' <> [] then
- Kernel.warning ~current:true
+ Kernel.warning ~source
"Too many initializers for character array %t" whoami;
(* Advance past the array *)
advanceSubobj so;
(* Continue *)
- doInit local_env asconst add_implicit_ensures preinit' so acc' restil
+ doInit loc local_env asconst add_implicit_ensures preinit' so acc' restil
(* If we are at an array of WIDE characters and the initializer is a
* WIDE string literal (optionally enclosed in braces) then explore
* the WIDE string into characters *)
@@ -8128,7 +8153,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
so'.stack <- [InArray(so'.curOff, bt, leno, ref 0)];
normalSubobj so';
let acc', preinit', initl' =
- doInit local_env asconst add_implicit_ensures preinit so' acc charinits
+ doInit loc local_env asconst add_implicit_ensures preinit so' acc charinits
in
if initl' <> [] then
(* sm: see above regarding ISO 6.7.8 para 14, which is not implemented
@@ -8139,7 +8164,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
(* Advance past the array *)
advanceSubobj so;
(* Continue *)
- doInit local_env asconst add_implicit_ensures preinit' so acc' restil
+ doInit loc local_env asconst add_implicit_ensures preinit' so acc' restil
(* If we are at an array and we see a single initializer then it must
* be one for the first element *)
| TArray(bt, leno, _), (Cabs.NEXT_INIT, Cabs.SINGLE_INIT _oneinit) :: _restil ->
@@ -8148,12 +8173,12 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
so.stack <- InArray(so.soOff, bt, leno, ref 0) :: so.stack;
normalSubobj so;
(* Start over with the fields *)
- doInit local_env asconst add_implicit_ensures preinit so acc allinitl
+ doInit loc local_env asconst add_implicit_ensures preinit so acc allinitl
(* An incomplete structure with any initializer is an error. *)
| TComp (comp, _), _ :: restil when comp.cfields = None ->
Kernel.error ~current:true ~once:true
"variable `%s' has initializer but incomplete type" so.host.vname;
- doInit local_env asconst add_implicit_ensures preinit so acc restil
+ doInit loc local_env asconst add_implicit_ensures preinit so acc restil
(* If we are at a composite and we see a single initializer of the same
* type as the composite then grab it all. If the type is not the same
* then we must go on and try to initialize the fields *)
@@ -8171,12 +8196,12 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
(* Advance to the next subobject *)
advanceSubobj so;
let se = acc @@@ (se, ghost) in
- doInit local_env asconst add_implicit_ensures preinit so se restil
+ doInit loc local_env asconst add_implicit_ensures preinit so se restil
end else begin (* Try to initialize fields *)
let toinit = fieldsToInit comp None in
so.stack <- InComp(so.soOff, comp, toinit) :: so.stack;
normalSubobj so;
- doInit local_env asconst add_implicit_ensures preinit so acc allinitl
+ doInit loc local_env asconst add_implicit_ensures preinit so acc allinitl
end
(* A scalar with a single initializer *)
@@ -8196,7 +8221,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
(* Move on *)
advanceSubobj so;
let se = acc @@@ (se,ghost) in
- doInit local_env asconst add_implicit_ensures preinit' so se restil
+ doInit loc local_env asconst add_implicit_ensures preinit' so se restil
(* An array with a compound initializer. The initializer is for the
* array elements *)
| TArray (bt, leno, _), (Cabs.NEXT_INIT, Cabs.COMPOUND_INIT initl) :: restil ->
@@ -8219,7 +8244,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
acc, preinit', []
| _ ->
doInit
- local_env asconst add_implicit_ensures preinit so' acc initl
+ loc local_env asconst add_implicit_ensures preinit so' acc initl
in
if initl' <> [] then
Kernel.warning ~current:true
@@ -8227,7 +8252,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
(* Advance past the array *)
advanceSubobj so;
(* Continue *)
- doInit local_env asconst add_implicit_ensures preinit' so acc' restil
+ doInit loc local_env asconst add_implicit_ensures preinit' so acc' restil
(* We have a designator that tells us to select the matching union field.
* This is to support a GCC extension *)
| TComp(ci, _) as targ,
@@ -8252,14 +8277,14 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
(* If this is a cast from union X to union X *)
if Typ.equal t'noattr (Cil.typeDeepDropAllAttributes targ) then
doInit
- local_env asconst add_implicit_ensures preinit so acc
+ loc local_env asconst add_implicit_ensures preinit so acc
[(Cabs.NEXT_INIT, Cabs.SINGLE_INIT oneinit)]
else
(* If this is a GNU extension with field-to-union cast find the field *)
let fi = findField (Option.value ~default:[] ci.cfields) in
(* Change the designator and redo *)
doInit
- local_env asconst add_implicit_ensures preinit so acc
+ loc local_env asconst add_implicit_ensures preinit so acc
[Cabs.INFIELD_INIT (fi.fname, Cabs.NEXT_INIT), Cabs.SINGLE_INIT oneinit]
(* A structure with a composite initializer. We initialize the fields*)
@@ -8277,14 +8302,14 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
let preinit' = setOneInit preinit so'.curOff (empty_preinit()) in
acc, preinit', []
| _ ->
- doInit local_env asconst add_implicit_ensures preinit so' acc initl
+ doInit loc local_env asconst add_implicit_ensures preinit so' acc initl
in
if initl' <> [] then
Kernel.warning ~current:true "Too many initializers for structure";
(* Advance past the structure *)
advanceSubobj so;
(* Continue *)
- doInit local_env asconst add_implicit_ensures preinit' so acc' restil
+ doInit loc local_env asconst add_implicit_ensures preinit' so acc' restil
(* A scalar with a initializer surrounded by a number of braces *)
| t, (Cabs.NEXT_INIT, next) :: restil ->
begin
@@ -8306,7 +8331,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
(* Move on *)
advanceSubobj so;
let se = acc @@@ (se, ghost) in
- doInit local_env asconst add_implicit_ensures preinit' so se restil
+ doInit loc local_env asconst add_implicit_ensures preinit' so se restil
with Not_found ->
abort_context
"scalar value (of type %a) initialized by compound initializer"
@@ -8337,6 +8362,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
end
| Cabs.ATINDEX_INIT(idx, whatnext) -> begin
+ CurrentLoc.set idx.expr_loc;
match unrollType so.soTyp with
| TArray (bt, leno, _) ->
let ilen = integerArrayLength leno in
@@ -8391,6 +8417,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
in
let doidxs = add_reads ~ghost idxs'.eloc rs doidxs in
let doidxe = add_reads ~ghost idxe'.eloc re doidxe in
+ Cil.CurrentLoc.set (fst idxs'.eloc, snd idxe'.eloc);
if isNotEmpty doidxs || isNotEmpty doidxe then
abort_context "Range designators are not constants";
let first, last =
@@ -8416,11 +8443,11 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
:: loop (i + 1)
in
doInit
- local_env asconst add_implicit_ensures preinit so acc (loop first)
+ loc local_env asconst add_implicit_ensures preinit so acc (loop first)
| Cabs.NEXT_INIT -> (* We have not found any RANGE *)
let acc' = addressSubobj so what acc in
doInit
- local_env asconst add_implicit_ensures preinit so acc'
+ loc local_env asconst add_implicit_ensures preinit so acc'
((Cabs.NEXT_INIT, ie) :: restil)
in
expandRange (fun x -> x) what
@@ -8429,7 +8456,7 @@ and doInit local_env asconst add_implicit_ensures preinit so acc initl =
(* Create and add to the file (if not already added) a global. Return the
* varinfo *)
-and createGlobal ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool * Cabs.attribute list))
+and createGlobal loc ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool * Cabs.attribute list))
(((n,ndt,a,cloc), inite) : Cabs.init_name) : varinfo =
Kernel.debug ~dkey:Kernel.dkey_typing_global "createGlobal: %s" n;
(* If the global is a Frama-C builtin, set the generated flag *)
@@ -8481,7 +8508,9 @@ and createGlobal ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool * C
if inite = Cabs.NO_INIT then
None
else
- let se, ie', et, _ = doInitializer (ghost_local_env ghost) vi inite in
+ let se, ie', et, _ =
+ doInitializer loc (ghost_local_env ghost) vi inite
+ in
(* Maybe we now have a better type? Use the type of the
* initializer only if it really differs from the type of
* the variable. *)
@@ -8715,7 +8744,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
(* Maybe we have a function prototype in local scope. Make it global. We
* do this even if the storage is Static *)
| _ when isProto ndt ->
- let vi = createGlobal ghost None specs init_name in
+ let vi = createGlobal loc ghost None specs init_name in
(* Add it to the environment to shadow previous decls *)
addLocalToEnv ghost n (EnvVar vi);
LocalFuncHook.apply vi;
@@ -8760,7 +8789,9 @@ and createLocal ghost ((_, sto, _, _) as specs)
if inite = Cabs.NO_INIT then
None
else begin
- let se, ie', et, _ = doInitializer (ghost_local_env ghost) vi inite in
+ let se, ie', et, _ =
+ doInitializer loc (ghost_local_env ghost) vi inite
+ in
(* Maybe we now have a better type? Use the type of the
* initializer only if it really differs from the type of
* the variable. *)
@@ -8789,7 +8820,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
then
Kernel.error ~current:true
"\'extern\' local variable cannot have an initializer";
- let vi = createGlobal ghost None specs init_name in
+ let vi = createGlobal loc ghost None specs init_name in
(* Add it to the local environment to ensure that it shadows previous
* local variables *)
addLocalToEnv ghost n (EnvVar vi);
@@ -8919,7 +8950,9 @@ and createLocal ghost ((_, sto, _, _) as specs)
(* TODO: if vi occurs in se4, this is not a real initialization. *)
vi.vdefined <- true;
contains_temp_subarray := false;
- let se4, ie', et, r = doInitializer (ghost_local_env ghost) vi inite in
+ let se4, ie', et, r =
+ doInitializer loc (ghost_local_env ghost) vi inite
+ in
let se4 = cleanup_autoreference vi se4 in
(* Fix the length *)
if Cil.isUnsizedArrayType vi.vtype && Cil.isSizedArrayType et
@@ -9007,7 +9040,8 @@ and doAliasFun ghost vtype (thisname:string) (othername:string)
(* Do one declaration *)
and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
| Cabs.DECDEF (logic_spec, (s, nl), loc) ->
- CurrentLoc.set (convLoc loc);
+ let cloc = convLoc loc in
+ CurrentLoc.set cloc;
(* Do the specifiers exactly once *)
let sugg =
match nl with
@@ -9015,10 +9049,11 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
| ((n, _, _, _), _) :: _ -> n
in
let ghost = local_env.is_ghost in
- let spec_res = doSpecList ghost sugg s in
+ let spec_res = doSpecList cloc ghost sugg s in
(* Do all the variables and concatenate the resulting statements *)
let doOneDeclarator (acc: chunk) (name: init_name) =
let (n,ndt,a,l),_ = name in
+ CurrentLoc.set l;
if isglobal then begin
let bt,_,_,attrs = spec_res in
let vtype, nattr =
@@ -9026,14 +9061,14 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
(AttrName false) bt (Cabs.PARENTYPE(attrs, ndt, a)) in
(match filterAttributes "alias" nattr with
| [] -> (* ordinary prototype. *)
- ignore (createGlobal local_env.is_ghost logic_spec spec_res name)
+ ignore (createGlobal l local_env.is_ghost logic_spec spec_res name)
(* E.log "%s is not aliased\n" name *)
| [Attr("alias", [AStr othername])] ->
if not (isFunctionType vtype) || local_env.is_ghost then begin
Kernel.warning ~current:true
"%a: CIL only supports attribute((alias)) for C functions."
Cil_printer.pp_location (CurrentLoc.get ());
- ignore (createGlobal ghost logic_spec spec_res name)
+ ignore (createGlobal l ghost logic_spec spec_res name)
end else
doAliasFun ghost vtype n othername (s, (n,ndt,a,l)) loc
| _ ->
@@ -9162,7 +9197,7 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
* We'll do it later *)
transparentUnionArgs := [];
- let bt,sto,inl,attrs = doSpecList local_env.is_ghost n specs in
+ let bt,sto,inl,attrs = doSpecList idloc local_env.is_ghost n specs in
!currentFunctionFDEC.svar.vinline <- inl;
let ftyp, funattr =
doType local_env.is_ghost false
@@ -9552,7 +9587,9 @@ and doTypedef ghost ((specs, nl): Cabs.name_group) =
"block-level typedefs currently unsupported;@ \
trying to convert it to a global-level typedef.@ \
Note that this may lead to incoherent error messages.";
- let bt, sto, inl, attrs = doSpecList ghost (suggestAnonName nl) specs in
+ let bt, sto, inl, attrs =
+ doSpecList (CurrentLoc.get()) ghost (suggestAnonName nl) specs
+ in
if sto <> NoStorage || inl then
Kernel.error ~once:true ~current:true
"Storage or inline specifier not allowed in typedef";
@@ -9651,7 +9688,9 @@ and doTypedef ghost ((specs, nl): Cabs.name_group) =
List.iter createTypedef nl
and doOnlyTypedef ghost (specs: Cabs.spec_elem list) : unit =
- let bt, sto, inl, attrs = doSpecList ghost "" specs in
+ let bt, sto, inl, attrs =
+ doSpecList (CurrentLoc.get()) ghost "" specs
+ in
if sto <> NoStorage || inl then
Kernel.error ~once:true ~current:true
"Storage or inline specifier not allowed in typedef";
@@ -10178,7 +10217,7 @@ and doStatement local_env (s : Cabs.statement) : chunk =
match var with
| None -> Catch_all
| Some (t,(n,ndt,a,ldecl)) ->
- let spec = doSpecList ghost n t in
+ let spec = doSpecList ldecl ghost n t in
let vi =
makeVarInfoCabs
~ghost ~isformal:false ~isglobal:false ldecl spec (n,ndt,a)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 6bfd4b301b5030ac589ec72bea962aa88381dffd..c25b28616c1630da8af6b913405f86babc1d7b08 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -71,10 +71,10 @@ let () = Log.set_current_source (fun () -> fst (CurrentLoc.get ()))
let pp_thisloc fmt = Location.pretty fmt (CurrentLoc.get ())
let abort_context msg =
- let pos = fst (CurrentLoc.get ()) in
+ let loc = CurrentLoc.get () in
let append fmt =
Format.pp_print_newline fmt ();
- Errorloc.pp_context_from_file fmt pos
+ Errorloc.pp_context_from_file fmt loc
in
Kernel.abort ~current:true ~append msg
diff --git a/src/plugins/aorai/utils_parser.ml b/src/plugins/aorai/utils_parser.ml
index e12815ab464a6ec87380121b1c7dbb4425a73680..f23a21f5898553216e22419821d67dd1e2ff5c8a 100644
--- a/src/plugins/aorai/utils_parser.ml
+++ b/src/plugins/aorai/utils_parser.ml
@@ -25,15 +25,17 @@
open Lexing
-let current_loc lex = Cil_datatype.Position.of_lexing_pos (lexeme_start_p lex)
-
let abort_current lex fmt =
- let source = current_loc lex in
- let start_line = source.Filepath.pos_lnum in
+ let start_pos =
+ Cil_datatype.Position.of_lexing_pos (lexeme_start_p lex)
+ in
+ let end_pos =
+ Cil_datatype.Position.of_lexing_pos (lexeme_end_p lex)
+ in
let fmt = "before or at token %s@\n%a@\n" ^^ fmt in
- Aorai_option.abort ~source fmt
+ Aorai_option.abort fmt
(Lexing.lexeme lex)
- (Errorloc.pp_context_from_file ~start_line ~ctx:2) source
+ (Errorloc.pp_context_from_file ~ctx:2) (start_pos,end_pos)
let unknown_token lex =
abort_current lex
diff --git a/src/plugins/aorai/utils_parser.mli b/src/plugins/aorai/utils_parser.mli
index 94495b62110040746c4b95118a696feec6cc7c6d..65d6018cc86c8d969b9696ef6d211d79e07d264a 100644
--- a/src/plugins/aorai/utils_parser.mli
+++ b/src/plugins/aorai/utils_parser.mli
@@ -25,10 +25,6 @@
(** utilities for parsing automaton's formulas *)
-(** returns the position corresponding to the
- current character in the lexbuf. *)
-val current_loc: Lexing.lexbuf -> Cil_datatype.Position.t
-
(** aborts the execution using current lexbuf position as source. *)
val abort_current:
Lexing.lexbuf -> ('a, Format.formatter, unit, 'b) format4 -> 'a
diff --git a/tests/misc/oracle/bts0451.res.oracle b/tests/misc/oracle/bts0451.res.oracle
index 909322412f84fc085ec941eaeb91d24b853f3097..0fbb9f6d610f59aa42578578fc8b9fd172bc3c66 100644
--- a/tests/misc/oracle/bts0451.res.oracle
+++ b/tests/misc/oracle/bts0451.res.oracle
@@ -4,7 +4,7 @@
25 /* should abort with an error at type-checking */
26 int main (void) {
27 break;
- ^^^^^^^^
+ ^^^^^^
28 return 0;
29 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/misc/oracle/pragma-pack.0.res.oracle b/tests/misc/oracle/pragma-pack.0.res.oracle
index 54c851ec7707c8feeb46ac865037b0081924c601..ad555d0abd1141433579884bf370aa2f0b3c7627 100644
--- a/tests/misc/oracle/pragma-pack.0.res.oracle
+++ b/tests/misc/oracle/pragma-pack.0.res.oracle
@@ -83,28 +83,28 @@
packing pragma: restoring alignment to default (16)
[kernel:typing:pragma] pragma-pack.c:135:
packing pragma: pushing alignment 16, setting alignment to 4
-[kernel:typing:pragma] pragma-pack.c:136:
+[kernel:typing:pragma] pragma-pack.c:137:
adding aligned(1) attribute to field '__anonstruct_test1_1.i' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:136:
+[kernel:typing:pragma] pragma-pack.c:138:
setting aligned(2) attribute to field '__anonstruct_test1_1.j' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:136:
+[kernel:typing:pragma] pragma-pack.c:139:
adding aligned(4) attribute to field '__anonstruct_test1_1.k' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:136:
+[kernel:typing:pragma] pragma-pack.c:140:
adding aligned(1) attribute to field '__anonstruct_test1_1.l' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:136:
+[kernel:typing:pragma] pragma-pack.c:141:
adding aligned(4) attribute to comp '__anonstruct_test1_1' due to packing pragma
[kernel:typing:pragma] pragma-pack.c:142: packing pragma: popped alignment 16
[kernel:typing:pragma] pragma-pack.c:152:
packing pragma: pushing alignment 16, setting alignment to 1
-[kernel:typing:pragma] pragma-pack.c:153:
+[kernel:typing:pragma] pragma-pack.c:154:
adding aligned(1) attribute to field '__anonstruct_test2_3.i' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:153:
+[kernel:typing:pragma] pragma-pack.c:155:
setting aligned(1) attribute to field '__anonstruct_test2_3.j' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:153:
+[kernel:typing:pragma] pragma-pack.c:156:
adding aligned(1) attribute to field '__anonstruct_test2_3.k' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:153:
+[kernel:typing:pragma] pragma-pack.c:157:
adding aligned(1) attribute to field '__anonstruct_test2_3.l' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:153:
+[kernel:typing:pragma] pragma-pack.c:158:
adding aligned(1) attribute to comp '__anonstruct_test2_3' due to packing pragma
[kernel:typing:pragma] pragma-pack.c:159: packing pragma: popped alignment 16
[kernel:typing:pragma] pragma-pack.c:169:
@@ -112,53 +112,53 @@
[kernel:typing:pragma] pragma-pack.c:176: packing pragma: popped alignment 16
[kernel:typing:pragma] pragma-pack.c:186:
packing pragma: pushing alignment 16, setting alignment to 2
-[kernel:typing:pragma] pragma-pack.c:187:
+[kernel:typing:pragma] pragma-pack.c:189:
setting aligned(2) attribute to field '__anonstruct_test4_7.j' due to packing pragma
[kernel:typing:pragma] pragma-pack.c:193: packing pragma: popped alignment 16
[kernel:typing:pragma] pragma-pack.c:203:
packing pragma: pushing alignment 16, setting alignment to 2
-[kernel:typing:pragma] pragma-pack.c:204:
+[kernel:typing:pragma] pragma-pack.c:206:
setting aligned(2) attribute to field '__anonstruct_test5_9.j' due to packing pragma
[kernel:typing:pragma] pragma-pack.c:210: packing pragma: popped alignment 16
[kernel:typing:pragma] pragma-pack.c:220:
packing pragma: pushing alignment 16, setting alignment to 2
-[kernel:typing:pragma] pragma-pack.c:221:
+[kernel:typing:pragma] pragma-pack.c:223:
setting aligned(2) attribute to field '__anonstruct_test6_11.j' due to packing pragma
[kernel:typing:pragma] pragma-pack.c:227: packing pragma: popped alignment 16
[kernel:typing:pragma] pragma-pack.c:237:
packing pragma: pushing alignment 16, setting alignment to 2
-[kernel:typing:pragma] pragma-pack.c:238:
+[kernel:typing:pragma] pragma-pack.c:239:
adding aligned(1) attribute to field '__anonstruct_test7_13.i' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:238:
+[kernel:typing:pragma] pragma-pack.c:240:
setting aligned(2) attribute to field '__anonstruct_test7_13.j' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:238:
+[kernel:typing:pragma] pragma-pack.c:241:
adding aligned(1) attribute to field '__anonstruct_test7_13.q' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:238:
+[kernel:typing:pragma] pragma-pack.c:242:
adding aligned(2) attribute to field '__anonstruct_test7_13.p' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:238:
+[kernel:typing:pragma] pragma-pack.c:243:
adding aligned(2) attribute to field '__anonstruct_test7_13.k' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:238:
+[kernel:typing:pragma] pragma-pack.c:244:
adding aligned(1) attribute to field '__anonstruct_test7_13.l' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:238:
+[kernel:typing:pragma] pragma-pack.c:245:
adding aligned(2) attribute to comp '__anonstruct_test7_13' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:246:
+[kernel:typing:pragma] pragma-pack.c:247:
adding aligned(2) attribute to field '__anonstruct_test7_2_14.i' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:246:
+[kernel:typing:pragma] pragma-pack.c:248:
adding aligned(1) attribute to field '__anonstruct_test7_2_14.j' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:246:
+[kernel:typing:pragma] pragma-pack.c:249:
adding aligned(2) attribute to field '__anonstruct_test7_2_14.k' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:246:
+[kernel:typing:pragma] pragma-pack.c:250:
adding aligned(2) attribute to field '__anonstruct_test7_2_14.l' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:246:
+[kernel:typing:pragma] pragma-pack.c:251:
adding aligned(2) attribute to comp '__anonstruct_test7_2_14' due to packing pragma
[kernel:typing:pragma] pragma-pack.c:252: packing pragma: popped alignment 16
[kernel:typing:pragma] pragma-pack.c:336:
packing pragma: pushing alignment 16, setting alignment to 1
-[kernel:typing:pragma] pragma-pack.c:337:
+[kernel:typing:pragma] pragma-pack.c:338:
adding aligned(1) attribute to field '__anonstruct_barcode_bmp_t_18.len' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:337:
+[kernel:typing:pragma] pragma-pack.c:339:
adding aligned(1) attribute to field '__anonstruct_barcode_bmp_t_18.data' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:337:
+[kernel:typing:pragma] pragma-pack.c:340:
adding aligned(1) attribute to comp '__anonstruct_barcode_bmp_t_18' due to packing pragma
[kernel:typing:pragma] pragma-pack.c:341: packing pragma: popped alignment 16
[eva] Analyzing a complete application starting at main
diff --git a/tests/spec/oracle/unfinished-oneline-acsl-comment.res.oracle b/tests/spec/oracle/unfinished-oneline-acsl-comment.res.oracle
index 12300c4682afe8c8db6a4939368017208a6c4ab1..e07c4fee78450068368a28fab4c4d6251952807c 100644
--- a/tests/spec/oracle/unfinished-oneline-acsl-comment.res.oracle
+++ b/tests/spec/oracle/unfinished-oneline-acsl-comment.res.oracle
@@ -5,5 +5,5 @@
4 */
5 // If you edit this file, make sure it ends WITHOUT a newline
6 //@ bad
- ^^^^^^^
+ ^
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/value/empty_base.c b/tests/syntax/empty_base.c
similarity index 100%
rename from tests/value/empty_base.c
rename to tests/syntax/empty_base.c
diff --git a/tests/syntax/error_end_decl.i b/tests/syntax/error_end_decl.i
new file mode 100644
index 0000000000000000000000000000000000000000..8fba5808d557f51da3eabbd664511175c1405fdd
--- /dev/null
+++ b/tests/syntax/error_end_decl.i
@@ -0,0 +1,13 @@
+/* run.config
+EXIT: 1
+STDOPT:
+*/
+
+/*@ assigns *p \from \nothing; */
+void f(char *p)
+
+/*@
+ assigns \result \from \nothing;
+ ensures \result == 0;
+*/
+char g(char *p);
diff --git a/tests/syntax/localisation_error.i b/tests/syntax/localisation_error.i
new file mode 100644
index 0000000000000000000000000000000000000000..c591e3490c99a3a0c4a87dd1987014cb1b0aa5f3
--- /dev/null
+++ b/tests/syntax/localisation_error.i
@@ -0,0 +1,8 @@
+/* run.config*
+EXIT: 1
+STDOPT:
+*/
+int main() {
+ int b = 0;
+ //@ ghost int a = 2; /*@ assert a == 3; */ /* test */ */
+}
diff --git a/tests/syntax/oracle/arg_type.res.oracle b/tests/syntax/oracle/arg_type.res.oracle
index 256d77be54eea88d5de89856edfa865ae4cd8abf..e38a0c4a8dbc72717d5f9bc66287becec04d567d 100644
--- a/tests/syntax/oracle/arg_type.res.oracle
+++ b/tests/syntax/oracle/arg_type.res.oracle
@@ -7,5 +7,5 @@
13 int g(int);
14
15 int g(short x) { return x; }
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/array_cast_bts1099.res.oracle b/tests/syntax/oracle/array_cast_bts1099.res.oracle
index 09ba17a47e269d5a40446c613f67d7d35cd6f4fd..9ba1eb0a36322413703fb4d5a80be7b78a5cd690 100644
--- a/tests/syntax/oracle/array_cast_bts1099.res.oracle
+++ b/tests/syntax/oracle/array_cast_bts1099.res.oracle
@@ -4,6 +4,6 @@
10 int tab1[4];
11 u* p = &tab1;
12 t* p2 = (t) p;
- ^^^^^^^^^^^^^^^^
+ ^^^^^
13 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/binary_op.0.res.oracle b/tests/syntax/oracle/binary_op.0.res.oracle
index 60dc2afc775623a14bdbf16138e62b32b11d1e61..ba9b4df4645c004647be9328520a4ac831ecd04a 100644
--- a/tests/syntax/oracle/binary_op.0.res.oracle
+++ b/tests/syntax/oracle/binary_op.0.res.oracle
@@ -4,7 +4,7 @@
9
10 #ifdef BITWISE
11 int v(void) { return 0 & v; }
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^
12 #endif
13
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/binary_op.1.res.oracle b/tests/syntax/oracle/binary_op.1.res.oracle
index b896f4027b9e1e78d89cc8d7ee7d295179e244cb..3c36f99b1ba2ca134d9bf826a1cfb7919a94580a 100644
--- a/tests/syntax/oracle/binary_op.1.res.oracle
+++ b/tests/syntax/oracle/binary_op.1.res.oracle
@@ -4,7 +4,7 @@
13
14 #ifdef MULT
15 int w(void) { return 0 * w; }
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^
16 #endif
17
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/cert_msc_38.0.res.oracle b/tests/syntax/oracle/cert_msc_38.0.res.oracle
index 35b7a148eb975f2de2aba45c97a7c741df1d3ab6..f6a1827a00ee1aa706ca699b14dfed85be6f92fc 100644
--- a/tests/syntax/oracle/cert_msc_38.0.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.0.res.oracle
@@ -6,7 +6,7 @@
24 void func(int e) {
25 // error: assert must be a macro, not a function
26 execute_handler(&(assert), e < 0);
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^
27 }
28
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/cert_msc_38.3.res.oracle b/tests/syntax/oracle/cert_msc_38.3.res.oracle
index 218315e21b14ed0d0a190d1042df3801383989b1..2e259dde2946d6569e10c5a4cc95a858c1737dbe 100644
--- a/tests/syntax/oracle/cert_msc_38.3.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.3.res.oracle
@@ -6,7 +6,7 @@
41 // error: can't suppress va_* macros
42 #ifdef TEST_VASTART
43 void *(*test1)() = &(va_start);
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^
44 #endif
45
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/cert_msc_38.4.res.oracle b/tests/syntax/oracle/cert_msc_38.4.res.oracle
index 0fc570c7b670da969e4e103274aa5a031fa77d53..0ede081258a48c2c8b7b39f35ea4dbf7c520b3c9 100644
--- a/tests/syntax/oracle/cert_msc_38.4.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.4.res.oracle
@@ -6,7 +6,7 @@
45
46 #ifdef TEST_VACOPY
47 void (*test2)() = &(va_copy);
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^
48 #endif
49
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/cert_msc_38.5.res.oracle b/tests/syntax/oracle/cert_msc_38.5.res.oracle
index 880f1b230eb0b5c44e5c6b09bc3c209c356842c9..9d7c6211083229cedc0417493187e8962410c61c 100644
--- a/tests/syntax/oracle/cert_msc_38.5.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.5.res.oracle
@@ -6,7 +6,7 @@
49
50 #ifdef TEST_VAARG
51 void* (*test3)() = &(va_arg);
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^
52 #endif
53
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/cert_msc_38.6.res.oracle b/tests/syntax/oracle/cert_msc_38.6.res.oracle
index 507ff0d508144acc5759a7f2a9199a02ecaf923a..7ae19b28c59175c9f7070afea5a74d61cb984a01 100644
--- a/tests/syntax/oracle/cert_msc_38.6.res.oracle
+++ b/tests/syntax/oracle/cert_msc_38.6.res.oracle
@@ -6,7 +6,7 @@
53
54 #ifdef TEST_VAEND
55 void (*test4)() = &(va_end);
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^
56 #endif
57
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/const-assignments.1.res.oracle b/tests/syntax/oracle/const-assignments.1.res.oracle
index fa6f9af638d0448cc55fd8c5a71071d0c5d2b33d..36093e3713d667b3a4b4c14a4afbdb667e6ffcab 100644
--- a/tests/syntax/oracle/const-assignments.1.res.oracle
+++ b/tests/syntax/oracle/const-assignments.1.res.oracle
@@ -4,7 +4,7 @@
20 #ifdef T0
21 void f() {
22 x = 42;
- ^^^^^^^^^
+ ^^^^^^
23 }
24 #endif
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/const-assignments.2.res.oracle b/tests/syntax/oracle/const-assignments.2.res.oracle
index 2dc9215a35ac450654652550a7134ac578f0d973..02f6615a1ee9edc00bfd905532236f7cd552ff30 100644
--- a/tests/syntax/oracle/const-assignments.2.res.oracle
+++ b/tests/syntax/oracle/const-assignments.2.res.oracle
@@ -4,7 +4,7 @@
26 #ifdef T1
27 void f() {
28 x++;
- ^^^^^^
+ ^^^
29 }
30 #endif
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/const-assignments.3.res.oracle b/tests/syntax/oracle/const-assignments.3.res.oracle
index 23e5bce2386bd9bb6e8994cb30b9b89d71e63abf..d2d7a5d27abb6ffa65c46316ea62d0cd041fce66 100644
--- a/tests/syntax/oracle/const-assignments.3.res.oracle
+++ b/tests/syntax/oracle/const-assignments.3.res.oracle
@@ -4,7 +4,7 @@
32 #ifdef T2
33 void f() {
34 --x;
- ^^^^^^
+ ^^^
35 }
36 #endif
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/const-assignments.4.res.oracle b/tests/syntax/oracle/const-assignments.4.res.oracle
index e1fc81de7638961470872331b6a7e2ace1f35cef..f773542dfc5f2fbc140fbeee5c59bb82fa9b2994 100644
--- a/tests/syntax/oracle/const-assignments.4.res.oracle
+++ b/tests/syntax/oracle/const-assignments.4.res.oracle
@@ -4,7 +4,7 @@
38 #ifdef T3
39 void f() {
40 x += 3;
- ^^^^^^^^^
+ ^^^^^^
41 }
42 #endif
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/const-assignments.5.res.oracle b/tests/syntax/oracle/const-assignments.5.res.oracle
index 6149ca6c14a7ef7f6b9b4cb653bace5472af8f22..1bc8881f49e26ef1b0188b643d9189325442879c 100644
--- a/tests/syntax/oracle/const-assignments.5.res.oracle
+++ b/tests/syntax/oracle/const-assignments.5.res.oracle
@@ -4,7 +4,7 @@
45 void f() {
46 const int x = 2;
47 x *= 2;
- ^^^^^^^^^
+ ^^^^^^
48 }
49 #endif
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/const-assignments.6.res.oracle b/tests/syntax/oracle/const-assignments.6.res.oracle
index 75d299175cdf14a4c23369123383d94c83412930..0a47849f5a7f32f7bdd6893625e758209a9117c1 100644
--- a/tests/syntax/oracle/const-assignments.6.res.oracle
+++ b/tests/syntax/oracle/const-assignments.6.res.oracle
@@ -4,7 +4,7 @@
51 #ifdef T5
52 void f(const int* x) {
53 *x = 1;
- ^^^^^^^^^
+ ^^^^^^
54 }
55 #endif
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/const-assignments.9.res.oracle b/tests/syntax/oracle/const-assignments.9.res.oracle
index 1eac0647def6c209d2ae35d2137f82a76bcaecde..195a24229577ea26b31a04c6abd36f9f2b5c8eaa 100644
--- a/tests/syntax/oracle/const-assignments.9.res.oracle
+++ b/tests/syntax/oracle/const-assignments.9.res.oracle
@@ -4,7 +4,7 @@
119
120 void mutable_test_ko(const T* t) {
121 t->s.y = 32; // KO: although t->s could be modified, t->s.y is still const
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^
122 }
123
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/value/oracle/empty_base.0.res.oracle b/tests/syntax/oracle/empty_base.0.res.oracle
similarity index 87%
rename from tests/value/oracle/empty_base.0.res.oracle
rename to tests/syntax/oracle/empty_base.0.res.oracle
index e0b917dec36cf5e98a9ca3de169f9f4359d6f917..989cc122c482b696749c24b9c8b580a7edafcc1f 100644
--- a/tests/value/oracle/empty_base.0.res.oracle
+++ b/tests/syntax/oracle/empty_base.0.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing empty_base.c (with preprocessing)
[kernel] empty_base.c:63: User Error:
variable `c' has initializer but incomplete type
-[kernel] empty_base.c:67: Warning: Too many initializers for structure
+[kernel] empty_base.c:70: Warning: Too many initializers for structure
[kernel] empty_base.c:81: User Error:
non-final field `f1' declared with a type containing a flexible array member.
[kernel] User Error: stopping on file "empty_base.c" that has errors. Add '-kernel-msg-key pp'
diff --git a/tests/value/oracle/empty_base.1.res.oracle b/tests/syntax/oracle/empty_base.1.res.oracle
similarity index 96%
rename from tests/value/oracle/empty_base.1.res.oracle
rename to tests/syntax/oracle/empty_base.1.res.oracle
index bba69f8432c7a4c311b70f979773601645d4e353..b4a399dcf365d8ce1b017d51ac57d98c3821e4f4 100644
--- a/tests/value/oracle/empty_base.1.res.oracle
+++ b/tests/syntax/oracle/empty_base.1.res.oracle
@@ -14,7 +14,7 @@
48 struct empty empty_array_of_empty[0];
49 struct empty array_of_empty[1];
50 struct empty many_empty[3] = {{}};
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^
51
52 comp array_of_comp[1] = {{.a = 17, .b = 45, .e = {}}};
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/error_end_decl.res.oracle b/tests/syntax/oracle/error_end_decl.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ffb6550d934e416b1ee2c60557afcee58f92af38
--- /dev/null
+++ b/tests/syntax/oracle/error_end_decl.res.oracle
@@ -0,0 +1,16 @@
+[kernel] Parsing error_end_decl.i (no preprocessing)
+[kernel] error_end_decl.i:7:
+ syntax error:
+ Location: between lines 7 and 12
+ 5
+ 6 /*@ assigns *p \from \nothing; */
+
+ 7 void f(char *p)
+ 8
+ 9 /*@
+ 10 assigns \result \from \nothing;
+ 11 ensures \result == 0;
+ 12 */
+
+ 13 char g(char *p);
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/fam.res.oracle b/tests/syntax/oracle/fam.res.oracle
index b1c6f8aa9bbee30d31e9c8fcf31e1ad48a40be91..55eb9b89b58a3ee32fa7fa58cd00993ad81f2c7b 100644
--- a/tests/syntax/oracle/fam.res.oracle
+++ b/tests/syntax/oracle/fam.res.oracle
@@ -1,15 +1,15 @@
[kernel] Parsing fam.i (no preprocessing)
-[kernel] fam.i:16: User Error:
+[kernel] fam.i:19: User Error:
static initialization of flexible array members is an unsupported GNU extension
[kernel] fam.i:29: User Error:
field `b' is declared with incomplete type char []
-[kernel] fam.i:28: User Error:
+[kernel] fam.i:31: User Error:
static initialization of flexible array members is an unsupported GNU extension
-[kernel] fam.i:49: User Error:
+[kernel] fam.i:56: User Error:
static initialization of flexible array members is an unsupported GNU extension
[kernel] fam.i:63: User Error:
static initialization of flexible array members is an unsupported GNU extension
-[kernel] fam.i:77: User Error:
+[kernel] fam.i:84: User Error:
static initialization of flexible array members is an unsupported GNU extension
[kernel] User Error: stopping on file "fam.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/func_locs.res.oracle b/tests/syntax/oracle/func_locs.res.oracle
index 8fd4ca099e2fa45737df2beec4c827b0473d0f65..3a3c61326536ab13d1b041577c80b9912a250734 100644
--- a/tests/syntax/oracle/func_locs.res.oracle
+++ b/tests/syntax/oracle/func_locs.res.oracle
@@ -3,8 +3,8 @@
found two contracts (old location: func_locs.i:13). Merging them
func_locs.i:31 char 3 - func_locs.i:36 char 1 -> main
func_locs.i:27 char 4 - func_locs.i:29 char 1 -> def_no_spec
-func_locs.i:25 char 20 - func_locs.i:25 char 26 -> id
-func_locs.i:25 char 0 - func_locs.i:25 char 16 -> decl_no_spec
+func_locs.i:25 char 24 - func_locs.i:25 char 26 -> id
+func_locs.i:25 char 4 - func_locs.i:25 char 16 -> decl_no_spec
func_locs.i:20 char 3 - func_locs.i:23 char 6 -> id
func_locs.i:13 char 3 - func_locs.i:18 char 6 -> id
func_locs.i:7 char 3 - func_locs.i:9 char 1 -> with_spec
diff --git a/tests/syntax/oracle/function_ptr_lvalue_1.res.oracle b/tests/syntax/oracle/function_ptr_lvalue_1.res.oracle
index 0eca364b644783f7bffc52806e552a4d1ac4eb80..e5ce52792dbd7cc2bb7339417a402b1cc66eb3db 100644
--- a/tests/syntax/oracle/function_ptr_lvalue_1.res.oracle
+++ b/tests/syntax/oracle/function_ptr_lvalue_1.res.oracle
@@ -4,7 +4,7 @@
11 void (*p)(void) = &f ;
12 p = 1 ;
13 *p = 1 ;
- ^^^^^^^^^^
+ ^^^^^^
14 return 0 ;
15 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/function_ptr_lvalue_2.res.oracle b/tests/syntax/oracle/function_ptr_lvalue_2.res.oracle
index 4bcdf11602646662df1553ed1c6d4b60bd297b50..e86474631363d992b654fe27948ccfac60aab5da 100644
--- a/tests/syntax/oracle/function_ptr_lvalue_2.res.oracle
+++ b/tests/syntax/oracle/function_ptr_lvalue_2.res.oracle
@@ -4,7 +4,7 @@
10 void (*p)(void) = &f ;
11 p = &f ;
12 *p = f ;
- ^^^^^^^^^^
+ ^^^^^^
13 return 0 ;
14 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.1.res.oracle b/tests/syntax/oracle/generic.1.res.oracle
index 07cb4e0900f35bf7656e01f4c4da47c996398609..c8f6605be6dcb690f616c3dd9bcdf7fc7226ea19 100644
--- a/tests/syntax/oracle/generic.1.res.oracle
+++ b/tests/syntax/oracle/generic.1.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing generic.c (with preprocessing)
[kernel] generic.c:36:
_Generic requires at least one generic association:
- Location: line 36, between columns 25 and 26, before or at token: ;
+ Location: line 36, between columns 10 and 25, before or at token: ;
34 int main() {
35 #ifdef NONE
36 int a = _Generic("abc");
- ^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^
37 #endif
38 #ifdef TOO_MANY_DEFAULTS
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.2.res.oracle b/tests/syntax/oracle/generic.2.res.oracle
index 97bc6f5808c4546a36098776a764a2b82d62c921..0edc5626dfd5157572f29d022cfbf997a14fba98 100644
--- a/tests/syntax/oracle/generic.2.res.oracle
+++ b/tests/syntax/oracle/generic.2.res.oracle
@@ -4,7 +4,7 @@
37 #endif
38 #ifdef TOO_MANY_DEFAULTS
39 int a = _Generic("abc", default: 1, default: 1);
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
40 #endif
41 #ifdef TOO_MANY_COMPATIBLE
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.3.res.oracle b/tests/syntax/oracle/generic.3.res.oracle
index e683c048013d632828688464c432aacd535c1d5c..af00e69e6f9a9db9d0453d3965d5af3f92f4deb1 100644
--- a/tests/syntax/oracle/generic.3.res.oracle
+++ b/tests/syntax/oracle/generic.3.res.oracle
@@ -5,7 +5,7 @@
41 #ifdef TOO_MANY_COMPATIBLE
42 // compatibility via typedef
43 int a = _Generic(42, my_uint: 1, unsigned int: 2);
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
44 #endif
45 #ifdef TOO_MANY_COMPATIBLE2
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.4.res.oracle b/tests/syntax/oracle/generic.4.res.oracle
index f1c86c668f3b5d44078dd2fad20ee3189ae350f2..4dea267e9f5cf04b162f789e3847a6714d99c8a0 100644
--- a/tests/syntax/oracle/generic.4.res.oracle
+++ b/tests/syntax/oracle/generic.4.res.oracle
@@ -4,8 +4,11 @@
'void (*)()' and 'void (*)(void)'
45 #ifdef TOO_MANY_COMPATIBLE2
46 // compatibility modulo implicit arguments
+
47 int a = _Generic(0,
- ^^^^^^^^^^^^^^^^^^^^^
48 void (*)(): 0,
49 void (*)(void): 0);
+
+ 50 #endif
+ 51 #ifdef TOO_MANY_COMPATIBLE3
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.5.res.oracle b/tests/syntax/oracle/generic.5.res.oracle
index 47db165e125863871e8aa11d51329b948954a9ff..579b9dde7959145550bcea41382a8e721f40b21d 100644
--- a/tests/syntax/oracle/generic.5.res.oracle
+++ b/tests/syntax/oracle/generic.5.res.oracle
@@ -5,8 +5,11 @@
compatible types: void (*)(void), void (*)(int )
52 // implicit arguments compatible between first and second selector,
53 // but the selectors themselves are not compatible between them
+
54 int a = _Generic((void (*)()) 0,
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
55 void (*)(int): 0,
56 void (*)(void): 0);
+
+ 57 #endif
+ 58 #ifdef INCOMPLETE_TYPE
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.6.res.oracle b/tests/syntax/oracle/generic.6.res.oracle
index 17b9dbce578c02ed0e29a79f18e4a5cc97fe53bb..fbfffc1be280933ec883e33e343a303d4541dd09 100644
--- a/tests/syntax/oracle/generic.6.res.oracle
+++ b/tests/syntax/oracle/generic.6.res.oracle
@@ -4,7 +4,7 @@
57 #endif
58 #ifdef INCOMPLETE_TYPE
59 int a = _Generic(42, void: 1, default: 2);
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
60 #endif
61 #ifdef FUNCTION_TYPE
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.7.res.oracle b/tests/syntax/oracle/generic.7.res.oracle
index b8635912296f2a8ab067e16ae5cd6c79e617740a..c232c3c417e6f8d49a53f25f9f116dc939d908b2 100644
--- a/tests/syntax/oracle/generic.7.res.oracle
+++ b/tests/syntax/oracle/generic.7.res.oracle
@@ -6,7 +6,7 @@
63 #endif
64 #ifdef INCOMPATIBLE_QUALIFIED_TYPE
65 int a = _Generic("abc", char const *: 0);
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
66 #endif
67 int ok1 = _Generic("abc", char*: 0);
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.8.res.oracle b/tests/syntax/oracle/generic.8.res.oracle
index d07d4fc7c3bf850b4f3952019549118ddfe091e9..fe35717281298c85c4a8ef02888473d4a3b90dce 100644
--- a/tests/syntax/oracle/generic.8.res.oracle
+++ b/tests/syntax/oracle/generic.8.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing generic.c (with preprocessing)
[kernel] generic.c:62:
syntax error:
- Location: line 62, between columns 27 and 30, before or at token: int
+ Location: line 62, column 27, before or at token: int
60 #endif
61 #ifdef FUNCTION_TYPE
62 int a = _Generic(1, void(int): 1);
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^
63 #endif
64 #ifdef INCOMPATIBLE_QUALIFIED_TYPE
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_cv_parsing_errors.0.res.oracle b/tests/syntax/oracle/ghost_cv_parsing_errors.0.res.oracle
index ccbca4666e4df299d560a288b948c2eb45309def..49cee6b2fe416da7b33a5720a1990948067c181d 100644
--- a/tests/syntax/oracle/ghost_cv_parsing_errors.0.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_parsing_errors.0.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing ghost_cv_parsing_errors.c (with preprocessing)
[kernel] ghost_cv_parsing_errors.c:14:
Use of \ghost out of ghost code:
- Location: line 14, between columns 0 and 8, before or at token: \ghost
+ Location: line 14, between columns 2 and 8, before or at token: \ghost
12 struct S {
13 int a ;
14 } \ghost ;
- ^^^^^^^^^^
+ ^^^^^^
15
16 #endif
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_cv_parsing_errors.1.res.oracle b/tests/syntax/oracle/ghost_cv_parsing_errors.1.res.oracle
index c6e7d874a8f04424b00edad07d8149bb2c69a414..0926c5ae2e4187081e7419b260018facdbd518c7 100644
--- a/tests/syntax/oracle/ghost_cv_parsing_errors.1.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_parsing_errors.1.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing ghost_cv_parsing_errors.c (with preprocessing)
[kernel] ghost_cv_parsing_errors.c:20:
Use of \ghost out of ghost code:
- Location: line 20, between columns 0 and 10, before or at token: \ghost
+ Location: line 20, between columns 4 and 10, before or at token: \ghost
18 #ifdef IN_DECL
19
20 int \ghost global ;
- ^^^^^^^^^^^^^^^^^^^
+ ^^^^^^
21
22 #endif
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle b/tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle
index 177a24a98458ddbea40ce3fb9ce2c855712a12bc..23eb9fb13e2f2b46c7f11cc6eceed5cdcec73e4b 100644
--- a/tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing ghost_cv_parsing_errors.c (with preprocessing)
[kernel] ghost_cv_parsing_errors.c:26:
Use of \ghost out of ghost code:
- Location: line 26, column 14, before or at token: global
+ Location: line 26, between columns 8 and 14, before or at token: global
24 #ifdef IN_GHOST_ATTR
25
26 int /*@ \ghost */ global ;
- ^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^
27
28 #endif
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_else_bad.0.res.oracle b/tests/syntax/oracle/ghost_else_bad.0.res.oracle
index 8c7597d919f243915e628427efbabb963df4021e..687b31dd0c0961e5eaa0d3866eabc41c09b62d8f 100644
--- a/tests/syntax/oracle/ghost_else_bad.0.res.oracle
+++ b/tests/syntax/oracle/ghost_else_bad.0.res.oracle
@@ -4,7 +4,7 @@
18 } */
19
20 z = 42;
- ^^^^^^^^^
+ ^
21 }
22
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_else_bad.2.res.oracle b/tests/syntax/oracle/ghost_else_bad.2.res.oracle
index 6664996b0f909d093330a7b0984499f8053f65bf..c72e9cf52cd938bacdb4e12ebebc45366787f0b6 100644
--- a/tests/syntax/oracle/ghost_else_bad.2.res.oracle
+++ b/tests/syntax/oracle/ghost_else_bad.2.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing ghost_else_bad.c (with preprocessing)
[kernel] ghost_else_bad.c:49:
syntax error:
- Location: line 49, between columns 5 and 9, before or at token: else
+ Location: line 49, between columns 0 and 5, before or at token: else
47 } /*@ ghost
48 //@ ensures \true ;
49 else {
- ^^^^^^^^^^
+ ^^^^^
50 y++ ;
51 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_else_bad_oneline.res.oracle b/tests/syntax/oracle/ghost_else_bad_oneline.res.oracle
index 2b50bccd39dedcfb69009075669398cfe856ba20..031c56441d08521ae27a25634ff32eb4c0791a1a 100644
--- a/tests/syntax/oracle/ghost_else_bad_oneline.res.oracle
+++ b/tests/syntax/oracle/ghost_else_bad_oneline.res.oracle
@@ -1,13 +1,12 @@
[kernel] Parsing ghost_else_bad_oneline.i (no preprocessing)
[kernel] ghost_else_bad_oneline.i:8:
syntax error:
- Location: between lines 8 and 9, before or at token:
+ Location: line 8, column 18, before or at token:
6 if (x) {
7 x++;
-
8 } //@ ghost else
+ ^
9 y++;
-
10 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_local_ill_formed.res.oracle b/tests/syntax/oracle/ghost_local_ill_formed.res.oracle
index db076a7b7a6ec433049a8b98e4ce8eb693c051ac..fcab3b6edda80dcf54a7d33a081288b9362689f8 100644
--- a/tests/syntax/oracle/ghost_local_ill_formed.res.oracle
+++ b/tests/syntax/oracle/ghost_local_ill_formed.res.oracle
@@ -7,6 +7,6 @@
19 //@ ghost int c = 0;
20 // ill-formed: the instruction should be ghost as well
21 c++;
- ^^^^^^
+ ^
22 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_multiline_annot.1.res.oracle b/tests/syntax/oracle/ghost_multiline_annot.1.res.oracle
index 1d4cfa1f5eb3b23af4f9b17b55bd11353f216e58..4e2d22bea4b4c24a002f034f8ac7c0ce57f4f367 100644
--- a/tests/syntax/oracle/ghost_multiline_annot.1.res.oracle
+++ b/tests/syntax/oracle/ghost_multiline_annot.1.res.oracle
@@ -1,11 +1,10 @@
[kernel] Parsing ghost_multiline_annot.c (with preprocessing)
-[kernel] ghost_multiline_annot.c:34:
+[kernel] ghost_multiline_annot.c:35:
Ghost multi-line annotation not terminated:
- Location: between lines 34 and 41
- 32 {
+ Location: between lines 35 and 41
33 /*@ ghost
-
34 int x = 10;
+
35 /@ loop invariant x >= 0;
36 loop assigns x;
37 loop variant x;
diff --git a/tests/syntax/oracle/ghost_multiline_annot.2.res.oracle b/tests/syntax/oracle/ghost_multiline_annot.2.res.oracle
index f78f3f7ccd20e4a34d9a03388a0fb55e9db7e090..77dc1648f28a1fae531786aad864e14528d49d60 100644
--- a/tests/syntax/oracle/ghost_multiline_annot.2.res.oracle
+++ b/tests/syntax/oracle/ghost_multiline_annot.2.res.oracle
@@ -1,13 +1,11 @@
[kernel] Parsing ghost_multiline_annot.c (with preprocessing)
-[kernel] ghost_multiline_annot.c:48:
+[kernel] ghost_multiline_annot.c:49:
This kind of annotation is valid only inside ghost code:
- Location: between lines 48 and 49, before or at token: /@
- 46 #ifdef P2
+ Location: line 49, between columns 2 and 4, before or at token: /@
47 int main()
-
48 {
49 /@ assert 2 == 2; @/
-
+ ^^
50 return 0;
51 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_multiline_annot.3.res.oracle b/tests/syntax/oracle/ghost_multiline_annot.3.res.oracle
index ca5a43f04dd43c19ee1655ce25e9acc0626720ef..2a1317e6562358993c37fbec5f462d91126a7f27 100644
--- a/tests/syntax/oracle/ghost_multiline_annot.3.res.oracle
+++ b/tests/syntax/oracle/ghost_multiline_annot.3.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing ghost_multiline_annot.c (with preprocessing)
[kernel] ghost_multiline_annot.c:57:
Invalid symbol:
- Location: line 57, between columns 17 and 20, before or at token: @
+ Location: line 57, between columns 19 and 20, before or at token: @
55 int main()
56 {
57 assert (2 == 2); @/
- ^^^^^^^^^^^^^^^^^^^^^
+ ^
58 return 0;
59 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.10.res.oracle b/tests/syntax/oracle/ghost_parameters.10.res.oracle
index 51ba9929f8136b5cb1cc74d0c293a6aca4f25e4c..4da452094df32e2e2da684c45537fc72e9155088 100644
--- a/tests/syntax/oracle/ghost_parameters.10.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.10.res.oracle
@@ -2,11 +2,11 @@
[kernel] ghost_parameters.c:187: User Error:
Declaration of function does not match previous declaration from ghost_parameters.c:181 (different number of arguments).
[kernel] ghost_parameters.c:187: User Error:
- Inconsistent formals
+ Function function redeclared with incompatible formals (original declaration was at ghost_parameters.c:181)
185 }
186
187 void function(int a, int b) /*@ ghost(int c, int d) */ {
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^
188
189 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.11.res.oracle b/tests/syntax/oracle/ghost_parameters.11.res.oracle
index 27c61b15f1593906bbc287ba234bda4c02c8c342..c649da62073f64858ab47dcccc22ee39abbe6a5a 100644
--- a/tests/syntax/oracle/ghost_parameters.11.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.11.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing ghost_parameters.c (with preprocessing)
[kernel] ghost_parameters.c:195:
syntax error:
- Location: line 195, between columns 36 and 37, before or at token: )
+ Location: line 195, column 36, before or at token: )
193 #ifdef VOID_EMPTY_GHOST_PARAMETER_LIST
194
195 void function_void(void) /*@ ghost () */ {
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^
196
197 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.3.res.oracle b/tests/syntax/oracle/ghost_parameters.3.res.oracle
index 3d1e0550a28df50bbbfdbfe592a846c7fc658a3a..38b53517ac2093f1177583a8fa98ed9e2a170e12 100644
--- a/tests/syntax/oracle/ghost_parameters.3.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.3.res.oracle
@@ -2,11 +2,11 @@
[kernel] ghost_parameters.c:92: User Error:
Declaration of function does not match previous declaration from ghost_parameters.c:88 (different number of arguments).
[kernel] ghost_parameters.c:92: User Error:
- Inconsistent formals
+ Function function redeclared with incompatible formals (original declaration was at ghost_parameters.c:88)
90 }
91
92 void function(int a, int b) /*@ ghost(int c, int d) */ {
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^
93
94 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.4.res.oracle b/tests/syntax/oracle/ghost_parameters.4.res.oracle
index 9f9d451cca4d7a3cb7ba454de014cce162e20a84..f07d36bc7a2202eef036a55775edb332bb4a0bc7 100644
--- a/tests/syntax/oracle/ghost_parameters.4.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.4.res.oracle
@@ -2,11 +2,11 @@
[kernel] ghost_parameters.c:106: User Error:
Declaration of function does not match previous declaration from ghost_parameters.c:100 (different number of arguments).
[kernel] ghost_parameters.c:106: User Error:
- Inconsistent formals
+ Function function redeclared with incompatible formals (original declaration was at ghost_parameters.c:100)
104 }
105
106 void function(int a, int b) /*@ ghost(int c, int d) */ {
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^
107
108 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.5.res.oracle b/tests/syntax/oracle/ghost_parameters.5.res.oracle
index 095cbbd26b45e686cc725c04319438085c845161..824a1c0380c7f7f9a77073c40643a3a58e2771fc 100644
--- a/tests/syntax/oracle/ghost_parameters.5.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.5.res.oracle
@@ -2,11 +2,11 @@
[kernel] ghost_parameters.c:119: User Error:
Declaration of function does not match previous declaration from ghost_parameters.c:115 (different number of ghost arguments).
[kernel] ghost_parameters.c:119: User Error:
- Inconsistent formals
+ Function function redeclared with incompatible formals (original declaration was at ghost_parameters.c:115)
117 }
118
119 void function(int a, int b) /*@ ghost(int c, int d) */ {
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^
120
121 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.6.res.oracle b/tests/syntax/oracle/ghost_parameters.6.res.oracle
index d94f2aee4c876a243e9e5420d33fa3611a921a75..6722a5254d4f99af476faa5cf46b1f2f8eb9816e 100644
--- a/tests/syntax/oracle/ghost_parameters.6.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.6.res.oracle
@@ -2,11 +2,11 @@
[kernel] ghost_parameters.c:133: User Error:
Declaration of function does not match previous declaration from ghost_parameters.c:127 (different number of ghost arguments).
[kernel] ghost_parameters.c:133: User Error:
- Inconsistent formals
+ Function function redeclared with incompatible formals (original declaration was at ghost_parameters.c:127)
131 }
132
133 void function(int a, int b) /*@ ghost(int c, int d) */ {
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^
134
135 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.7.res.oracle b/tests/syntax/oracle/ghost_parameters.7.res.oracle
index dae1c5e043d6ea0136c04c3a735b63efe7690ae2..9f9a551e2f6fa4d4fa1803eadce79f51d11b02e7 100644
--- a/tests/syntax/oracle/ghost_parameters.7.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.7.res.oracle
@@ -2,11 +2,11 @@
[kernel] ghost_parameters.c:146: User Error:
Declaration of function does not match previous declaration from ghost_parameters.c:142 (different number of arguments).
[kernel] ghost_parameters.c:146: User Error:
- Inconsistent formals
+ Function function redeclared with incompatible formals (original declaration was at ghost_parameters.c:142)
144 }
145
146 void function(int a, int b) /*@ ghost(int c, int d) */ {
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^
147
148 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.8.res.oracle b/tests/syntax/oracle/ghost_parameters.8.res.oracle
index 30443d6f1138945a5113952ee3796e16f6f18afd..65509b4741fa55b4c21db801098c8b879636601c 100644
--- a/tests/syntax/oracle/ghost_parameters.8.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.8.res.oracle
@@ -2,11 +2,11 @@
[kernel] ghost_parameters.c:160: User Error:
Declaration of function does not match previous declaration from ghost_parameters.c:154 (different number of arguments).
[kernel] ghost_parameters.c:160: User Error:
- Inconsistent formals
+ Function function redeclared with incompatible formals (original declaration was at ghost_parameters.c:154)
158 }
159
160 void function(int a, int b) /*@ ghost(int c, int d) */ {
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^
161
162 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.9.res.oracle b/tests/syntax/oracle/ghost_parameters.9.res.oracle
index ba34ee79c97c3cfffa2603e84dcea6d13a54b0e3..ba008d3a8c743a1da2c43e5d7fa25875ef1aea75 100644
--- a/tests/syntax/oracle/ghost_parameters.9.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.9.res.oracle
@@ -2,11 +2,11 @@
[kernel] ghost_parameters.c:173: User Error:
Declaration of function does not match previous declaration from ghost_parameters.c:169 (different number of arguments).
[kernel] ghost_parameters.c:173: User Error:
- Inconsistent formals
+ Function function redeclared with incompatible formals (original declaration was at ghost_parameters.c:169)
171 }
172
173 void function(int a, int b) /*@ ghost(int c, int d) */ {
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^
174
175 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/incomplete_struct_field.res.oracle b/tests/syntax/oracle/incomplete_struct_field.res.oracle
index f2fe46a7218f4e48596c2a96c4773d15971234f6..75a737c68a9be04685c441563916e714b3d155da 100644
--- a/tests/syntax/oracle/incomplete_struct_field.res.oracle
+++ b/tests/syntax/oracle/incomplete_struct_field.res.oracle
@@ -1,14 +1,14 @@
[kernel] Parsing incomplete_struct_field.i (no preprocessing)
-[kernel] incomplete_struct_field.i:5: User Error:
+[kernel] incomplete_struct_field.i:7: User Error:
declaration of array of incomplete type 'struct _s`
[kernel] incomplete_struct_field.i:7: User Error:
field `v' is declared with incomplete type struct _s [12]
-[kernel] incomplete_struct_field.i:5: User Error:
- type struct _s is circular
- 3 STDOPT:
- 4 */
+[kernel] incomplete_struct_field.i:7: User Error:
+ field v declaration contains a circular reference to type struct _s
5 typedef struct _s {
- ^^^^^^^^^^^^^^^^^^^
6 int i;
7 struct _s v[12];
+ ^
+ 8 } ts;
+ 9
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/inconsistent_global_ghost_spec.0.res.oracle b/tests/syntax/oracle/inconsistent_global_ghost_spec.0.res.oracle
index 91706e15eaf26f9bedcea422d359921b82289b31..9b4dd9a90766818a45943c9ee2e9e289d1bc80e5 100644
--- a/tests/syntax/oracle/inconsistent_global_ghost_spec.0.res.oracle
+++ b/tests/syntax/oracle/inconsistent_global_ghost_spec.0.res.oracle
@@ -5,7 +5,7 @@
9
10 void function(void) ;
11 /*@ ghost void function(void){ } */
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^
12
13 void user(void){
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/inconsistent_global_ghost_spec.1.res.oracle b/tests/syntax/oracle/inconsistent_global_ghost_spec.1.res.oracle
index 366eb65da8bebad673e81287f1547ce7ba696a8c..9c6cce1bd60612b82c08bcbb27e39af7a9581feb 100644
--- a/tests/syntax/oracle/inconsistent_global_ghost_spec.1.res.oracle
+++ b/tests/syntax/oracle/inconsistent_global_ghost_spec.1.res.oracle
@@ -5,7 +5,7 @@
20
21 /*@ ghost void function(void) ; */
22 void function(void){ }
- ^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^
23
24 void user(void){
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/inconsistent_global_ghost_spec.2.res.oracle b/tests/syntax/oracle/inconsistent_global_ghost_spec.2.res.oracle
index 35cfc826665ee35836dba7b90ce92b099648f190..72045be30e748f3a23d52fa5bf88c2f8140ef868 100644
--- a/tests/syntax/oracle/inconsistent_global_ghost_spec.2.res.oracle
+++ b/tests/syntax/oracle/inconsistent_global_ghost_spec.2.res.oracle
@@ -5,7 +5,7 @@
31
32 /*@ ghost void function(void){ } */
33 void function(void) ;
- ^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^
34
35 void user(void){
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/inconsistent_global_ghost_spec.3.res.oracle b/tests/syntax/oracle/inconsistent_global_ghost_spec.3.res.oracle
index d75f41a1ba1dad33bb8bca4163eab7f693a6d10e..d429e28777b75d7f9d2699584783bc69529627c4 100644
--- a/tests/syntax/oracle/inconsistent_global_ghost_spec.3.res.oracle
+++ b/tests/syntax/oracle/inconsistent_global_ghost_spec.3.res.oracle
@@ -5,7 +5,7 @@
42
43 void function(void){ }
44 /*@ ghost void function(void) ; */
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^
45
46 void user(void){
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/init_bts1352.res.oracle b/tests/syntax/oracle/init_bts1352.res.oracle
index f38741556ecfae1c1e706ec18f985659d0687909..e6d8d227b4510643f819c200d7cd3a0fc3d793bc 100644
--- a/tests/syntax/oracle/init_bts1352.res.oracle
+++ b/tests/syntax/oracle/init_bts1352.res.oracle
@@ -4,6 +4,6 @@
6
7 int main(void) {
8 int t /* [5] missing */ = { 1, 2, 3, 4, 5 };
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^
9 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/invalid_implicit_cast_issue_1346.res.oracle b/tests/syntax/oracle/invalid_implicit_cast_issue_1346.res.oracle
index 507b75f850f52a8e8ca5a4fbcb70fed6ce83f536..1d7458f98dd1567775551f62b4177d14d6903e44 100644
--- a/tests/syntax/oracle/invalid_implicit_cast_issue_1346.res.oracle
+++ b/tests/syntax/oracle/invalid_implicit_cast_issue_1346.res.oracle
@@ -5,6 +5,6 @@
12
13 void f(FILE *file) {
14 (*(T*)&B) = 0; // error: implicit cast: cannot cast from int to T
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^
15 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/line_number.res.oracle b/tests/syntax/oracle/line_number.res.oracle
index 8f92b8bb7cdd6e1ddb1e9565c894fd9015e468e1..dba6ed32a4142f9562c93d8de3bde49c7758bf27 100644
--- a/tests/syntax/oracle/line_number.res.oracle
+++ b/tests/syntax/oracle/line_number.res.oracle
@@ -5,6 +5,6 @@
4 */
5
6 //@ assert \result == 0;
- ^^^^^^^^^^^^^^^^^^^^^^^^
+ ^
7 extern int p(void void);
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/localisation_error.res.oracle b/tests/syntax/oracle/localisation_error.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a99a0894ae2dd6de7e3610fbfa264ba454971f9b
--- /dev/null
+++ b/tests/syntax/oracle/localisation_error.res.oracle
@@ -0,0 +1,10 @@
+[kernel] Parsing localisation_error.i (no preprocessing)
+[kernel] localisation_error.i:7:
+ syntax error:
+ Location: line 7, column 57, before or at token: /
+ 5 int main() {
+ 6 int b = 0;
+ 7 //@ ghost int a = 2; /*@ assert a == 3; */ /* test */ */
+ ^
+ 8 }
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/lvalvoid.res.oracle b/tests/syntax/oracle/lvalvoid.res.oracle
index a43dffc8a880f058bfef52ebfded61cdad2cde23..bca0bd162992eb724b4d064e8082d926153db988 100644
--- a/tests/syntax/oracle/lvalvoid.res.oracle
+++ b/tests/syntax/oracle/lvalvoid.res.oracle
@@ -5,7 +5,7 @@
6 char* d=dst; char* s=src;
7 for (int i=0;i<n;i++)
8 d[i]=(char)(src[i]);
- ^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^
9 return dst;
10 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/mutually_recursive_struct.res.oracle b/tests/syntax/oracle/mutually_recursive_struct.res.oracle
index 932ba6a9399444dec741181df9db902b126368a9..1ddf39e0d0663bc42046cd57c4520b597eb6af06 100644
--- a/tests/syntax/oracle/mutually_recursive_struct.res.oracle
+++ b/tests/syntax/oracle/mutually_recursive_struct.res.oracle
@@ -8,11 +8,11 @@
[kernel] mutually_recursive_struct.i:11: User Error:
field `s1' is declared with incomplete type struct S1 [2]
[kernel] mutually_recursive_struct.i:11: User Error:
- type struct S2 is circular
+ field s1 declaration contains a circular reference to type struct S2
9 struct S1 { struct S2 s2[2]; int x; };
10
11 struct S2 { struct S1 s1[2]; int y; };
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^
12
13 int main () {
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/no_prototype.res.oracle b/tests/syntax/oracle/no_prototype.res.oracle
index c3a946c73e7cff7cd41935da87661bed4453c4c2..5cebe4f9f28a2c1a8b524a6f4d57087d5e9ce37c 100644
--- a/tests/syntax/oracle/no_prototype.res.oracle
+++ b/tests/syntax/oracle/no_prototype.res.oracle
@@ -9,7 +9,7 @@
9 foo();
10 }
11 void foo(int a) {
- ^^^^^^^^^^^^^^^^^
+ ^^^
12 int i = a ;
13 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/reject_use_decl_mismatch_bts728.0.res.oracle b/tests/syntax/oracle/reject_use_decl_mismatch_bts728.0.res.oracle
index 76603c68330d472624936e438e76176d33c1e163..bf2f7f89e245cbd71d7a066e6ea9022572e2f2c6 100644
--- a/tests/syntax/oracle/reject_use_decl_mismatch_bts728.0.res.oracle
+++ b/tests/syntax/oracle/reject_use_decl_mismatch_bts728.0.res.oracle
@@ -5,11 +5,11 @@
[kernel] reject_use_decl_mismatch_bts728.c:19: User Error:
Declaration of f does not match previous declaration from reject_use_decl_mismatch_bts728.c:7 (different number of arguments).
[kernel] reject_use_decl_mismatch_bts728.c:19: User Error:
- Inconsistent formals
+ Function f redeclared with incompatible formals (original declaration was at reject_use_decl_mismatch_bts728.c:7)
17 }
18
19 int f(int x,int y, int z, int t,int t1,int t2,int t3,int t4,int t5,int t6) {
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^
20 x = 17;
21 y=18;
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/reject_use_decl_mismatch_bts728.1.res.oracle b/tests/syntax/oracle/reject_use_decl_mismatch_bts728.1.res.oracle
index 177b11f83f9963da63cc7a8b11fde507a1181387..5d84c3028c2971a19e8d2a142c7ed3fe88e0d56a 100644
--- a/tests/syntax/oracle/reject_use_decl_mismatch_bts728.1.res.oracle
+++ b/tests/syntax/oracle/reject_use_decl_mismatch_bts728.1.res.oracle
@@ -4,11 +4,11 @@
[kernel] reject_use_decl_mismatch_bts728.c:19: User Error:
Declaration of f does not match previous declaration from reject_use_decl_mismatch_bts728.c:15 (different number of arguments).
[kernel] reject_use_decl_mismatch_bts728.c:19: User Error:
- Inconsistent formals
+ Function f redeclared with incompatible formals (original declaration was at reject_use_decl_mismatch_bts728.c:15)
17 }
18
19 int f(int x,int y, int z, int t,int t1,int t2,int t3,int t4,int t5,int t6) {
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^
20 x = 17;
21 y=18;
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/spurious_brace_bts_1273.res.oracle b/tests/syntax/oracle/spurious_brace_bts_1273.res.oracle
index 5c29aee6daded821f472bdf4600fe4657cc83294..a7eee9649423c175a124e16cbefcbbacc2ddb639 100644
--- a/tests/syntax/oracle/spurious_brace_bts_1273.res.oracle
+++ b/tests/syntax/oracle/spurious_brace_bts_1273.res.oracle
@@ -1,11 +1,13 @@
[kernel] Parsing spurious_brace_bts_1273.i (no preprocessing)
-[kernel] spurious_brace_bts_1273.i:8:
+[kernel] spurious_brace_bts_1273.i:7:
syntax error:
- Location: line 8, between columns 0 and 1, before or at token: }
+ Location: between lines 7 and 8, before or at token: }
+ 5
6 void foo() {
+
7 }
8 }
- ^
+
9
10 void main () {
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/static_assert_wrong.res.oracle b/tests/syntax/oracle/static_assert_wrong.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6b70ee159b2a50426081d077d4c4b491b89c3d45
--- /dev/null
+++ b/tests/syntax/oracle/static_assert_wrong.res.oracle
@@ -0,0 +1,11 @@
+[kernel] Parsing static_assert_wrong.i (no preprocessing)
+[kernel] static_assert_wrong.i:6:
+ syntax error:
+ Location: between lines 6 and 8, before or at token: int
+ 4 */
+ 5
+
+ 6 _Static_assert(1,"assert succeeds")
+ 7
+ 8 int x = 0;
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/syntactic_hook.res.oracle b/tests/syntax/oracle/syntactic_hook.res.oracle
index 36eadea81f3b5b6bd52fb3eb0797126e9bfe2d4f..22cd7bb63303436f32a7c1ebdd6e5cce200468ef 100644
--- a/tests/syntax/oracle/syntactic_hook.res.oracle
+++ b/tests/syntax/oracle/syntactic_hook.res.oracle
@@ -39,9 +39,9 @@
[kernel] syntactic_hook.i:30: Warning:
[SH]: conflict with declaration of f at line 8: different number of arguments
[kernel] syntactic_hook.i:30: User Error:
- Inconsistent formals
+ Function f redeclared with incompatible formals (original declaration was at syntactic_hook.i:8)
28 }
29
30 int f(int); //error: conflicting decls
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/type_branch_bts_1081.res.oracle b/tests/syntax/oracle/type_branch_bts_1081.res.oracle
index 279e77e82b0a80efa541243786ebfbbf0a8f6e85..ea64e936b23e0310ebda4a4b2c078f8f30ee68f5 100644
--- a/tests/syntax/oracle/type_branch_bts_1081.res.oracle
+++ b/tests/syntax/oracle/type_branch_bts_1081.res.oracle
@@ -4,7 +4,7 @@
8 foo ? (void)x : (signed char)y;
9 // accepted (we drop the expressions, don't care about their types)
10 int z = foo ? (void)x: (signed char)y; // rejected
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
11 return 0;
12 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/typedef_namespace_bts1500.1.res.oracle b/tests/syntax/oracle/typedef_namespace_bts1500.1.res.oracle
index 382925a17d83920679a858652248efddf67a7fcf..6dfc1df3a047e00c0284e137f3bfe697da90b3af 100644
--- a/tests/syntax/oracle/typedef_namespace_bts1500.1.res.oracle
+++ b/tests/syntax/oracle/typedef_namespace_bts1500.1.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing typedef_namespace_bts1500.c (with preprocessing)
[kernel] typedef_namespace_bts1500.c:24:
syntax error:
- Location: line 24, between columns 8 and 9, before or at token: y
+ Location: line 24, between columns 7 and 8, before or at token: y
22 // error: digit is now a variable
23 #ifdef HIDING_TYPEDEF
24 digit y = 5;
- ^^^^^^^^^^^^^^
+ ^
25 #endif
26 return x + digit+A;
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.0.res.oracle b/tests/syntax/oracle/very_large_integers.0.res.oracle
index e366b8133a7e85112801a124416854e98bebead7..130856143cd0476be5cc6627d35715e8bfdf22e7 100644
--- a/tests/syntax/oracle/very_large_integers.0.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.0.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:35: User Error:
+[kernel] very_large_integers.c:36: User Error:
integer constant too large in expression 999999999999999999U + 9999999999999999999U
[kernel] very_large_integers.c:36: User Error:
bitfield width is not a valid integer constant
diff --git a/tests/syntax/oracle/very_large_integers.1.res.oracle b/tests/syntax/oracle/very_large_integers.1.res.oracle
index 543e2f77a34315e860d772c2f77dff770b5c85e6..2a1bce76081fd479209be6cb1e51193270f0fce5 100644
--- a/tests/syntax/oracle/very_large_integers.1.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.1.res.oracle
@@ -4,9 +4,9 @@
Cannot represent the integer 99999999999999999999U
[kernel] very_large_integers.c:42: User Error:
Cannot represent the integer 99999999999999999999U
-[kernel] very_large_integers.c:84: Warning:
+[kernel] very_large_integers.c:86: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:84: Warning:
+[kernel] very_large_integers.c:87: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
diff --git a/tests/syntax/oracle/very_large_integers.10.res.oracle b/tests/syntax/oracle/very_large_integers.10.res.oracle
index 2ad84d77204218912477e33a003703ac20ce4ce7..eac4bf461ee5354f8e6ae4a130ab7a041df0c677 100644
--- a/tests/syntax/oracle/very_large_integers.10.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.10.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:84: Warning:
+[kernel] very_large_integers.c:86: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:84: Warning:
+[kernel] very_large_integers.c:87: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
[kernel] very_large_integers.c:97: User Error:
diff --git a/tests/syntax/oracle/very_large_integers.11.res.oracle b/tests/syntax/oracle/very_large_integers.11.res.oracle
index 7bcdbc1686f6c8bd85fbac11eaa1d86e02c91561..3270a28dd6f5ba3e83b7c88e4fb0e848db680b77 100644
--- a/tests/syntax/oracle/very_large_integers.11.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.11.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:84: Warning:
+[kernel] very_large_integers.c:86: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:84: Warning:
+[kernel] very_large_integers.c:87: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
[kernel:annot-error] very_large_integers.c:132: Warning:
diff --git a/tests/syntax/oracle/very_large_integers.12.res.oracle b/tests/syntax/oracle/very_large_integers.12.res.oracle
index 8b9b72707ecc9fd6c21a7915fd0c220d2c065b3f..dfd952019ddb236a0207da59d1a3fb802c642556 100644
--- a/tests/syntax/oracle/very_large_integers.12.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.12.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:84: Warning:
+[kernel] very_large_integers.c:86: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:84: Warning:
+[kernel] very_large_integers.c:87: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
[kernel] very_large_integers.c:136: User Error:
diff --git a/tests/syntax/oracle/very_large_integers.13.res.oracle b/tests/syntax/oracle/very_large_integers.13.res.oracle
index baa5289f5572f4aa93d8eb04ac649a6b2bb3887d..282be584e672cbbf55e86062804c415161bb0d20 100644
--- a/tests/syntax/oracle/very_large_integers.13.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.13.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:84: Warning:
+[kernel] very_large_integers.c:86: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:84: Warning:
+[kernel] very_large_integers.c:87: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
[kernel] very_large_integers.c:102: User Error:
@@ -9,7 +9,7 @@
100 #ifdef ARRAY_INIT1
101 // Previously caused Invalid_argument(Array.make)
102 int a1[] = {[72057594037927936] = 0};
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^
103 #endif
104
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.14.res.oracle b/tests/syntax/oracle/very_large_integers.14.res.oracle
index bfd5d8b7eb57423236a1136fb001b9e59c49351b..acee0c62d23cdcd3a31efe64314cb577c50d4c19 100644
--- a/tests/syntax/oracle/very_large_integers.14.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.14.res.oracle
@@ -1,16 +1,16 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:84: Warning:
+[kernel] very_large_integers.c:86: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:84: Warning:
+[kernel] very_large_integers.c:87: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
-[kernel] very_large_integers.c:106: User Error: Array length is too large.
-[kernel] very_large_integers.c:113: User Error:
+[kernel] very_large_integers.c:107: User Error: Array length is too large.
+[kernel] very_large_integers.c:114: User Error:
array length too large: 7205759403792794
- 111 };
112 // Previously caused Out of memory
113 struct st s = {
- ^^^^^^^^^^^^^^^
114 {{[7205759403792793 ... 7205759403792793] = 0}}
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
115 };
+ 116 #endif
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.15.res.oracle b/tests/syntax/oracle/very_large_integers.15.res.oracle
index c8f36fffabbea0ea7fb9e8339e9582d4c8feefef..cda1d1f80484ac52850d292c0d1236439396d933 100644
--- a/tests/syntax/oracle/very_large_integers.15.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.15.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:84: Warning:
+[kernel] very_large_integers.c:86: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:84: Warning:
+[kernel] very_large_integers.c:87: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
[kernel] very_large_integers.c:119: User Error:
@@ -9,7 +9,7 @@
117
118 #ifdef ARRAY_INIT3
119 int ai3[] = {0xdead, [72057594037927936] = 0xbeef};
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^
120 #endif
121 #ifdef ARRAY_INIT4
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.16.res.oracle b/tests/syntax/oracle/very_large_integers.16.res.oracle
index 773cecaac1fd5f1a4faf437574f6578214519a23..f8a35d7b077aaec663e8a2c715aa4fb4b49821fa 100644
--- a/tests/syntax/oracle/very_large_integers.16.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.16.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:84: Warning:
+[kernel] very_large_integers.c:86: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:84: Warning:
+[kernel] very_large_integers.c:87: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
[kernel] very_large_integers.c:123: User Error:
@@ -9,7 +9,7 @@
121 #ifdef ARRAY_INIT4
122 // Previously caused Out of memory
123 int ai4[] = {1, [7205759403792793] = 11};
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^
124 #endif
125
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.17.res.oracle b/tests/syntax/oracle/very_large_integers.17.res.oracle
index 3012ddb57d4c817230e4b623ba1731f31374dd26..3358d5f03d550e6db60ecd6b91ac10cfbcfe4eca 100644
--- a/tests/syntax/oracle/very_large_integers.17.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.17.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:84: Warning:
+[kernel] very_large_integers.c:86: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:84: Warning:
+[kernel] very_large_integers.c:87: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
[kernel] very_large_integers.c:141: Warning:
diff --git a/tests/syntax/oracle/very_large_integers.2.res.oracle b/tests/syntax/oracle/very_large_integers.2.res.oracle
index 999706dea413ac6c5c63956a666e93586569bb94..b72cb2ce3d3125db17c085a63e7fdc88d3a091d2 100644
--- a/tests/syntax/oracle/very_large_integers.2.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.2.res.oracle
@@ -6,7 +6,7 @@
47 void case_range() {
48 switch (nondetul)
49 case 0 ... 9999999999999999999U:;
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
50 case 0 ... 199999999999999999U:;
51 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.3.res.oracle b/tests/syntax/oracle/very_large_integers.3.res.oracle
index 7c9ba7c178fdb4909990ec08bd4d6dcf11caf537..2659f34187783f6f3f32c31b89c229f75ee37083 100644
--- a/tests/syntax/oracle/very_large_integers.3.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.3.res.oracle
@@ -4,7 +4,7 @@
55 void case_range2() {
56 switch (nondet)
57 case 0 ... 10000000U:;
- ^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^^^^^^
58 }
59 #endif
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.4.res.oracle b/tests/syntax/oracle/very_large_integers.4.res.oracle
index 77a8b542245f0fbe7d3a2607a9f110cf9a092df9..f30af367582a82c726be86d33ea3487afffee4a2 100644
--- a/tests/syntax/oracle/very_large_integers.4.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.4.res.oracle
@@ -5,7 +5,7 @@
60
61 #ifdef INIT_DESIGNATOR
62 int arr2[9999999999999999999U] = { [9999999999999999999U] = 42 };
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^^^^
63 #endif
64
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.5.res.oracle b/tests/syntax/oracle/very_large_integers.5.res.oracle
index 2dd40615234abca06fe729a6f9805df6005aebe3..71b8acde63287df8b59e062509a2375eb2b3a5a3 100644
--- a/tests/syntax/oracle/very_large_integers.5.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.5.res.oracle
@@ -4,7 +4,7 @@
64
65 #ifdef INIT_DESIGNATOR2
66 int arr3[1] = { [9999999999999999999U] = 42 };
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^^^^
67 #endif
68
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.6.res.oracle b/tests/syntax/oracle/very_large_integers.6.res.oracle
index 8858cc405bb0645d7f38002cae3026c63d295700..a276df46d02a52e4e83faadd7a57ddb0b035a565 100644
--- a/tests/syntax/oracle/very_large_integers.6.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.6.res.oracle
@@ -8,7 +8,7 @@
68
69 #ifdef RANGE_DESIGNATOR
70 int arr4[1] = { [-9999999999999999999U ... 9999999999999999999U] = 42 };
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
71 #endif
72
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.7.res.oracle b/tests/syntax/oracle/very_large_integers.7.res.oracle
index 22ddabcd753fb60429538a5af7d37fb3174b8581..9e0b1da102ea4f9ae9e17219f10d684ce6c480bf 100644
--- a/tests/syntax/oracle/very_large_integers.7.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.7.res.oracle
@@ -4,7 +4,7 @@
72
73 #ifdef RANGE_DESIGNATOR2
74 int widths[] = { [99999999999999999 ... 999999999999999999] = 2 };
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
75 #endif
76
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/very_large_integers.8.res.oracle b/tests/syntax/oracle/very_large_integers.8.res.oracle
index bf9a096053416e2ccb7778ba85efc209edc8d656..b1e5c95fc9b4f87425c186e929588296979e3a35 100644
--- a/tests/syntax/oracle/very_large_integers.8.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.8.res.oracle
@@ -1,9 +1,9 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:79: User Error:
+[kernel] very_large_integers.c:80: User Error:
Invalid attribute constant: 0x80000000000000000
-[kernel] very_large_integers.c:84: Warning:
+[kernel] very_large_integers.c:86: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:84: Warning:
+[kernel] very_large_integers.c:87: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
[kernel] User Error: stopping on file "very_large_integers.c" that has errors. Add
diff --git a/tests/syntax/oracle/very_large_integers.9.res.oracle b/tests/syntax/oracle/very_large_integers.9.res.oracle
index dd5b469d1be2e225d142f3cc3d4a8f65493e6c88..0bfb0f1fa8b50bb3501656fe128231a9eb10ef3f 100644
--- a/tests/syntax/oracle/very_large_integers.9.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.9.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing very_large_integers.c (with preprocessing)
-[kernel] very_large_integers.c:84: Warning:
+[kernel] very_large_integers.c:86: Warning:
ignoring invalid aligned attribute: __aligned__(9223372036854775808)
-[kernel] very_large_integers.c:84: Warning:
+[kernel] very_large_integers.c:87: Warning:
ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
(9223372036854775808) )
[kernel] User Error: Cannot represent logical integer in C: 9999999999999999999
diff --git a/tests/syntax/oracle/wrong-assignment.res.oracle b/tests/syntax/oracle/wrong-assignment.res.oracle
index a6f9c43d92dca9c7475fc7aaaa1761c2613f7ee7..2dd3d505f17b9a5d75d7f5cfd8192ccad7f3e34a 100644
--- a/tests/syntax/oracle/wrong-assignment.res.oracle
+++ b/tests/syntax/oracle/wrong-assignment.res.oracle
@@ -4,6 +4,6 @@
11 void d() {
12 // this assignment should be rejected
13 c.a = b;
- ^^^^^^^^^^
+ ^
14 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/wrong_label.res.oracle b/tests/syntax/oracle/wrong_label.res.oracle
index 8ccccb3e43634dfae541b21c6c3e1429bc8fbc48..3103fda144a35c1adeaed71ffc9a2c418ebcfa60 100644
--- a/tests/syntax/oracle/wrong_label.res.oracle
+++ b/tests/syntax/oracle/wrong_label.res.oracle
@@ -1,10 +1,10 @@
[kernel] Parsing wrong_label.i (no preprocessing)
[kernel] wrong_label.i:11:
syntax error:
- Location: line 11, between columns 8 and 9, before or at token: }
+ Location: line 11, column 8, before or at token: }
9
10 void main() {
11 {_LOR:} // KO: labels can't be at the end of a block.
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^
12 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/static_assert_wrong.i b/tests/syntax/static_assert_wrong.i
new file mode 100644
index 0000000000000000000000000000000000000000..fd27a5c70f7046819343f242140208e72f0692a8
--- /dev/null
+++ b/tests/syntax/static_assert_wrong.i
@@ -0,0 +1,8 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
+_Static_assert(1,"assert succeeds")
+
+int x = 0;
diff --git a/tests/value/oracle/array_zero_length.2.res.oracle b/tests/value/oracle/array_zero_length.2.res.oracle
index 62bce111ca998c475103f11cedc7d16c75c6b07a..440a1beac59d2fbcb72a118f60ae03d9d4638e1f 100644
--- a/tests/value/oracle/array_zero_length.2.res.oracle
+++ b/tests/value/oracle/array_zero_length.2.res.oracle
@@ -11,7 +11,7 @@
11 char W[][0];
12
13 char T1[] = {};
- ^^^^^^^^^^^^^^^
+ ^^
14 char U1[0] = {};
15 char V1[][2] = {};
[kernel] Frama-C aborted: invalid user input.