search

AdaCore / spark2014

SPARK 2014 is the new version of SPARK, a software development technology specifically designed for engineering high-reliability applications.
GNU General Public License v3.0
249 stars 33 forks source link

Strange traceback when running proof with gnatstudio from gnat-2021-20210519 #27

Closed jcdubois closed 3 years ago

jcdubois commented 3 years ago

When running a proof through gnatstudio (from gnat-2021-20210519) I am getting an output with strange traceback (see below).

To reproduce the problem you could run "SPARK => Prove All" from gnatstudio on the source code from branch "spark_model" from the "https://github.com/jcdubois/moth" repository (https://github.com/jcdubois/moth/tree/spark_model).

Note: Running the gnatprove without the GUI doesn't trigger the traceback.

gnatprove -P/home/jcd/Projects/hypervisor/moth/moth.gpr -j0 --ide-progress-bar --level=4 Phase 1 of 2: generation of Global contracts ... Phase 2 of 2: flow analysis and proof ... moth-config.ads:36:07: info: data dependencies proved[#0] moth-config.ads:44:07: info: data dependencies proved[#1] moth.ads:106:10: info: flow dependencies proved[#3] moth.ads:107:10: info: initial condition proved[#55] moth.ads:131:37: info: range check proved[#56] moth.ads:133:40: info: range check proved[#57] moth.ads:136:10: info: initialization of "Model" proved[#2] moth.ads:141:21: info: postcondition proved[#103] moth.ads:174:18: info: postcondition proved[#121] moth.ads:182:10: info: initialization of "task_id" proved[#10] moth.ads:186:18: info: postcondition proved[#127] moth.ads:195:24: info: initialization of "task_id" proved[#17] moth.ads:198:18: info: postcondition proved[#131] moth.ads:206:28: info: initialization of "task_id" proved[#8] moth.ads:209:18: info: postcondition proved[#134] moth.ads:231:23: info: initialization of "task_id" proved[#16] moth.ads:232:18: info: postcondition proved[#140] moth.ads:278:10: info: initialization of "status" proved[#14] moth.ads:278:36: info: initialization of "mbx_entry" proved[#15] moth.ads:280:18: info: postcondition proved[#159] moth.ads:288:10: info: initialization of "status" proved[#0] moth.ads:292:18: info: postcondition proved[#163] moth.ads:301:18: info: postcondition proved[#164] moth.ads:305:20: info: initialization of "task_id" proved[#13] moth.ads:306:15: info: postcondition proved[#165] a-cforse.ads:516:18: info: precondition proved, in instantiation at moth.ads:124[#83] Traceback (most recent call last): File "/opt/GNAT/2021/share/gnatstudio/plug-ins/jobs_view.py", line 128, in on_stdout self.child.on_stdout(text, command) File "/opt/GNAT/2021/share/gnatstudio/plug-ins/spark2014.py", line 918, in on_stdout fn, lineno, column, text, importance, extra) File "/opt/GNAT/2021/share/gnatstudio/plug-ins/spark2014.py", line 836, in split_in_secondary_messages extra)) GPS.Unexpected_Exception: unexpected internal exception raised GNATCOLL.SCRIPTS.NO_SUCH_PARAMETER : 7 [/opt/GNAT/2021/bin/../lib/gnatstudio/libgnatcoll_python.so.22.0w] 0x7fe59162c829 [/opt/GNAT/2021/bin/gnatstudio_exe] 0x3483695 [/opt/GNAT/2021/bin/../lib/gnatstudio/libgnatcoll_python.so.22.0w] 0x7fe59161b0ab 0x7fe59161d6d3 [/opt/GNAT/2021/bin/gnatstudio_exe] 0x3d504c4 0x3d50f3a 0x3d50f3a 0x3d524d6 0x3ce89ff 0x3ccc311 0x3cd05ba 0x3ccc311 [/opt/GNAT/2021/bin/../lib/gnatstudio/libgnatcoll_python.so.22.0w] 0x7fe59162d8df 0x7fe59162debc 0x7fe59162e04e [/opt/GNAT/2021/bin/../lib/gnatstudio/libgnatcoll.so.22.0w] 0x7fe5902f6f5a gnatcollscriptsexecute__4 at ??? [/opt/GNAT/2021/bin/gnatstudio_exe] 0x2a0bec1 0x2a2d6ef 0x31e07e4 0x2cf054e 0x2cf09a7 0x2cf0e4d 0x2d69b7c 0x2d6aa25 0x2d679e9 [/opt/GNAT/2021/bin/../lib/gnatstudio/libglib-2.0.so.0] 0x7fe58872ac22 g_timeout_dispatch at gmain.c:4545 0x7fe58872a4a3 g_main_context_dispatch at gmain.c:3122 0x7fe58872a7e6 g_main_context_iterate.constprop.0 at gmain.c:3808 0x7fe58872a88d g_main_context_iteration at gmain.c:3869 [/opt/GNAT/2021/bin/../lib/gnatstudio/libgio-2.0.so.0] 0x7fe588ed59ea g_application_run at gapplication.c:2308 [/opt/GNAT/2021/bin/gnatstudio_exe] 0x206f250 0x2051a64 [/lib/x86_64-linux-gnu/libc.so.6] 0x7fe5874b5563 [/opt/GNAT/2021/bin/gnatstudio_exe] 0x2051ab7 0xfffffffffffffffe

a-cforse.ads:1397:20: info: precondition proved, in instantiation at moth.ads:124[#99] Traceback (most recent call last): File "/opt/GNAT/2021/share/gnatstudio/plug-ins/jobs_view.py", line 128, in on_stdout self.child.on_stdout(text, command) File "/opt/GNAT/2021/share/gnatstudio/plug-ins/spark2014.py", line 918, in on_stdout fn, lineno, column, text, importance, extra) File "/opt/GNAT/2021/share/gnatstudio/plug-ins/spark2014.py", line 836, in split_in_secondary_messages extra)) GPS.Unexpected_Exception: unexpected internal exception raised GNATCOLL.SCRIPTS.NO_SUCH_PARAMETER : 7 [/opt/GNAT/2021/bin/../lib/gnatstudio/libgnatcoll_python.so.22.0w] 0x7fe59162c829 [/opt/GNAT/2021/bin/gnatstudio_exe] 0x3483695 [/opt/GNAT/2021/bin/../lib/gnatstudio/libgnatcoll_python.so.22.0w] 0x7fe59161b0ab 0x7fe59161d6d3 [/opt/GNAT/2021/bin/gnatstudio_exe] 0x3d504c4 0x3d50f3a 0x3d50f3a 0x3d524d6 0x3ce89ff 0x3ccc311 0x3cd05ba 0x3ccc311 [/opt/GNAT/2021/bin/../lib/gnatstudio/libgnatcoll_python.so.22.0w] 0x7fe59162d8df 0x7fe59162debc 0x7fe59162e04e [/opt/GNAT/2021/bin/../lib/gnatstudio/libgnatcoll.so.22.0w] 0x7fe5902f6f5a gnatcollscriptsexecute__4 at ??? [/opt/GNAT/2021/bin/gnatstudio_exe] 0x2a0bec1 0x2a2d6ef 0x31e07e4 0x2cf054e 0x2cf09a7 0x2cf0e4d 0x2d69b7c 0x2d6aa25 0x2d679e9 [/opt/GNAT/2021/bin/../lib/gnatstudio/libglib-2.0.so.0] 0x7fe58872ac22 g_timeout_dispatch at gmain.c:4545 0x7fe58872a4a3 g_main_context_dispatch at gmain.c:3122 0x7fe58872a7e6 g_main_context_iterate.constprop.0 at gmain.c:3808 0x7fe58872a88d g_main_context_iteration at gmain.c:3869 [/opt/GNAT/2021/bin/../lib/gnatstudio/libgio-2.0.so.0] 0x7fe588ed59ea g_application_run at gapplication.c:2308 [/opt/GNAT/2021/bin/gnatstudio_exe] 0x206f250 0x2051a64 [/lib/x86_64-linux-gnu/libc.so.6] 0x7fe5874b5563 [/opt/GNAT/2021/bin/gnatstudio_exe] 0x2051ab7 0xfffffffffffffffe

a-cfdlli.ads:1262:06: info: disjoint contract cases proved, in instantiation at moth.ads:117[#72] Traceback (most recent call last): File "/opt/GNAT/2021/share/gnatstudio/plug-ins/jobs_view.py", line 128, in on_stdout self.child.on_stdout(text, command) File "/opt/GNAT/2021/share/gnatstudio/plug-ins/spark2014.py", line 918, in on_stdout fn, lineno, column, text, importance, extra) File "/opt/GNAT/2021/share/gnatstudio/plug-ins/spark2014.py", line 836, in split_in_secondary_messages extra)) GPS.Unexpected_Exception: unexpected internal exception raised GNATCOLL.SCRIPTS.NO_SUCH_PARAMETER : 7 [/opt/GNAT/2021/bin/../lib/gnatstudio/libgnatcoll_python.so.22.0w] 0x7fe59162c829 [/opt/GNAT/2021/bin/gnatstudio_exe] 0x3483695 [/opt/GNAT/2021/bin/../lib/gnatstudio/libgnatcoll_python.so.22.0w] 0x7fe59161b0ab 0x7fe59161d6d3 [/opt/GNAT/2021/bin/gnatstudio_exe] 0x3d504c4 0x3d50f3a 0x3d50f3a 0x3d524d6 0x3ce89ff 0x3ccc311 0x3cd05ba 0x3ccc311 [/opt/GNAT/2021/bin/../lib/gnatstudio/libgnatcoll_python.so.22.0w] 0x7fe59162d8df 0x7fe59162debc 0x7fe59162e04e [/opt/GNAT/2021/bin/../lib/gnatstudio/libgnatcoll.so.22.0w] 0x7fe5902f6f5a gnatcollscriptsexecute__4 at ??? [/opt/GNAT/2021/bin/gnatstudio_exe] 0x2a0bec1 0x2a2d6ef 0x31e07e4 0x2cf054e 0x2cf09a7 0x2cf0e4d 0x2d69b7c 0x2d6aa25 0x2d679e9 [/opt/GNAT/2021/bin/../lib/gnatstudio/libglib-2.0.so.0] 0x7fe58872ac22 g_timeout_dispatch at gmain.c:4545 0x7fe58872a4a3 g_main_context_dispatch at gmain.c:3122 0x7fe58872a7e6 g_main_context_iterate.constprop.0 at gmain.c:3808 0x7fe58872a88d g_main_context_iteration at gmain.c:3869 [/opt/GNAT/2021/bin/../lib/gnatstudio/libgio-2.0.so.0] 0x7fe588ed59ea g_application_run at gapplication.c:2308 [/opt/GNAT/2021/bin/gnatstudio_exe] 0x206f250 0x2051a64 [/lib/x86_64-linux-gnu/libc.so.6] 0x7fe5874b5563 [/opt/GNAT/2021/bin/gnatstudio_exe] 0x2051ab7 0xfffffffffffffffe

moth-scheduler.adb:228:13: info: precondition proved[#105] moth-scheduler.adb:240:49: info: range check proved[#117] moth-scheduler.adb:245:68: info: index check proved[#112] moth-scheduler.adb:248:22: info: precondition proved[#106] moth-scheduler.adb:249:22: info: precondition proved[#109] moth-scheduler.adb:250:38: info: precondition proved[#108] moth-scheduler.adb:250:57: info: range check proved[#107]

...

yannickmoy commented 3 years ago

I cannot reproduce with GNAT Community 2021 on Ubuntu. For some reason, it seems that in your install, the call to self.analysis_tool.create_message at line 831 of spark2014.py does not accept a 7th parameter. A workaround is to patch the file spark2014.py to avoid calling split_in_secondary_messages:

                # Add action to the message
                if extra:
                    pass
                    # self.has_analysis_messages = True
                    # # Create the message and its secondaries
                    # message = self.split_in_secondary_messages(
                    #     fn, lineno, column, text, importance, extra)
                    # self.act_on_extra_info(
                    #     message, extra, imported_units[unit], command)
jcdubois commented 3 years ago

Le 30/07/2021 à 10:26, yannickmoy a écrit :

I cannot reproduce with GNAT Community 2021 on Ubuntu.

I am running GNAT community 2021 on Xubuntu 21.04.

For some reason, it seems that in your install, the call to |self.analysis_tool.create_message| at line 831 of spark2014.py does not accept a 7th parameter. A workaround is to patch the file |spark2014.py| to avoid calling |split_in_secondary_messages|:

|# Add action to the message if extra: pass # self.has_analysis_messages = True # # Create the message and its secondaries # message = self.split_in_secondary_messages( # fn, lineno, column, text, importance, extra) # self.act_on_extra_info( # message, extra, imported_units[unit], command)| |Do you mean it is up to the user to patch gnatstudio files to get it to work?|

JC

||

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/AdaCore/spark2014/issues/27#issuecomment-889729494, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAJUSWPD7LYX3AQ56S32Z23T2JO4TANCNFSM5BG2S3XQ.

yannickmoy commented 3 years ago

Of course, it should work, and I don't know why you have this message, maybe a bad install? I'm just suggesting a workaround, as we can't fix Community release 2021 now.