Prover fails to complete

[sschaub]

Another example where the prover fails to complete:

Facility PushDemo;
    uses String_Theory;
    Facility Integer_Stack_Fac is Stack_Template(Integer, 5)
            realized by Array_Realiz;

    Operation MyPush(preserves I: Integer; updates S: Stack);
      ensures (|#S| < 5 and S = <#I> o #S) or |#S| = 5 and S = #S;
    Procedure
      Var J: Integer;
      J := I;
      If Depth(S) + 1 <= 5 then
        Push(J, S);
      end;
    end;

  Operation Main(); 
  Procedure 


  end Main;

end;

[mikekab]

Hi,

I ran this example before applying this morning's update. No problems.
Applied the update:
Error:(VCGenerator) Ty is ambiguous: NameTy
Integer
If you run it locally, you will see the compiler is exiting the process.
Mike

On Thu, Nov 5, 2015 at 1:50 PM, sschaub notifications@github.com wrote:

Another example where the prover fails to complete:

Facility PushDemo;
uses String_Theory;
Facility Integer_Stack_Fac is Stack_Template(Integer, 5)
realized by Array_Realiz;

Operation MyPush(preserves I: Integer; updates S: Stack);
  ensures (|#S| < 5 and S = <#I> o #S) or |#S| = 5 and S = #S;
Procedure
  Var J: Integer;
  J := I;
  If Depth(S) + 1 <= 5 then
    Push(J, S);
  end;
end;

Operation Main();
Procedure

end Main;

end;

—
Reply to this email directly or view it on GitHub
#205.

[yushan87]

So the general problem is there is a crash somewhere in the VC Generator, but the compiler is choosing to ignore that exception and reporting "done" to the WebIDE. The WebIDE is then confused about why the VCs field is blank...

[yushan87]

Pull Request #206 allows the files in issue #204 and in this one to compile. However, the general crash error is still pending. Therefore, this issue shall remain open...