Crash when returning structs from functions

The plugin (using the current tip: 95923bc) crash when returning structs from functions with the following stack trace:

The full backtrace is: Raised at Stdlib.invalid_arg in file "stdlib.ml", line 30, characters 20-45 Called from StdlibOption.get in file "option.ml" (inlined), line 21, characters 41-69 Called from IspIsp_emitters.Auxiliary.emit_eva_result_of_term in file "src/isp_emitters.ml", line 202, characters 30-57 Called from StdlibHashtbl.iter.do_bucket in file "hashtbl.ml", line 159, characters 8-18 Called from StdlibHashtbl.iter in file "hashtbl.ml", line 165, characters 6-21 Re-raised at StdlibHashtbl.iter in file "hashtbl.ml", line 170, characters 4-13 Called from IspIsp_emitters.Auxiliary.emit in file "src/isp_emitters.ml", line 340, characters 4-56 Called from IspIsp_visitor.interface_specifications_propagator#vstmt_aux in file "src/isp_visitor.ml", line 243, characters 12-74 Called from Frama_c_kernelVisitor.internal_generic_frama_c_visitor#vstmt in file "src/kernel_services/visitors/visitor.ml", line 73, characters 16-35 Called from Frama_c_kernelCil.doVisit in file "src/kernel_services/ast_queries/cil.ml", line 1292, characters 15-31 Called from Frama_c_kernelCil.visitCilStmt in file "src/kernel_services/ast_queries/cil.ml", line 2410, characters 4-103 Called from Frama_c_kernelCil.mapNoCopy.aux in file "src/kernel_services/ast_queries/cil.ml", line 1331, characters 15-18 Called from Frama_c_kernelCil.childrenBlock in file "src/kernel_services/ast_queries/cil.ml", line 2598, characters 15-39 Called from Frama_c_kernelCil.doVisit in file "src/kernel_services/ast_queries/cil.ml", line 1307, characters 19-39 Called from Frama_c_kernelCil.childrenFunction in file "src/kernel_services/ast_queries/cil.ml", line 2826, characters 13-38 Called from Frama_c_kernelCil.doVisit in file "src/kernel_services/ast_queries/cil.ml", line 1307, characters 19-39 Called from Frama_c_kernelCil.visitCilFunction in file "src/kernel_services/ast_queries/cil.ml", line 2787, characters 4-89 Called from Frama_c_kernelCil.childrenGlobal in file "src/kernel_services/ast_queries/cil.ml", line 2879, characters 13-35 Called from Frama_c_kernelCil.mapNoCopy.aux in file "src/kernel_services/ast_queries/cil.ml", line 1331, characters 15-18 Called from Frama_c_kernelCil.doVisitList in file "src/kernel_services/ast_queries/cil.ml", line 1376, characters 20-53 Called from Frama_c_kernelCil.visitCilGlobal in file "src/kernel_services/ast_queries/cil.ml", line 2873, characters 4-52 Called from Frama_c_kernelCil.childrenFileCopy.fGlob in file "src/kernel_services/ast_queries/cil.ml", line 5386, characters 16-36 Called from Frama_c_kernelCil.childrenFileCopy in file "src/kernel_services/ast_queries/cil.ml", line 5393, characters 2-19 Called from Frama_c_kernelCil.doVisit in file "src/kernel_services/ast_queries/cil.ml", line 1307, characters 19-39 Called from Frama_c_kernelVisitor.visitFramacFileCopy in file "src/kernel_services/visitors/visitor.ml" (inlined), line 856, characters 32-68 Called from Frama_c_kernelFile.init_project_from_visitor in file "src/kernel_services/ast_queries/file.ml", line 1846, characters 12-43 Called from Frama_c_kernel__File.create_project_from_visitor in file "src/kernel_services/ast_queries/file.ml", line 1881, characters 2-43 Called from IspIsp_visitor.execute_isp in file "src/isp_visitor.ml", line 305, characters 4-105 Called from StdlibQueue.iter.iter in file "queue.ml", line 121, characters 6-15 Called from Frama_c_bootBoot.play_analysis in file "src/init/boot/boot.ml", line 36, characters 4-20 Called from Frama_c_kernelCmdline.play_in_toplevel_one_shot in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 850, characters 2-9 Called from Frama_c_kernelCmdline.play_in_toplevel in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 880, characters 18-64 Called from Frama_c_kernel__Cmdline.catch_toplevel_run in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 233, characters 4-8

Unexpected error (Invalid_argument("option is None")).

The following test program can be used to reproduce the bug:

struct Strct
{
    int f1;
};

struct Strct s;

struct Strct get_struct(){
        return s;
}

void main()
{
        struct Strct ls;
        ls = get_struct();
}

rse-verification / interface-specification-propagator

Crash when returning structs from functions #6