native.aug

A native C boundary · Source and specification

Files in this project

• main.aug
• native.aug

Code

Indentation

// aug-spec: "native.aug.md" explains this file. Read it before changes; refresh with aug spec.
Explanation 1Explanation 2
extern C puts(string message) returns c_int
Explanation 1Explanation 2
announce():
    unsafe:
        puts(message="hello from C FFI")

Braces

// aug-spec: "native.aug.md" explains this file. Read it before changes; refresh with aug spec.
Explanation 1Explanation 2
extern C puts(string message) returns c_int
Explanation 1Explanation 2
announce() {
    unsafe {
        puts(message="hello from C FFI")
    }
}

Compiled specification

Interactions and sequences

puts · source

It takes message as a string. It returns c_int. Native C implementation; only its declared contract is visible here.

announce · source

It can call C.puts. Within an unsafe block, it calls puts with message "hello from C FFI". Native operations must satisfy their declared C contracts. source

Checked interface

announce() returns void uses C.puts

It can call C.puts.