Frama-C Bug Tracking System - Frama-C
View Issue Details
0002467Frama-CKernelpublic2019-07-26 16:052019-08-05 16:18
Victor Sverdlin 
signoles 
normalcrashalways
assignedopen 
x86_64opensuse-tumbleweed20190723
Frama-C 19-Potassium 
 
0002467: Crash at "hashtbl.ml", line 462
Raised at file "hashtbl.ml", line 462, characters 17-32
Called from file "src/libraries/project/state_topological.ml", line 62, characters 23-38
Just open new project and add at least one .c (or .h) file
(* Frama-C journal generated at 16:46 the 26/07/2019 *)

exception Unreachable
exception Exception of string

[@@@ warning "-26"]

(* Run the user commands *)
let run () =
  Project.set_keep_current false;
  File.init_from_cmdline ();
  Dynamic.Parameter.String.set ""
    "/media/sf_home/temp/gps_try/sent_LDRA/src/main.c";
  begin try
    (* exception Log.AbortError("kernel") raised on: *)
    File.init_from_cmdline ();
    raise Unreachable
  with
  | Unreachable as exn -> raise exn
  | exn (* Log.AbortError("kernel") *) ->
    (* continuing: *)
    begin try
      (* exception Log.AbortError("kernel") raised on: *)
      File.prepare_from_c_files ();
      raise Unreachable
    with
    | Unreachable as exn -> raise exn
    | exn (* Log.AbortError("kernel") *) ->
      (* continuing: *) raise (Exception (Printexc.to_string exn))
    end
  end

(* Main *)
let main () =
  Journal.keep_file "./.frama-c/frama_c_journal.ml";
  try run ()
  with
  | Unreachable -> Kernel.fatal "Journal reaches an assumed dead code"
  | Exception s -> Kernel.log "Journal re-raised the exception %S" s
  | exn ->
    Kernel.fatal
      "Journal raised an unexpected exception: %s"
      (Printexc.to_string exn)

(* Registering *)
let main : unit -> unit =
  Dynamic.register
    ~plugin:"Frama_c_journal.ml"
    "main"
    (Datatype.func Datatype.unit Datatype.unit)
    ~journalize:false
    main

(* Hooking *)
let () = Cmdline.run_after_loading_stage main; Cmdline.is_going_to_load ()
No tags attached.
c main.c (319) 2019-07-26 16:05
https://bts.frama-c.com/file_download.php?file_id=1319&type=bug
Issue History
2019-07-26 16:05Victor SverdlinNew Issue
2019-07-26 16:05Victor SverdlinFile Added: main.c
2019-08-01 16:03signolesNote Added: 0006840
2019-08-01 16:04signolesAssigned To => signoles
2019-08-01 16:04signolesStatusnew => feedback
2019-08-05 16:18Victor SverdlinNote Added: 0006841
2019-08-05 16:18Victor SverdlinStatusfeedback => assigned

Notes
(0006840)
signoles   
2019-08-01 16:03   
I cannot reproduce your issue (either by reproducing the steps in the GUI, or by executing the provided journal). I test it on a .c file of my own (a very basic one).

Could you provide additional details and your C file that reproduce the issue?

Thank you
(0006841)
Victor Sverdlin   
2019-08-05 16:18   
Actually, it can be any file. I've tested it on real source from the project and on the simple hello_world.c too with same effect. Some files are OK some not. I work from virtual machine, could it be the reason? Is there any way to check installation?

All the best.