mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

Merge pull request #869 from danpere/fix/coreclr

Browse source 
Fix .NET Core bindings
This commit is contained in:
Nikolaj Bjorner 2017-01-11 20:52:49 -08:00 • committed by GitHub
commit 9e4142d599
2 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
scripts/update_api.py
View file

@ -365,7 +365,7 @@ def mk_dotnet(dotnet):
dotnet.write(' public delegate void Z3_error_handler(Z3_context c, Z3_error_code e);\n\n') dotnet.write(' public delegate void Z3_error_handler(Z3_context c, Z3_error_code e);\n\n')
dotnet.write(' public class LIB\n') dotnet.write(' public class LIB\n')
dotnet.write(' {\n') dotnet.write(' {\n')
dotnet.write(' const string Z3_DLL_NAME = \"libz3.dll\";\n' dotnet.write(' const string Z3_DLL_NAME = \"libz3\";\n'
' \n') ' \n')
dotnet.write(' [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]\n') dotnet.write(' [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]\n')
dotnet.write(' public extern static void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1);\n\n') dotnet.write(' public extern static void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1);\n\n')

6
src/api/dotnet/core/DummyContracts.cs
View file

@ -44,15 +44,21 @@ namespace System.Diagnostics.Contracts
public static class Contract public static class Contract
{ {
[Conditional("false")]
public static void Ensures(bool b) { } public static void Ensures(bool b) { }
[Conditional("false")]
public static void Requires(bool b) { } public static void Requires(bool b) { }
[Conditional("false")]
public static void Assume(bool b, string msg) { } public static void Assume(bool b, string msg) { }
[Conditional("false")]
public static void Assert(bool b) { } public static void Assert(bool b) { }
public static bool ForAll(bool b) { return true; } public static bool ForAll(bool b) { return true; }
public static bool ForAll(Object c, Func<Object, bool> p) { 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 bool ForAll(int from, int to, Predicate<int> p) { return true; }
[Conditional("false")]
public static void Invariant(bool b) { } public static void Invariant(bool b) { }
public static T[] Result<T>() { return new T[1]; } public static T[] Result<T>() { return new T[1]; }
[Conditional("false")]
public static void EndContractBlock() { } public static void EndContractBlock() { }
public static T ValueAtReturn<T>(out T v) { T[] t = new T[1]; v = t[0]; return v; } public static T ValueAtReturn<T>(out T v) { T[] t = new T[1]; v = t[0]; return v; }
} }