You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This probably boils down to an issue with Corral, but I thought I’d post here first in case there’s some issue with the way we’re invoking Corral.
% cat a.c &&echo --- && smack a.c#include <smack.h>#include <stdio.h>int main() { int x = 0; printf("Hello, world!"); assert(x);}---SMACK program verifier version 2.4.0Traceback (most recent call last): File "/usr/local/bin/smack", line 13, in <module> smack.top.main() File "/usr/local/bin/../share/smack/top.py", line 685, in main verify_bpl(args) File "/usr/local/bin/../share/smack/top.py", line 507, in verify_bpl verifier_output = try_command(command, timeout=args.time_limit) File "/usr/local/bin/../share/smack/utils.py", line 69, in try_command raise Exception(output)Exception: Single threaded program detectedLB: Took 0.00 sVerifying program while tracking: {assertsPassed}Program has a potential bug: Unhandled Exception:CoreLib.InsufficientDetailsToConstructCexPath: StratifiedInliningErrorReporter: Must find a successor at CoreLib.StratifiedInliningErrorReporter.GetAbsyTraceLabels (VC.StratifiedVC svc, System.Collections.Generic.IList`1[T] labels) [0x000ce] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 at CoreLib.StratifiedInliningErrorReporter.GetAbsyTrace (VC.StratifiedVC svc, System.Collections.Generic.IList`1[T] labels) [0x00027] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 at CoreLib.StratifiedInliningErrorReporter.OnModel (System.Collections.Generic.IList`1[T] labels, Microsoft.Boogie.Model model, Microsoft.Boogie.ProverInterface+Outcome proverOutcome) [0x0002e] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.CheckOutcomeCore (Microsoft.Boogie.ProverInterface+ErrorHandler handler, System.Int32 taskID) [0x006d0] in <19ca4884bb9d4ccb8c3a80682b5b183b>:0 at CoreLib.StratifiedInlining.CheckVC (Microsoft.Boogie.ProverInterface+ErrorHandler reporter) [0x0003e] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 at CoreLib.StratifiedInlining.Fwd (System.Collections.Generic.HashSet`1[T] openCallSites, CoreLib.StratifiedInliningErrorReporter reporter, System.Boolean main, System.Int32 recBound) [0x00110] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 at CoreLib.StratifiedInlining.VerifyImplementation (Microsoft.Boogie.Implementation impl, Microsoft.Boogie.VerifierCallback callback) [0x00645] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 at VC.ConditionGeneration.VerifyImplementation (Microsoft.Boogie.Implementation impl, System.Collections.Generic.List`1[Microsoft.Boogie.Counterexample]& errors, System.String requestId) [0x00019] in <693f0436fa9c41f6a229442309a8ffe4>:0 at cba.Util.BoogieVerify.Verify (Microsoft.Boogie.Program program, System.Boolean needErrorTraces, System.Collections.Generic.List`1[cba.Util.BoogieErrorTrace]& allErrors, System.Collections.Generic.List`1[System.String]& timedOut, System.Boolean isCBA) [0x003f0] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 at cba.Util.BoogieVerify.Verify (Microsoft.Boogie.Program program, System.Collections.Generic.List`1[cba.Util.BoogieErrorTrace]& allErrors, System.Boolean isCBA) [0x00007] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 at cba.VerificationPass.feedToBoogie (cba.CBAProgram p) [0x00070] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 at cba.VerificationPass.runCBAPass (cba.CBAProgram prog) [0x0001f] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 at cba.CompilerPass.runPass (Microsoft.Boogie.Program inp) [0x00012] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 at ProgTransformation.TransformationPass.run (ProgTransformation.PersistentProgram inp) [0x0009c] in <5fc8c0b22e1047d2a1bef434cbda2c83>:0 at cba.CompilerPass.run (cba.PersistentCBAProgram inp) [0x00007] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 at cba.CBADriver.VerifyProgram (cba.PersistentCBAProgram& prog, cba.VarSet trackedVars, System.Boolean returnTrace, cba.PersistentCBAProgram& pout, cba.InsertionTrans& tinfo, cba.ErrorTrace& cex) [0x00156] in <9c847b8b7e9c451fb8593bfcea859ec4>:0 at cba.CBADriver.checkPath (cba.PersistentCBAProgram prog, cba.VarSet trackedVars, System.Boolean returnTrace, cba.PersistentCBAProgram& pout, cba.InsertionTrans& tinfo, cba.ErrorTrace& cex) [0x0002a] in <9c847b8b7e9c451fb8593bfcea859ec4>:0 at cba.CBADriver.checkPath (cba.PersistentCBAProgram pmeta, cba.VarSet trackedVars, cba.ErrorTrace& trace) [0x00001] in <9c847b8b7e9c451fb8593bfcea859ec4>:0 at cba.Driver.checkAndRefinePathFewPasses (cba.PersistentCBAProgram counterexample, cba.RefinementState refinementState, cba.ErrorTrace& cexTrace) [0x00013] in <9c847b8b7e9c451fb8593bfcea859ec4>:0 at cba.Driver.checkAndRefine (cba.PersistentCBAProgram prog, cba.RefinementState refinementState, System.Action`2[T1,T2] printTrace, cba.ErrorTrace& cexTrace) [0x001d4] in <9c847b8b7e9c451fb8593bfcea859ec4>:0 at cba.Driver.run (System.String[] args) [0x00466] in <9c847b8b7e9c451fb8593bfcea859ec4>:0 at cba.Driver.Main (System.String[] args) [0x00067] in <9c847b8b7e9c451fb8593bfcea859ec4>:0 [ERROR] FATAL UNHANDLED EXCEPTION: CoreLib.InsufficientDetailsToConstructCexPath: StratifiedInliningErrorReporter: Must find a successor at CoreLib.StratifiedInliningErrorReporter.GetAbsyTraceLabels (VC.StratifiedVC svc, System.Collections.Generic.IList`1[T] labels) [0x000ce] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 at CoreLib.StratifiedInliningErrorReporter.GetAbsyTrace (VC.StratifiedVC svc, System.Collections.Generic.IList`1[T] labels) [0x00027] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 at CoreLib.StratifiedInliningErrorReporter.OnModel (System.Collections.Generic.IList`1[T] labels, Microsoft.Boogie.Model model, Microsoft.Boogie.ProverInterface+Outcome proverOutcome) [0x0002e] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.CheckOutcomeCore (Microsoft.Boogie.ProverInterface+ErrorHandler handler, System.Int32 taskID) [0x006d0] in <19ca4884bb9d4ccb8c3a80682b5b183b>:0 at CoreLib.StratifiedInlining.CheckVC (Microsoft.Boogie.ProverInterface+ErrorHandler reporter) [0x0003e] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 at CoreLib.StratifiedInlining.Fwd (System.Collections.Generic.HashSet`1[T] openCallSites, CoreLib.StratifiedInliningErrorReporter reporter, System.Boolean main, System.Int32 recBound) [0x00110] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 at CoreLib.StratifiedInlining.VerifyImplementation (Microsoft.Boogie.Implementation impl, Microsoft.Boogie.VerifierCallback callback) [0x00645] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 at VC.ConditionGeneration.VerifyImplementation (Microsoft.Boogie.Implementation impl, System.Collections.Generic.List`1[Microsoft.Boogie.Counterexample]& errors, System.String requestId) [0x00019] in <693f0436fa9c41f6a229442309a8ffe4>:0 at cba.Util.BoogieVerify.Verify (Microsoft.Boogie.Program program, System.Boolean needErrorTraces, System.Collections.Generic.List`1[cba.Util.BoogieErrorTrace]& allErrors, System.Collections.Generic.List`1[System.String]& timedOut, System.Boolean isCBA) [0x003f0] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 at cba.Util.BoogieVerify.Verify (Microsoft.Boogie.Program program, System.Collections.Generic.List`1[cba.Util.BoogieErrorTrace]& allErrors, System.Boolean isCBA) [0x00007] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 at cba.VerificationPass.feedToBoogie (cba.CBAProgram p) [0x00070] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 at cba.VerificationPass.runCBAPass (cba.CBAProgram prog) [0x0001f] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 at cba.CompilerPass.runPass (Microsoft.Boogie.Program inp) [0x00012] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 at ProgTransformation.TransformationPass.run (ProgTransformation.PersistentProgram inp) [0x0009c] in <5fc8c0b22e1047d2a1bef434cbda2c83>:0 at cba.CompilerPass.run (cba.PersistentCBAProgram inp) [0x00007] in <74af7dec571c4e7cb3d494865d2ba8e7>:0 at cba.CBADriver.VerifyProgram (cba.PersistentCBAProgram& prog, cba.VarSet trackedVars, System.Boolean returnTrace, cba.PersistentCBAProgram& pout, cba.InsertionTrans& tinfo, cba.ErrorTrace& cex) [0x00156] in <9c847b8b7e9c451fb8593bfcea859ec4>:0 at cba.CBADriver.checkPath (cba.PersistentCBAProgram prog, cba.VarSet trackedVars, System.Boolean returnTrace, cba.PersistentCBAProgram& pout, cba.InsertionTrans& tinfo, cba.ErrorTrace& cex) [0x0002a] in <9c847b8b7e9c451fb8593bfcea859ec4>:0 at cba.CBADriver.checkPath (cba.PersistentCBAProgram pmeta, cba.VarSet trackedVars, cba.ErrorTrace& trace) [0x00001] in <9c847b8b7e9c451fb8593bfcea859ec4>:0 at cba.Driver.checkAndRefinePathFewPasses (cba.PersistentCBAProgram counterexample, cba.RefinementState refinementState, cba.ErrorTrace& cexTrace) [0x00013] in <9c847b8b7e9c451fb8593bfcea859ec4>:0 at cba.Driver.checkAndRefine (cba.PersistentCBAProgram prog, cba.RefinementState refinementState, System.Action`2[T1,T2] printTrace, cba.ErrorTrace& cexTrace) [0x001d4] in <9c847b8b7e9c451fb8593bfcea859ec4>:0 at cba.Driver.run (System.String[] args) [0x00466] in <9c847b8b7e9c451fb8593bfcea859ec4>:0 at cba.Driver.Main (System.String[] args) [0x00067] in <9c847b8b7e9c451fb8593bfcea859ec4>:0
The text was updated successfully, but these errors were encountered:
This probably boils down to an issue with Corral, but I thought I’d post here first in case there’s some issue with the way we’re invoking Corral.
The text was updated successfully, but these errors were encountered: