2021-02-24 18:25 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000510Frama-CPlug-in > jessiepublic2014-02-12 16:55
Reporteradytzul_ac 
Assigned Tosignoles 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000510: Jessie generates error when called to be executed.
DescriptionTest steps:
1. new project (see main.c from attachement)
2. Configure and Run Analysis menu: setting Jessie and Value Analysis both ON
3. Execute analysis

Results:
-see also JPEG from attachement
-see frama_c_journal.ml from attachement
The full backtrace is:
Raised at file "src/kernel/log.ml", line 506, characters 30-31
Called from file "src/kernel/log.ml", line 500, characters 2-9
Re-raised at file "src/kernel/log.ml", line 503, characters 8-9
Called from file "src/kernel/journal.ml", line 323, characters 15-26
Re-raised at file "src/kernel/journal.ml", line 338, characters 14-15
Called from file "src/lib/type.ml", line 746, characters 40-45
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 50, characters 4-20
Called from file "src/gui/launcher.ml", line 38, characters 7-23
Called from file "src/lib/extlib.ml", line 176, characters 12-15
Re-raised at file "src/lib/extlib.ml", line 181, characters 10-11
Called from file "src/gui/gtk_helper.ml", line 533, characters 8-385

Plug-in jessie aborted because of an internal error.
Look at the console for additional information (if any).
Please report as 'crash' at http://bts.frama-c.com
TagsNo tags attached.
Attached Files
  • jpg file icon error3.JPG (139,548 bytes) 2010-06-14 15:57 -
    jpg file icon error3.JPG (139,548 bytes) 2010-06-14 15:57 +
  • ? file icon frama_c_journal.ml (2,543 bytes) 2010-06-14 15:57 -
    (* Frama-C journal generated at 16:49 the 14/06/2010 *)
    
    exception Unreachable
    exception Exception of string
    
    (* Run the user commands *)
    let run () =
      File.init_from_cmdline ();
      let p_interactive = Project.create "interactive" in
      Project.set_current ~on:true p_interactive;
      Parameters.Files.set [ "D:\\main.c" ];
      File.init_from_cmdline ();
      Project.set_current ~on:true (Project.from_unique_name "default");
      Project.set_current p_interactive;
      !Db.Slicing.Project.set_project None;
      !Db.Metrics.compute ();
      Parameters.Dynamic.Bool.set "-jessie" true;
      Parameters.Dynamic.Bool.set "-jessie-adhoc-normalization" false;
      Parameters.Dynamic.Bool.set "-val" true;
      !Db.Value.compute ();
      begin try
        (* exception Log.AbortFatal("jessie") raised on:Applying dynamic
                                                          functions
                                                          "run_analysis" of type
                                                          unit -> unit *)
        Dynamic.get ~plugin:"Jessie" "run_analysis" (Type.func Type.unit Type.unit)
          ();
        raise Unreachable
      with
      | Unreachable as exn -> raise exn
      | exn (* Log.AbortFatal("jessie") *) ->
        (* continuing: *)
        !Db.Slicing.Project.set_project None;
        !Db.Value.compute ();
        begin try
          (* exception Log.AbortFatal("jessie") raised on:Applying dynamic
                                                            functions
                                                            "run_analysis" of
                                                            type unit -> unit *)
          Dynamic.get ~plugin:"Jessie" "run_analysis" (Type.func Type.unit Type.unit)
            ();
          raise Unreachable
        with
        | Unreachable as exn -> raise exn
        | exn (* Log.AbortFatal("jessie") *) ->
          (* continuing: *) !Db.Slicing.Project.set_project None; ()
        end
      end
    
    (* Main *)
    let main () =
      Journal.keep_file "frama_c_journal.ml";
      try run ()
      with
      | Unreachable -> Kernel.fatal "Journal reachs 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"
        "main"
        (Type.func Type.unit Type.unit)
        ~journalize:false
        main
    
    (* Hooking *)
    let () = Cmdline.run_after_loading_stage main; Cmdline.is_going_to_load ()
    
    ? file icon frama_c_journal.ml (2,543 bytes) 2010-06-14 15:57 +
  • c file icon main.c (239 bytes) 2010-06-14 15:58 -
    int i, t[10];
    
    int main(void)
    {
    	unsigned int j;
    	j=suma(1,2);
    	for(i=0;i<20;i++)
    		t[i]=i+1;
    	return 0;
    }
    
    int suma(int i, int j)
    {
    	if(i==0 && j==0)
    		return 0;
    	else
    		return i+j;
    }
    
    void f(void)
    {
    	return 1;
    }
    
    
    c file icon main.c (239 bytes) 2010-06-14 15:58 +

-Relationships
+Relationships

-Notes

~0000936

signoles (manager)

Error in the GUI launcher whenever there is an hook on a option which modifies another option.

~0000946

signoles (manager)

The remaining bug was resolved in another context few days ago.

~0000947

signoles (manager)

In any way, the Jessie plug-in has its own GUI. Thus it is better to not use the Frama-C GUI to run Jessie. Use the batch mode instead.
+Notes

-Issue History
Date Modified Username Field Change
2010-06-14 15:57 adytzul_ac New Issue
2010-06-14 15:57 adytzul_ac Status new => assigned
2010-06-14 15:57 adytzul_ac Assigned To => cmarche
2010-06-14 15:57 adytzul_ac File Added: error3.JPG
2010-06-14 15:57 adytzul_ac File Added: frama_c_journal.ml
2010-06-14 15:58 adytzul_ac File Added: main.c
2010-06-14 16:48 signoles Note Added: 0000936
2010-06-14 16:48 signoles Assigned To cmarche =>
2010-06-14 16:48 signoles Status assigned => confirmed
2010-06-15 10:15 signoles Assigned To => signoles
2010-06-15 10:15 signoles Status confirmed => assigned
2010-06-15 10:16 signoles Status assigned => confirmed
2010-06-15 10:17 svn
2010-06-25 10:55 signoles Status confirmed => resolved
2010-06-25 10:55 signoles Resolution open => fixed
2010-06-25 10:56 signoles Note Added: 0000946
2010-06-25 10:57 signoles Note Added: 0000947
2010-12-10 15:47 signoles Fixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:35 signoles Status resolved => closed
2013-12-19 01:13 signoles Source_changeset_attached => framac master 0786afba
2014-02-12 16:55 signoles Source_changeset_attached => framac stable/neon 0786afba
+Issue History