diff --git a/src/kernel_internals/parsing/errorloc.ml b/src/kernel_internals/parsing/errorloc.ml index 31b21bccd37d9d703941c1526e157e10743e0f27..5ff43c012eca5d04c9146bfa3f80d0c0a53fa136 100644 --- a/src/kernel_internals/parsing/errorloc.ml +++ b/src/kernel_internals/parsing/errorloc.ml @@ -199,10 +199,13 @@ let pp_context_from_file ?(ctx=2) ?start_pos 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 (start_char - 1) ' ' ^ - String.make (pos.pos_cnum - pos.pos_bol - start_char + 1) '^' + String.make len '^' in Format.fprintf fmt "%s\n" cursor end; 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.