Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002467Frama-CKernelpublic2019-07-26 16:052019-08-22 08:57
ReporterVictor Sverdlin 
Assigned Tosignoles 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionunable to reproduce 
Platformx86_64OSopensuse-tumbleweedOS Version20190723
Product VersionFrama-C 19-Potassium 
Target VersionFixed in Version 
Summary0002467: Crash at "hashtbl.ml", line 462
DescriptionRaised at file "hashtbl.ml", line 462, characters 17-32 Called from file "src/libraries/project/state_topological.ml", line 62, characters 23-38
Steps To ReproduceJust open new project and add at least one .c (or .h) file
Additional Information(* 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 ()
TagsNo tags attached.
Attached Filesc file icon main.c [^] (319 bytes) 2019-07-26 16:05 [Show Content]

- Relationships

-  Notes
(0006840)
signoles (manager)
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 (reporter)
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.
(0006842)
signoles (manager)
2019-08-19 09:09

Frama-C is often used on a virtual machine; so it cannot be the only reason. Are you sure that Frama-C is properly installed? Is the following command line working properly? $ frama-c-gui main.c
(0006845)
Victor Sverdlin (reporter)
2019-08-22 00:12

I have run it with parameters -kernel-msg-key pp and now it works ok. Can not reproduce anymore. Thanks!

- Issue History
Date Modified Username Field Change
2019-07-26 16:05 Victor Sverdlin New Issue
2019-07-26 16:05 Victor Sverdlin File Added: main.c
2019-08-01 16:03 signoles Note Added: 0006840
2019-08-01 16:04 signoles Assigned To => signoles
2019-08-01 16:04 signoles Status new => feedback
2019-08-05 16:18 Victor Sverdlin Note Added: 0006841
2019-08-05 16:18 Victor Sverdlin Status feedback => assigned
2019-08-19 09:09 signoles Note Added: 0006842
2019-08-19 09:09 signoles Status assigned => feedback
2019-08-22 00:12 Victor Sverdlin Note Added: 0006845
2019-08-22 00:12 Victor Sverdlin Status feedback => assigned
2019-08-22 08:57 signoles Status assigned => closed
2019-08-22 08:57 signoles Resolution open => unable to reproduce


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker