A trailing "true" in a clause cause a segmentation fault.

mattiasw2 / teyjus

Automatically exported from code.google.com/p/teyjus

GNU General Public License v3.0

0 stars 0 forks source link

A trailing "true" in a clause cause a segmentation fault. #54

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago

It seems that compiling a clause of the form

r :- 1 = 1, true.

yields code that produces a segmentation fault when one attempts to prove r.  
Removing the trailing "true" fixes the problem.  I attach a simple mod and sig 
file for illustrating this problem.  Specifics of my system are below.  -Dale

$ tjcc -v
Teyjus version 2.0-b1
$ uname -a
Linux alonzo 2.6.32-34-generic #77-Ubuntu SMP Tue Sep 13 19:40:53 UTC 2011 i686 
GNU/Linux
$

Original issue reported on code.google.com by dale.a.m...@gmail.com on 15 Oct 2011 at 8:15

Attachments:

GoogleCodeExporter commented 9 years ago

The following patch seems to do the job (adding a last proceed is what was done 
in Teyjus 1):

svn diff source/compiler/clausegen.ml
@@ -1830,9 +1848,10 @@
    let (inst, size) =
      if (last) then 
        if (Absyn.getClauseHasEnv cl) then
-         ([Instr.Ins_deallocate], Instr.getSize_deallocate)
+                  ([Instr.Ins_deallocate ; Instr.Ins_proceed], 
+                        Instr.getSize_deallocate + Instr.getSize_proceed)

The number of tests checked remains the same.

Fabien

Original comment by fafounet@gmail.com on 29 Jan 2013 at 11:04

GoogleCodeExporter commented 9 years ago

Gopalan, do you agree that a "proceed" should follow the deallocate as in 
Teyjus 1?

Original comment by fafounet@gmail.com on 28 Aug 2013 at 12:19