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
// ######################################
// # HEAP INITIALISATION #
// ######################################
type Ref;
type Field a;
type Heap = <a> [Ref, Field a] a;
const unique null : Ref;
const unique alloc : Field bool;
var heap : Heap;
// ######################################
// # LOCAL VARIABLES #
// ######################################
var this : Ref;
var time : Field int;
var value : Field int;
var error : Field bool;
// ######################################
// # SYMBOOGLIX #
// ######################################
procedure main(i : int)
{
var o : int;
call o := getElapsedTime(i);
}
// ######################################
// # METHODS #
// ######################################
procedure getElapsedTime(t : int) returns (r : int)
ensures heap == old(heap);
{
r := heap[this,time] - t;
}
This is not supported by the MapProxy and causes an exception to be raised when type checking
Symbooglix.ExprTypeCheckException: Type mismatch at index 1 expected type Field a but was type Field int
at Symbooglix.MapProxy.TypeCheckIndices (IList`1 indices) <0x40c3b140 + 0x002c7> in <filename unknown>:0
at Symbooglix.MapProxy.ReadMapAt (IList`1 indices) <0x40c3af10 + 0x00037> in <filename unknown>:0
at Symbooglix.SimpleVariableStore.ReadMap (Microsoft.Boogie.Variable mapVariable, IList`1 indicies) <0x40c3ae00 + 0x00077> in <filename unknown>:0
at Symbooglix.ExecutionState.ReadMapVariableInScopeAt (Microsoft.Boogie.Variable v, IList`1 indices) <0x40c3acf0 + 0x00092> in <filename unknown>:0
at Symbooglix.MapExecutionStateVariablesDuplicator.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) <0x40c391f0 + 0x003db> in <filename unknown>:0
at Microsoft.Boogie.NAryExpr.StdDispatch (Microsoft.Boogie.StandardVisitor visitor) <0x40b98d60 + 0x00020> in <filename unknown>:0
at Microsoft.Boogie.StandardVisitor.Visit (Microsoft.Boogie.Absy node) <0x40bb79f0 + 0x0001d> in <filename unknown>:0
at Microsoft.Boogie.Duplicator.Visit (Microsoft.Boogie.Absy node) <0x40c348f0 + 0x00017> in <filename unknown>:0
at Symbooglix.BuilderDuplicator.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) <0x40c39760 + 0x000ec> in <filename unknown>:0
at Symbooglix.MapExecutionStateVariablesDuplicator.VisitNAryExpr (Microsoft.Boogie.NAryExpr node) <0x40c391f0 + 0x003f7> in <filename unknown>:0
at Microsoft.Boogie.NAryExpr.StdDispatch (Microsoft.Boogie.StandardVisitor visitor) <0x40b98d60 + 0x00020> in <filename unknown>:0
at Microsoft.Boogie.StandardVisitor.Visit (Microsoft.Boogie.Absy node) <0x40bb79f0 + 0x0001d> in <filename unknown>:0
at Microsoft.Boogie.Duplicator.Visit (Microsoft.Boogie.Absy node) <0x40c348f0 + 0x00017> in <filename unknown>:0
at Symbooglix.Executor.Handle (Microsoft.Boogie.AssignCmd c) <0x40c38000 + 0x00884> in <filename unknown>:0
at (wrapper dynamic-method) System.Object:CallSite.Target (System.Runtime.CompilerServices.Closure,System.Runtime.CompilerServices.CallSite,Symbooglix.Executor,object)
at System.Dynamic.UpdateDelegates.UpdateAndExecuteVoid2[T0,T1] (System.Runtime.CompilerServices.CallSite site, System.Dynamic.T0 arg0, System.Dynamic.T1 arg1) <0x40bd47f0 + 0x0053b> in <filename unknown>:0
at (wrapper dynamic-method) System.Object:CallSite.Target (System.Runtime.CompilerServices.Closure,System.Runtime.CompilerServices.CallSite,Symbooglix.Executor,object)
at Symbooglix.Executor.ExecuteInstruction () <0x40bcff40 + 0x001c3> in <filename unknown>:0
at Symbooglix.Executor.InternalRun (Microsoft.Boogie.Implementation entryPoint, Int32 timeout) <0x40bb46b0 + 0x0059b> in <filename unknown>:0
at Symbooglix.Executor.Run (Microsoft.Boogie.Implementation entryPoint, Int32 timeout) <0x40bb4040 + 0x0015f> in <filename unknown>:0
Exiting with EXCEPTION_RAISED
The text was updated successfully, but these errors were encountered:
Symbooglix cannot currently run this
This is not supported by the MapProxy and causes an exception to be raised when type checking
The text was updated successfully, but these errors were encountered: