3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00

Added dummy code contracts for .NET Core/CoreCLR builds.

This commit is contained in:
Christoph M. Wintersteiger 2016-10-06 16:24:49 +01:00
parent 4956f6ef5b
commit 9548b88e71
2 changed files with 80 additions and 0 deletions

View file

@ -0,0 +1,59 @@
/*++
Copyright (<c>) 2016 Microsoft Corporation
Module Name:
Contracts.cs
Abstract:
Z3 Managed API: Dummy Code Contracts class for .NET
frameworks that don't support them (e.g., CoreCLR).
Author:
Christoph Wintersteiger (cwinter) 2016-10-06
Notes:
--*/
namespace System.Diagnostics.Contracts
{
public class ContractClass : Attribute
{
public ContractClass(Type t) { }
}
public class ContractClassFor : Attribute
{
public ContractClassFor(Type t) { }
}
public class ContractInvariantMethod : Attribute
{
public ContractInvariantMethod() { }
}
public class ContractVerification : Attribute
{
public ContractVerification(bool b) { }
}
public class Pure : Attribute { }
public static class Contract
{
public static void Ensures(bool b) { }
public static void Requires(bool b) { }
public static void Assume(bool b, string msg) { }
public static void Assert(bool b) { }
public static bool ForAll(bool b) { return true; }
public static bool ForAll(Object c, Func<Object, bool> p) { return true; }
public static bool ForAll(int from, int to, Predicate<int> p) { return true; }
public static void Invariant(bool b) { }
public static T[] Result<T>() { return new T[1]; }
public static void EndContractBlock() { }
public static T ValueAtReturn<T>(out T v) { T[] t = new T[1]; v = t[0]; return v; }
}
}

View file

@ -0,0 +1,21 @@
{
"version": "1.0.0-*",
"buildOptions": {
"debugType": "portable",
"emitEntryPoint": false,
"outputName": "Microsoft.Z3",
"compile": [ "../*.cs", "*.cs" ]
},
"dependencies": { },
"frameworks": {
"netcoreapp1.0": {
"dependencies": {
"Microsoft.NETCore.App": {
"type": "platform",
"version": "1.0.1"
}
},
"imports": "dnxcore50"
}
}
}