Skip to content

Commit b6ee16e

Browse files
authored
fix: improve golang externs (#1133)
* fix: improve golang externs
1 parent 983f752 commit b6ee16e

File tree

4 files changed

+23
-13
lines changed

4 files changed

+23
-13
lines changed

Diff for: StandardLibrary/runtimes/go/ImplementationFromDafny-go/FileIO/externs.go

+10-8
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ import (
55
os "os"
66
"path/filepath"
77

8+
"github.com/dafny-lang/DafnyRuntimeGo/v4/dafny"
89
_dafny "github.com/dafny-lang/DafnyRuntimeGo/v4/dafny"
910
)
1011

@@ -28,8 +29,7 @@ func (_static CompanionStruct_Default___) INTERNAL_ReadBytesFromFile(path _dafny
2829

2930
dat, err := ioutil.ReadFile(p)
3031
if err != nil {
31-
errAsSequence := _dafny.UnicodeSeqOfUtf8Bytes(err.Error())
32-
return true, _dafny.EmptySeq, errAsSequence
32+
return true, _dafny.EmptySeq, _dafny.SeqOfChars([]dafny.Char(err.Error())...)
3333
}
3434
datAsSequence := _dafny.SeqOfBytes(dat)
3535
return false, datAsSequence, _dafny.EmptySeq
@@ -53,8 +53,7 @@ func (_static CompanionStruct_Default___) INTERNAL_WriteBytesToFile(path _dafny.
5353
bytesArray := _dafny.ToByteArray(bytes)
5454
err := ioutil.WriteFile(p, bytesArray, 0644)
5555
if err != nil {
56-
errAsSequence := _dafny.UnicodeSeqOfUtf8Bytes(err.Error())
57-
return true, errAsSequence
56+
return true, _dafny.SeqOfChars([]dafny.Char(err.Error())...)
5857
}
5958
return false, _dafny.EmptySeq
6059
}
@@ -73,21 +72,24 @@ func (_static CompanionStruct_Default___) INTERNAL_AppendBytesToFile(path _dafny
7372
}()
7473

7574
// Create directories
76-
os.MkdirAll(filepath.Dir(p), os.ModePerm)
75+
err := os.MkdirAll(filepath.Dir(p), os.ModePerm)
76+
if err != nil {
77+
return true, _dafny.SeqOfChars([]dafny.Char(err.Error())...)
78+
}
7779

7880
bytesArray := _dafny.ToByteArray(bytes)
7981

8082
f, err := os.OpenFile(p, os.O_APPEND|os.O_CREATE|os.O_WRONLY, 0644)
8183
if err != nil {
82-
return true, _dafny.UnicodeSeqOfUtf8Bytes(err.Error())
84+
return true, _dafny.SeqOfChars([]dafny.Char(err.Error())...)
8385
}
8486

8587
if _, err := f.Write(bytesArray); err != nil {
86-
return true, _dafny.UnicodeSeqOfUtf8Bytes(err.Error())
88+
return true, _dafny.SeqOfChars([]dafny.Char(err.Error())...)
8789
}
8890

8991
if err := f.Close(); err != nil {
90-
return true, _dafny.UnicodeSeqOfUtf8Bytes(err.Error())
92+
return true, _dafny.SeqOfChars([]dafny.Char(err.Error())...)
9193
}
9294

9395
return false, _dafny.EmptySeq

Diff for: StandardLibrary/runtimes/go/ImplementationFromDafny-go/Time_/externs.go

+5-2
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,10 @@ func (CompanionStruct_Default___) GetProcessCpuTimeMillis() int64 {
3838
}
3939

4040
func GetProcessCpuTimeMillis() int64 {
41-
usage := new(syscall.Rusage)
42-
syscall.Getrusage(syscall.RUSAGE_SELF, usage)
41+
var usage syscall.Rusage
42+
err := syscall.Getrusage(syscall.RUSAGE_SELF, &usage)
43+
if err != nil {
44+
return 0
45+
}
4346
return (usage.Utime.Nano() + usage.Stime.Nano()) / 1000000
4447
}

Diff for: StandardLibrary/test/GetOpt.dfy

-3
Original file line numberDiff line numberDiff line change
@@ -152,7 +152,6 @@ module GetOptTest {
152152
]);
153153
var x :- expect GetOptions(MyOptions, ["cmd", "--help"]);
154154
var y :- expect NeedsHelp(MyOptions, x);
155-
print "\n", y, "\n";
156155
}
157156

158157
method {:test} TestHelpFail() {
@@ -196,11 +195,9 @@ module GetOptTest {
196195

197196
x :- expect GetOptions(MyOptions, ["MyProg", "--help"]);
198197
var y :- expect NeedsHelp(MyOptions, x);
199-
print "\n", y, "\n";
200198

201199
x :- expect GetOptions(MyOptions, ["MyProg", "command", "--help"]);
202200
y :- expect NeedsHelp(MyOptions, x);
203-
print "\n", y, "\n";
204201
}
205202

206203
method {:test} TestDefault() {

Diff for: StandardLibrary/test/TestString.dfy

+8
Original file line numberDiff line numberDiff line change
@@ -47,4 +47,12 @@ module TestStrings {
4747
expect y == [1,2,3,4,5];
4848
}
4949

50+
// ensure that FileIO error are returned properly, and not a panic! or the like
51+
// This fails to fail on Windows+Dotnet, becasue \ instead of /
52+
// method {:test} TestBadFileIO()
53+
// {
54+
// var x := WriteBytesToFile("/../../MyFile", [1,2,3,4,5]);
55+
// expect x.Failure?;
56+
// }
57+
5058
}

0 commit comments

Comments
 (0)